HasFiniteRange predicate on linear maps, and the associated equivalence relation

In this file, we define:

• LinearMap.HasFiniteRange: a predicate expressing that a linear map has finitely generated range.
• LinearMap.HasNoetherianRange: a predicate expressing that a linear map has noetherian range, i.e, all submodules of the range are finitely generated. This should be thought of as the "better behaved" version of LinearMap.HasFiniteRange: for example, HasNoetherianRange is always stable by addition, whereas HasFiniteRange might not be. The two notions agree over noetherian rings (hence, in particular, over fields).
• LinearMap.finiteRange: the submodule of E →ₗ[K] F consisting of linear maps with noetherian ranges. We allow ourself this slightly abusive name because the more natural definition (the submodule of linear maps with finitely generated ranges) only makes sense over a noetherian ring, in which case the two notions agree.
• LinearMap.FiniteRangeSetoid.setoid: the setoid on E →ₗ[K] F associated to LinearMap.finiteRange. This identifies linear maps which differ by a linear map with noetherian range. Equivalently, two linear maps are equivalent for this relation if and only if they agree on a subspace A of the domain such that E ⧸ A is noetherian. As with LinearMap.finiteRange, we allow ourself a slightly abusive name because the more natural definition in terms of LinearMap.HasFiniteRange is only well behaved over a noetherian ring, in which case the two notions agree. This is an instance in the scope LinearMap.FiniteRangeSetoid, so opening this scope allows this relation to be denoted by ≈.
• LinearMap.IsQuasiInverse: two linear maps u and v are quasi-inverses if we have u ∘ₗ v ≈ id and v ∘ₗ u ≈ id modulo linear maps with noetherian ranges.

def LinearMap.HasNoetherianRange {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] (f : V →ₗ[K] V₂) : Prop

A linear map has Noetherian range if its range is a Noetherian module.

Equations

• f.HasNoetherianRange = IsNoetherian K ↥f.range

def LinearMap.HasFiniteRange {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] (f : V →ₗ[K] V₂) : Prop

A linear map has finite range if its range is finitely generated.

Equations

• f.HasFiniteRange = f.range.FG

theorem LinearMap.hasNoetherianRange_iff_range {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] {f : V →ₗ[K] V₂} : f.HasNoetherianRange ↔ IsNoetherian K ↥f.range

theorem LinearMap.hasFiniteRange_iff_range {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] {f : V →ₗ[K] V₂} : f.HasFiniteRange ↔ f.range.FG

theorem LinearMap.HasNoetherianRange.isNoetherian_range {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] {f : V →ₗ[K] V₂} : f.HasNoetherianRange → IsNoetherian K ↥f.range

Alias of the forward direction of LinearMap.hasNoetherianRange_iff_range.

theorem LinearMap.HasFiniteRange.fg_range {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] {f : V →ₗ[K] V₂} : f.HasFiniteRange → f.range.FG

Alias of the forward direction of LinearMap.hasFiniteRange_iff_range.

theorem LinearMap.HasNoetherianRange.hasFiniteRange {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] {u : V →ₗ[K] V₂} (h : u.HasNoetherianRange) : u.HasFiniteRange

@[simp]

theorem LinearMap.HasNoetherianRange.zero {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] : HasNoetherianRange 0

@[simp]

theorem LinearMap.HasFiniteRange.zero {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] : HasFiniteRange 0

theorem LinearMap.HasNoetherianRange.comp_left {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] [AddCommMonoid V₃] [Module K V₃] {u : V →ₗ[K] V₂} (h : u.HasNoetherianRange) (v : V₂ →ₗ[K] V₃) : (v ∘ₗ u).HasNoetherianRange

theorem LinearMap.HasFiniteRange.comp_left {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] [AddCommMonoid V₃] [Module K V₃] {u : V →ₗ[K] V₂} (h : u.HasFiniteRange) (v : V₂ →ₗ[K] V₃) : (v ∘ₗ u).HasFiniteRange

@[simp]

theorem LinearMap.HasNoetherianRange.of_isNoetherian_dom {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] [IsNoetherian K V] {f : V →ₗ[K] V₂} : f.HasNoetherianRange

@[simp]

theorem LinearMap.HasFiniteRange.of_finite_dom {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] [Module.Finite K V] {f : V →ₗ[K] V₂} : f.HasFiniteRange

@[simp]

theorem LinearMap.HasNoetherianRange.of_isNoetherian_rng {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] [IsNoetherian K V₂] {f : V →ₗ[K] V₂} : f.HasNoetherianRange

@[simp]

theorem LinearMap.HasFiniteRange.of_isNoetherian_rng {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] [IsNoetherian K V₂] {f : V →ₗ[K] V₂} : f.HasFiniteRange

theorem LinearMap.HasFiniteRange.hasNoetherianRange {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [IsNoetherianRing K] {u : V →ₗ[K] V₂} (h : u.HasFiniteRange) : u.HasNoetherianRange

theorem LinearMap.hasNoetherianRange_iff_hasFiniteRange {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [IsNoetherianRing K] {u : V →ₗ[K] V₂} : u.HasNoetherianRange ↔ u.HasFiniteRange

theorem LinearMap.HasNoetherianRange.comp_right {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {v : V₂ →ₗ[K] V₃} (h : v.HasNoetherianRange) (u : V →ₗ[K] V₂) : (v ∘ₗ u).HasNoetherianRange

theorem LinearMap.HasFiniteRange.comp_right {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] [IsNoetherianRing K] {v : V₂ →ₗ[K] V₃} (h : v.HasFiniteRange) (u : V →ₗ[K] V₂) : (v ∘ₗ u).HasFiniteRange

@[simp]

theorem LinearMap.HasNoetherianRange.neg {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] {f : V →ₗ[K] V₂} (hf : f.HasNoetherianRange) : (-f).HasNoetherianRange

@[simp]

theorem LinearMap.HasFiniteRange.neg {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] {f : V →ₗ[K] V₂} (hf : f.HasFiniteRange) : (-f).HasFiniteRange

@[simp]

theorem LinearMap.HasNoetherianRange.add {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] {f g : V →ₗ[K] V₂} (hf : f.HasNoetherianRange) (hg : g.HasNoetherianRange) : (f + g).HasNoetherianRange

@[simp]

theorem LinearMap.HasFiniteRange.add {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [IsNoetherianRing K] {f g : V →ₗ[K] V₂} (hf : f.HasFiniteRange) (hg : g.HasFiniteRange) : (f + g).HasFiniteRange

@[simp]

theorem LinearMap.HasNoetherianRange.sub {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] {f g : V →ₗ[K] V₂} (hf : f.HasNoetherianRange) (hg : g.HasNoetherianRange) : (f - g).HasNoetherianRange

@[simp]

theorem LinearMap.HasFiniteRange.sub {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [IsNoetherianRing K] {f g : V →ₗ[K] V₂} (hf : f.HasFiniteRange) (hg : g.HasFiniteRange) : (f - g).HasFiniteRange

theorem LinearMap.hasNoetherianRange_iff_quotient_ker {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] {f : V →ₗ[K] V₂} : f.HasNoetherianRange ↔ IsNoetherian K (V ⧸ f.ker)

@[simp]

theorem LinearMap.ker_coFG_iff_hasFiniteRange {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] {f : V →ₗ[K] V₂} : f.ker.CoFG ↔ f.HasFiniteRange

theorem LinearMap.HasNoetherianRange.quotient_ker {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] {f : V →ₗ[K] V₂} : f.HasNoetherianRange → IsNoetherian K (V ⧸ f.ker)

Alias of the forward direction of LinearMap.hasNoetherianRange_iff_quotient_ker.

theorem LinearMap.HasFiniteRange.cofg_ker {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] {f : V →ₗ[K] V₂} : f.HasFiniteRange → f.ker.CoFG

Alias of the reverse direction of LinearMap.ker_coFG_iff_hasFiniteRange.

@[simp]

theorem LinearMap.HasNoetherianRange.smul {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] {f : V →ₗ[K] V₂} (hf : f.HasNoetherianRange) (c : K) : (c • f).HasNoetherianRange

@[simp]

theorem LinearMap.HasFiniteRange.smul {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] {f : V →ₗ[K] V₂} (hf : f.HasFiniteRange) (c : K) : (c • f).HasFiniteRange

def LinearMap.finiteRange (K : Type u_1) (V : Type u_2) (V₂ : Type u_4) [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] : Submodule K (V →ₗ[K] V₂)

LinearMap.finiteRange is the submodule of V →ₗ[K] W consisting of linear maps satisfying LinearMap.HasNoetherianRange. We allow ourself this slightly abusive name because the set of linear maps satisfying LinearMap.HasFiniteRange is only a submodule over a noetherian ring, in which case the two notions agree.

Equations

• LinearMap.finiteRange K V V₂ = { carrier := {u : V →ₗ[K] V₂ | u.HasNoetherianRange}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem LinearMap.mem_finiteRange_iff_hasNoetherianRange {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] {f : V →ₗ[K] V₂} : f ∈ finiteRange K V V₂ ↔ f.HasNoetherianRange

theorem LinearMap.mem_finiteRange_iff_hasFiniteRange {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [IsNoetherianRing K] {f : V →ₗ[K] V₂} : f ∈ finiteRange K V V₂ ↔ f.HasFiniteRange

@[implicit_reducible]

def LinearMap.FiniteRangeSetoid.setoid {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] : Setoid (V →ₗ[K] V₂)

This is the equivalence relation on linear maps such that u ≈ v precisely when u - v is a linear map with noetherian range. We allow ourself this slightly abusive name because the more natural definition (u - v has finitely generated range) only yields a well-behaved relation (more precisely, an additive congruence relation compatible with composition on both sides) over a noetherian ring, in which case the two notions agree.

This setoid is declared as an instance in scope LinearMap.FiniteRangeSetoid.

Equations

• LinearMap.FiniteRangeSetoid.setoid = (LinearMap.finiteRange K V V₂).quotientRel

theorem LinearMap.FiniteRangeSetoid.equiv_iff_hasNoetherianRange {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] {u v : V →ₗ[K] V₂} : u ≈ v ↔ (u - v).HasNoetherianRange

theorem LinearMap.FiniteRangeSetoid.equiv_iff_hasFiniteRange {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [IsNoetherianRing K] {u v : V →ₗ[K] V₂} : u ≈ v ↔ (u - v).HasFiniteRange

theorem LinearMap.FiniteRangeSetoid.equiv_zero_iff_hasNoetherianRange {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] {u : V →ₗ[K] V₂} : u ≈ 0 ↔ u.HasNoetherianRange

theorem LinearMap.FiniteRangeSetoid.equiv_zero_iff_hasFiniteRange {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [IsNoetherianRing K] {u : V →ₗ[K] V₂} : u ≈ 0 ↔ u.HasFiniteRange

theorem LinearMap.FiniteRangeSetoid.equiv_iff_isNoetherian_quotient_eqLocus {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] {u v : V →ₗ[K] V₂} : u ≈ v ↔ IsNoetherian K (V ⧸ u.eqLocus v)

theorem LinearMap.FiniteRangeSetoid.equiv_iff_eqLocus_coFG {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [IsNoetherianRing K] {u v : V →ₗ[K] V₂} : u ≈ v ↔ (u.eqLocus v).CoFG

theorem LinearMap.FiniteRangeSetoid.equiv_of_eqOn_of_isNoetherian {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] {u v : V →ₗ[K] V₂} (A : Submodule K V) [quot_A_noeth : IsNoetherian K (V ⧸ A)] (eqOn_A : Set.EqOn ⇑u ⇑v ↑A) : u ≈ v

theorem LinearMap.FiniteRangeSetoid.equiv_of_eqOn_coFG {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [IsNoetherianRing K] {u v : V →ₗ[K] V₂} {A : Submodule K V} (A_coFG : A.CoFG) (eqOn_A : Set.EqOn ⇑u ⇑v ↑A) : u ≈ v

theorem LinearMap.FiniteRangeSetoid.equiv_comp_right {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u : V →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃} (h' : v ≈ v') : v ∘ₗ u ≈ v' ∘ₗ u

theorem LinearMap.FiniteRangeSetoid.equiv_comp_left {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u v : V →ₗ[K] V₂} {u' : V₂ →ₗ[K] V₃} (h : u ≈ v) : u' ∘ₗ u ≈ u' ∘ₗ v

theorem LinearMap.FiniteRangeSetoid.equiv_comp {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u v : V →ₗ[K] V₂} {u' v' : V₂ →ₗ[K] V₃} (h : u ≈ v) (h' : u' ≈ v') : u' ∘ₗ u ≈ v' ∘ₗ v

theorem LinearMap.FiniteRangeSetoid.projection_equiv_zero_iff_isNoetherian {K : Type u_1} {V : Type u_2} [CommRing K] [AddCommGroup V] [Module K V] {S T : Submodule K V} (hST : IsCompl S T) : S.projection T hST ≈ 0 ↔ IsNoetherian K ↥S

theorem LinearMap.FiniteRangeSetoid.projection_equiv_zero {K : Type u_1} {V : Type u_2} [CommRing K] [AddCommGroup V] [Module K V] {S T : Submodule K V} [IsNoetherian K ↥S] (hST : IsCompl S T) : S.projection T hST ≈ 0

theorem LinearMap.FiniteRangeSetoid.projection_equiv_id_iff_isNoetherian {K : Type u_1} {V : Type u_2} [CommRing K] [AddCommGroup V] [Module K V] {S T : Submodule K V} (hST : IsCompl S T) : S.projection T hST ≈ id ↔ IsNoetherian K ↥T

theorem LinearMap.FiniteRangeSetoid.projection_equiv_id {K : Type u_1} {V : Type u_2} [CommRing K] [AddCommGroup V] [Module K V] {S T : Submodule K V} [IsNoetherian K ↥T] (hST : IsCompl S T) : S.projection T hST ≈ id

def LinearMap.IsLeftQuasiInverse {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] (u : V →ₗ[K] V₂) (v : V₂ →ₗ[K] V) : Prop

u is a left quasi-inverse to v if u ∘ₗ v ≈ id modulo linear maps with noetherian ranges. Recall that if the scalar ring is noetherian (e.g a field), then "noetherian range" can be replaced by "finitely generated range".

Equations

• u.IsLeftQuasiInverse v = (u ∘ₗ v ≈ LinearMap.id)

def LinearMap.IsRightQuasiInverse {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] (u : V₃ →ₗ[K] V₂) (v : V₂ →ₗ[K] V₃) : Prop

u is a right quasi-inverse to v if v ∘ₗ u ≈ id modulo linear maps with noetherian ranges. Recall that if the scalar ring is noetherian (e.g a field), then "noetherian range" can be replaced by "finitely generated range".

Equations

• u.IsRightQuasiInverse v = (v ∘ₗ u ≈ LinearMap.id)

def LinearMap.IsQuasiInverse {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] (u : V₃ →ₗ[K] V₂) (v : V₂ →ₗ[K] V₃) : Prop

u is a quasi-inverse to v if u ∘ₗ v ≈ id and v ∘ₗ u ≈ id modulo linear maps with noetherian ranges. Recall that if the scalar ring is noetherian (e.g a field), then "noetherian range" can be replaced by "finitely generated range".

Equations

• u.IsQuasiInverse v = (u.IsLeftQuasiInverse v ∧ u.IsRightQuasiInverse v)

theorem LinearMap.isLeftQuasiInverse_iff_isRightQuasiInverse_swap {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u : V₃ →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} : u.IsLeftQuasiInverse v ↔ v.IsRightQuasiInverse u

theorem LinearMap.IsLeftQuasiInverse.isRightQuasiInverse {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u : V₃ →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} : u.IsLeftQuasiInverse v → v.IsRightQuasiInverse u

Alias of the forward direction of LinearMap.isLeftQuasiInverse_iff_isRightQuasiInverse_swap.

theorem LinearMap.IsRightQuasiInverse.isLeftQuasiInverse {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u : V₃ →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} : v.IsRightQuasiInverse u → u.IsLeftQuasiInverse v

Alias of the reverse direction of LinearMap.isLeftQuasiInverse_iff_isRightQuasiInverse_swap.

theorem LinearMap.IsLeftQuasiInverse.equiv {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u : V₃ →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} (h : u.IsLeftQuasiInverse v) : u ∘ₗ v ≈ id

theorem LinearMap.IsRightQuasiInverse.equiv {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u : V₃ →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} (h : u.IsRightQuasiInverse v) : v ∘ₗ u ≈ id

theorem LinearMap.IsQuasiInverse.symm {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u : V₃ →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} (h : u.IsQuasiInverse v) : v.IsQuasiInverse u

theorem LinearMap.IsLeftQuasiInverse.congr {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u u' : V₃ →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃} (h : u.IsLeftQuasiInverse v) (hu : u' ≈ u) (hv : v' ≈ v) : u'.IsLeftQuasiInverse v'

theorem LinearMap.isLeftQuasiInverse_congr {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u u' : V₃ →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃} (hu : u' ≈ u) (hv : v' ≈ v) : u.IsLeftQuasiInverse v ↔ u'.IsLeftQuasiInverse v'

theorem LinearMap.IsRightQuasiInverse.congr {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u u' : V₃ →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃} (h : u.IsRightQuasiInverse v) (hu : u' ≈ u) (hv : v' ≈ v) : u'.IsRightQuasiInverse v'

theorem LinearMap.isRightQuasiInverse_congr {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u u' : V₃ →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃} (hu : u' ≈ u) (hv : v' ≈ v) : u.IsRightQuasiInverse v ↔ u'.IsRightQuasiInverse v'

theorem LinearMap.IsQuasiInverse.congr {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u u' : V₃ →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃} (h : u.IsQuasiInverse v) (hu : u' ≈ u) (hv : v' ≈ v) : u'.IsQuasiInverse v'

theorem LinearMap.isQuasiInverse_congr {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u u' : V₃ →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃} (hu : u' ≈ u) (hv : v' ≈ v) : u.IsQuasiInverse v ↔ u'.IsQuasiInverse v'

theorem LinearMap.IsQuasiInverse.equiv_of_left {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u u' : V₃ →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃} (h : u.IsQuasiInverse v) (h' : u'.IsQuasiInverse v') (hu : u ≈ u') : v ≈ v'

theorem LinearMap.IsQuasiInverse.equiv_of_right {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u u' : V₃ →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃} (h : u.IsQuasiInverse v) (h' : u'.IsQuasiInverse v') (hv : v ≈ v') : u ≈ u'

theorem LinearMap.IsLeftQuasiInverse.comp {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u : V →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} {u' : V₂ →ₗ[K] V} {v' : V₃ →ₗ[K] V₂} (hu : u'.IsLeftQuasiInverse u) (hv : v'.IsLeftQuasiInverse v) : (u' ∘ₗ v').IsLeftQuasiInverse (v ∘ₗ u)

Left quasi-inverses compose in the opposite order.

theorem LinearMap.IsRightQuasiInverse.comp {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u : V →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} {u' : V₂ →ₗ[K] V} {v' : V₃ →ₗ[K] V₂} (hu : u'.IsRightQuasiInverse u) (hv : v'.IsRightQuasiInverse v) : (u' ∘ₗ v').IsRightQuasiInverse (v ∘ₗ u)

Right quasi-inverses compose in the opposite order.

theorem LinearMap.IsQuasiInverse.comp {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u : V →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} {u' : V₂ →ₗ[K] V} {v' : V₃ →ₗ[K] V₂} (hu : u'.IsQuasiInverse u) (hv : v'.IsQuasiInverse v) : (u' ∘ₗ v').IsQuasiInverse (v ∘ₗ u)

Quasi-inverses compose in the opposite order.

theorem LinearMap.IsLeftQuasiInverse.of_comp_left {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u : V →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} {u' : V₂ →ₗ[K] V} {w : V₃ →ₗ[K] V} (hu : u'.IsRightQuasiInverse u) (hw : w.IsLeftQuasiInverse (v ∘ₗ u)) : (u ∘ₗ w).IsLeftQuasiInverse v

If u' is a right quasi-inverse of u and w is a left quasi-inverse of v ∘ₗ u, then u ∘ₗ w is a left quasi-inverse of v.

theorem LinearMap.IsQuasiInverse.of_comp_left {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u : V →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} {u' : V₂ →ₗ[K] V} {w : V₃ →ₗ[K] V} (hu : u'.IsQuasiInverse u) (hw : w.IsQuasiInverse (v ∘ₗ u)) : (u ∘ₗ w).IsQuasiInverse v

If u' is a quasi-inverse of u and w is a quasi-inverse of v ∘ₗ u, then u ∘ₗ w is a quasi-inverse of v.

theorem LinearMap.IsRightQuasiInverse.of_comp_right {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u : V →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} {v' : V₃ →ₗ[K] V₂} {w : V₃ →ₗ[K] V} (hv : v'.IsLeftQuasiInverse v) (hw : w.IsRightQuasiInverse (v ∘ₗ u)) : (w ∘ₗ v).IsRightQuasiInverse u

If v' is a left quasi-inverse of v and w is a right quasi-inverse of v ∘ₗ u, then w ∘ₗ v is a right quasi-inverse of u.

theorem LinearMap.IsQuasiInverse.of_comp_right {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] {u : V →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} {v' : V₃ →ₗ[K] V₂} {w : V₃ →ₗ[K] V} (hv : v'.IsQuasiInverse v) (hw : w.IsQuasiInverse (v ∘ₗ u)) : (w ∘ₗ v).IsQuasiInverse u

If v' is a quasi-inverse of v and w is a quasi-inverse of v ∘ₗ u, then w ∘ₗ v is a quasi-inverse of u.

theorem LinearMap.isQuasiInverse_subtype_projectionOnto_iff {K : Type u_1} {V : Type u_2} [CommRing K] [AddCommGroup V] [Module K V] {S T : Submodule K V} (hST : IsCompl S T) : S.subtype.IsQuasiInverse (S.projectionOnto T hST) ↔ IsNoetherian K ↥T

theorem LinearMap.isQuasiInverse_subtype_projectionOnto {K : Type u_1} {V : Type u_2} [CommRing K] [AddCommGroup V] [Module K V] {S T : Submodule K V} [IsNoetherian K ↥T] (hST : IsCompl S T) : S.subtype.IsQuasiInverse (S.projectionOnto T hST)