Quotients of submodules

If F is the sum of disjoint submodules p and p', then the quotient of F by p' is linearly equivalent to p. The equivalence Submodule.quotientEquivOfEqSup specializes Mathlib's second isomorphism theorem LinearMap.quotientInfEquivSupQuotient, allowing the ambient submodule F to be identified by an equality. This applies, for example, when a successive filtration step splits into the preceding step and a homogeneous component.

Pulling back the span of a quotient class and then mapping it along a linear map gives the image of the quotient kernel plus the span of the image of a representative. This identifies the underlying submodule when lifting a cyclic submodule of a subquotient, for example an eigenline, into the ambient module.

A linear map φ : P → M induces an isomorphism from the quotient of P by the preimage of a submodule F onto the subquotient (F ⊔ range φ) ⧸ F; Submodule.quotientComapEquivSupQuotient generalizes the second isomorphism theorem, which is the case φ = p.subtype.

Two surjective linear maps with the same kernel identify their codomains, by the first isomorphism theorem; LinearMap.equivOfSurjectiveOfKerEq packages this equivalence.

If an ideal I annihilates S, every linear map M → S kills I • M, so maps out of M ⧸ I • M into S are the same as maps out of M; TauCeti.linearMapQuotientSMulTopEquiv packages this as an additive equivalence. For I = Ring.jacobson R it applies to every semisimple S, by IsSemisimpleModule.jacobson_le_annihilator.

noncomputable def Submodule.quotientEquivOfEqSup {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (F p p' : Submodule R M) (hF : F = p ⊔ p') (h : Disjoint p p') : (↥F ⧸ comap F.subtype p') ≃ₗ[R] ↥p

If F = p ⊔ p' and p and p' are disjoint, the quotient of F by p' is p.

@[simp]

theorem Submodule.quotientEquivOfEqSup_symm_apply {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (F p p' : Submodule R M) (hF : F = p ⊔ p') (h : Disjoint p p') (x : ↥p) : (F.quotientEquivOfEqSup p p' hF h).symm x = Quotient.mk ⟨↑x, ⋯⟩

The inverse equivalence sends an element of p to its quotient class in F.

@[simp]

theorem Submodule.quotientEquivOfEqSup_apply_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (F p p' : Submodule R M) (hF : F = p ⊔ p') (h : Disjoint p p') (y : ↥F) (hy : ↑y ∈ p) : (F.quotientEquivOfEqSup p p' hF h) (Quotient.mk y) = ⟨↑y, hy⟩

The equivalence sends the class of any representative lying in p to that representative.

theorem Submodule.quotientEquivOfEqSup_apply_mk_eq_zero_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (F p p' : Submodule R M) (hF : F = p ⊔ p') (h : Disjoint p p') (y : ↥F) : (F.quotientEquivOfEqSup p p' hF h) (Quotient.mk y) = 0 ↔ ↑y ∈ p'

A quotient representative has zero image exactly when it lies in the right summand.

theorem Submodule.quotientEquivOfEqSup_apply_mk_of_mem_right {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (F p p' : Submodule R M) (hF : F = p ⊔ p') (h : Disjoint p p') (y : ↥F) (hy : ↑y ∈ p') : (F.quotientEquivOfEqSup p p' hF h) (Quotient.mk y) = 0

The equivalence sends the class of any representative in the right summand to zero.

theorem Submodule.map_comap_mkQ_span_singleton {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] (S : Submodule R M) (f : M →ₗ[R] N) (v : M) : map f (comap S.mkQ (R ∙ S.mkQ v)) = map f S ⊔ R ∙ f v

Mapping the inverse image of the span of a quotient class gives the image of the quotient kernel plus the span of the image of a representative.

noncomputable def Submodule.quotientComapEquivSupQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {P : Type u_4} [AddCommGroup P] [Module R P] (F : Submodule R M) (φ : P →ₗ[R] M) : (P ⧸ comap φ F) ≃ₗ[R] ↥(F ⊔ φ.range) ⧸ F.submoduleOf (F ⊔ φ.range)

The map φ induces a linear isomorphism from the quotient of P by the preimage of F under φ onto the subquotient (F ⊔ range φ) ⧸ F. For φ = p.subtype this is the second isomorphism theorem LinearMap.quotientInfEquivSupQuotient.

@[simp]

theorem Submodule.quotientComapEquivSupQuotient_apply_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {P : Type u_4} [AddCommGroup P] [Module R P] (F : Submodule R M) (φ : P →ₗ[R] M) (c : P) : (F.quotientComapEquivSupQuotient φ) (Quotient.mk c) = Quotient.mk ⟨φ c, ⋯⟩

noncomputable def LinearMap.equivOfSurjectiveOfKerEq {R : Type u_1} {M : Type u_2} {N : Type u_3} {N' : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup N'] [Module R M] [Module R N] [Module R N'] (g : M →ₗ[R] N) (h : M →ₗ[R] N') (hg : Function.Surjective ⇑g) (hh : Function.Surjective ⇑h) (hk : g.ker = h.ker) : N ≃ₗ[R] N'

Two surjective linear maps with the same kernel identify their codomains, by the first isomorphism theorem.

@[simp]

theorem LinearMap.equivOfSurjectiveOfKerEq_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} {N' : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup N'] [Module R M] [Module R N] [Module R N'] (g : M →ₗ[R] N) (h : M →ₗ[R] N') (hg : Function.Surjective ⇑g) (hh : Function.Surjective ⇑h) (hk : g.ker = h.ker) (x : M) : (g.equivOfSurjectiveOfKerEq h hg hh hk) (g x) = h x

The equivalence sends the image of an element under the first map to its image under the second map.

@[simp]

theorem LinearMap.equivOfSurjectiveOfKerEq_symm_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} {N' : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup N'] [Module R M] [Module R N] [Module R N'] (g : M →ₗ[R] N) (h : M →ₗ[R] N') (hg : Function.Surjective ⇑g) (hh : Function.Surjective ⇑h) (hk : g.ker = h.ker) (x : M) : (g.equivOfSurjectiveOfKerEq h hg hh hk).symm (h x) = g x

The inverse equivalence sends the image of an element under the second map to its image under the first map.

def TauCeti.linearMapQuotientSMulTopEquiv {R : Type u_1} [Ring R] {I : Ideal R} (M : Type u_2) [AddCommGroup M] [Module R M] {S : Type u_3} [AddCommGroup S] [Module R S] (hI : I ≤ Module.annihilator R S) : (M ⧸ I • ⊤ →ₗ[R] S) ≃+ (M →ₗ[R] S)

Maps into a module annihilated by I factor through M ⧸ I • M. If the ideal I annihilates S, then composition with M → M ⧸ I • M identifies maps out of M ⧸ I • M with maps out of M; the identification is additive. For I = Ring.jacobson R this applies to every semisimple S by IsSemisimpleModule.jacobson_le_annihilator.

@[simp]

theorem TauCeti.linearMapQuotientSMulTopEquiv_apply {R : Type u_1} [Ring R] {I : Ideal R} (M : Type u_2) [AddCommGroup M] [Module R M] {S : Type u_3} [AddCommGroup S] [Module R S] (hI : I ≤ Module.annihilator R S) (g : M ⧸ I • ⊤ →ₗ[R] S) (x : M) : ((linearMapQuotientSMulTopEquiv M hI) g) x = g (Submodule.Quotient.mk x)

@[simp]

theorem TauCeti.linearMapQuotientSMulTopEquiv_symm_apply_mk {R : Type u_1} [Ring R] {I : Ideal R} (M : Type u_2) [AddCommGroup M] [Module R M] {S : Type u_3} [AddCommGroup S] [Module R S] (hI : I ≤ Module.annihilator R S) (f : M →ₗ[R] S) (x : M) : ((linearMapQuotientSMulTopEquiv M hI).symm f) (Submodule.Quotient.mk x) = f x