Submodule intervals and quotients

This file records the generic order correspondence between a submodule interval and submodules of the associated quotient, and the identifications of subquotients ↥B ⧸ A that a linear map induces when it is injective or surjective.

Main declarations

• TauCeti.mapIic_symm_apply: the inverse of Submodule.mapIic takes inverse images along the inclusion.
• TauCeti.iccOrderIsoQuotientOfMapEq: the interval/quotient correspondence for a specified copy of the lower endpoint inside the upper endpoint.
• TauCeti.mapSubquotientEquivOfInjective: an injective linear map identifies the subquotient of the images of two submodules with the subquotient of the two submodules themselves.
• TauCeti.comapSubquotientEquivOfSurjective: a surjective linear map identifies the subquotient of the preimages of two submodules with the subquotient of the two submodules themselves.
• LinearMap.quotientEquivRangeQuotientMap: a linear map whose kernel lies below a submodule identifies the quotient by that submodule with the corresponding quotient of its range, and LinearMap.ker_mkQ_comp_rangeRestrict is the kernel computation behind it.
• Submodule.quotientEquivPiZModOfBasis: a quotient by a submodule with a specified diagonal basis is a product of cyclic groups with the specified diagonal orders.

References

The diagonal quotient construction follows Mathlib's Submodule.quotientEquivPiSpan and Submodule.quotientEquivPiZMod, with the bases and diagonal coefficients made explicit so an externally normalized Smith form can be retained.

noncomputable def Submodule.subquotientEquivOfEq {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (A B A' B' : Submodule R M) (hA : A = A') (hB : B = B') : (↥B ⧸ comap B.subtype A) ≃ₗ[R] ↥B' ⧸ comap B'.subtype A'

Transport a subquotient across equalities of its ambient and denominator submodules.

Equations

• A.subquotientEquivOfEq B A' B' hA hB = hA ▸ hB ▸ LinearEquiv.refl R (↥B ⧸ Submodule.comap B.subtype A)

@[simp]

theorem Submodule.subquotientEquivOfEq_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (A B A' B' : Submodule R M) (hA : A = A') (hB : B = B') (x : ↥B) : (A.subquotientEquivOfEq B A' B' hA hB) (Quotient.mk x) = Quotient.mk (have this := ⟨↑x, ⋯⟩; this)

Forward transport preserves the ambient representative.

@[simp]

theorem Submodule.subquotientEquivOfEq_symm_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (A B A' B' : Submodule R M) (hA : A = A') (hB : B = B') (x : ↥B') : (A.subquotientEquivOfEq B A' B' hA hB).symm (Quotient.mk x) = Quotient.mk (have this := ⟨↑x, ⋯⟩; this)

The inverse transport takes quotient representatives to the same ambient vector.

@[simp]

theorem TauCeti.mapIic_symm_apply {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (N : ↑(Set.Iic p)) : p.mapIic.symm N = Submodule.comap p.subtype ↑N

The inverse of Submodule.mapIic takes the inverse image along the inclusion. This is the symm-side counterpart of Mathlib's Submodule.coe_mapIic_apply.

def TauCeti.iccOrderIsoQuotientOfMapEq {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p q : Submodule R M} (r : Submodule R ↥q) (hr : Submodule.map q.subtype r = p) : ↑(Set.Icc p q) ≃o Submodule R (↥q ⧸ r)

The interval correspondence for a specified copy r of the lower endpoint inside q.

Equations

• TauCeti.iccOrderIsoQuotientOfMapEq r hr = (TauCeti.iciSubmoduleOrderIsoIcc✝ r hr).symm.trans r.comapMkQRelIso.symm

@[simp]

theorem TauCeti.mk_mem_iccOrderIsoQuotientOfMapEq_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p q : Submodule R M} (r : Submodule R ↥q) (hr : Submodule.map q.subtype r = p) (N : ↑(Set.Icc p q)) (x : ↥q) : Submodule.Quotient.mk x ∈ (iccOrderIsoQuotientOfMapEq r hr) N ↔ ↑x ∈ ↑N

A representative belongs to the quotient submodule in the interval correspondence exactly when its underlying ambient element belongs to the corresponding interval submodule.

@[simp]

theorem TauCeti.mem_iccOrderIsoQuotientOfMapEq_symm_apply_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p q : Submodule R M} (r : Submodule R ↥q) (hr : Submodule.map q.subtype r = p) (Q : Submodule R (↥q ⧸ r)) (x : ↥q) : ↑x ∈ ↑((iccOrderIsoQuotientOfMapEq r hr).symm Q) ↔ Submodule.Quotient.mk x ∈ Q

An ambient representative belongs to the interval submodule corresponding to Q exactly when its quotient class belongs to Q.

@[simp]

theorem TauCeti.map_equivMapOfInjective_comap_subtype {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Injective ⇑f) (A B : Submodule R M) : Submodule.map (↑(Submodule.equivMapOfInjective f hf B)) (Submodule.comap B.subtype A) = Submodule.comap (Submodule.map f B).subtype (Submodule.map f A)

An injective linear map carries the trace of A in B onto the trace of A.map f in B.map f, so it descends to the subquotients.

noncomputable def TauCeti.mapSubquotientEquivOfInjective {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Injective ⇑f) (A B : Submodule R M) : (↥(Submodule.map f B) ⧸ Submodule.comap (Submodule.map f B).subtype (Submodule.map f A)) ≃ₗ[R] ↥B ⧸ Submodule.comap B.subtype A

An injective linear map identifies subquotients. For arbitrary submodules A, B of M the subquotient cut out by the images A.map f, B.map f is the subquotient cut out by A and B themselves; for A ≤ B this reads B.map f ⧸ A.map f ≃ₗ[R] B ⧸ A.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.mapSubquotientEquivOfInjective_symm_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Injective ⇑f) (A B : Submodule R M) (x : ↥B) : (mapSubquotientEquivOfInjective f hf A B).symm (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((Submodule.equivMapOfInjective f hf B) x)

TauCeti.mapSubquotientEquivOfInjective read on representatives: its inverse is induced by the restriction Submodule.equivMapOfInjective of f to B.

@[simp]

theorem TauCeti.mapSubquotientEquivOfInjective_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Injective ⇑f) (A B : Submodule R M) (x : ↥B) : (mapSubquotientEquivOfInjective f hf A B) (Submodule.Quotient.mk ((Submodule.equivMapOfInjective f hf B) x)) = Submodule.Quotient.mk x

TauCeti.mapSubquotientEquivOfInjective read on representatives, in the forward direction: it undoes the restriction Submodule.equivMapOfInjective of f to B.

theorem TauCeti.ker_mkQ_comp_submoduleComap {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (A B : Submodule R N) : ((Submodule.comap B.subtype A).mkQ ∘ₗ f.submoduleComap B).ker = Submodule.comap (Submodule.comap f B).subtype (Submodule.comap f A)

The kernel of x ↦ f x mod A, on the preimage of B, is the trace of the preimage of A.

noncomputable def TauCeti.comapSubquotientEquivOfSurjective {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) (A B : Submodule R N) : (↥(Submodule.comap f B) ⧸ Submodule.comap (Submodule.comap f B).subtype (Submodule.comap f A)) ≃ₗ[R] ↥B ⧸ Submodule.comap B.subtype A

A surjective linear map identifies subquotients. For arbitrary submodules A, B of N the subquotient cut out by the preimages A.comap f, B.comap f is the subquotient cut out by A and B themselves; for A ≤ B this reads B.comap f ⧸ A.comap f ≃ₗ[R] B ⧸ A.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.comapSubquotientEquivOfSurjective_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) (A B : Submodule R N) (x : ↥(Submodule.comap f B)) : (comapSubquotientEquivOfSurjective f hf A B) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((f.submoduleComap B) x)

TauCeti.comapSubquotientEquivOfSurjective read on representatives: it is induced by the restriction LinearMap.submoduleComap of f to the preimage of B.

@[simp]

theorem TauCeti.comapSubquotientEquivOfSurjective_symm_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) (A B : Submodule R N) (x : ↥(Submodule.comap f B)) : (comapSubquotientEquivOfSurjective f hf A B).symm (Submodule.Quotient.mk ((f.submoduleComap B) x)) = Submodule.Quotient.mk x

TauCeti.comapSubquotientEquivOfSurjective read on representatives, in the inverse direction: it undoes the restriction LinearMap.submoduleComap of f to the preimage of B.

theorem LinearMap.ker_mkQ_comp_rangeRestrict {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (I : Submodule R M) (hker : f.ker ≤ I) : ((Submodule.map f.rangeRestrict I).mkQ ∘ₗ f.rangeRestrict).ker = I

The kernel of the map from M to the quotient of the range of f by the image of I is exactly I, provided that I contains the kernel of f.

noncomputable def LinearMap.quotientEquivRangeQuotientMap {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (I : Submodule R M) (hker : f.ker ≤ I) : (M ⧸ I) ≃ₗ[R] ↥f.range ⧸ Submodule.map f.rangeRestrict I

A quotient above the kernel is the corresponding quotient of the range.

If ker f ≤ I, the map x ↦ f x identifies M / I with the range of f modulo the image of I. This form of the first isomorphism theorem is useful when f is a representation with a controlled kernel.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearMap.quotientEquivRangeQuotientMap_apply_mk {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (I : Submodule R M) (hker : f.ker ≤ I) (x : M) : (f.quotientEquivRangeQuotientMap I hker) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (f.rangeRestrict x)

LinearMap.quotientEquivRangeQuotientMap sends the class of x to the class of f x in the range quotient.

@[simp]

theorem LinearMap.quotientEquivRangeQuotientMap_symm_apply_mk {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (I : Submodule R M) (hker : f.ker ≤ I) (x : M) : (f.quotientEquivRangeQuotientMap I hker).symm (Submodule.Quotient.mk (f.rangeRestrict x)) = Submodule.Quotient.mk x

LinearMap.quotientEquivRangeQuotientMap read in the inverse direction: the class of f.rangeRestrict x in the range quotient comes from the class of x.

noncomputable def Submodule.quotientEquivPiZModOfBasis {M : Type u_1} {ι : Type u_2} [AddCommGroup M] [Finite ι] (N : Submodule ℤ M) (b : Module.Basis ι ℤ M) (bN : Module.Basis ι ℤ ↥N) (a : ι → ℤ) (hdiag : ∀ (i : ι), ↑(bN i) = a i • b i) : M ⧸ N ≃+ ((i : ι) → ZMod (a i).natAbs)

A quotient by a submodule with a specified diagonal basis is a product of cyclic groups.

Unlike Submodule.quotientEquivPiZMod, this construction takes both bases and their diagonal coefficients as input. This lets a caller retain a normalized choice of Smith invariant factors rather than using the coefficients selected internally by Mathlib's basis-level Smith form.

Equations

• N.quotientEquivPiZModOfBasis b bN a hdiag = (TauCeti.coordinateQuotientEquiv✝ N b bN a hdiag).trans (TauCeti.quotientPiZModEquiv✝ a)

@[simp]

theorem Submodule.quotientEquivPiZModOfBasis_mk_apply {M : Type u_1} {ι : Type u_2} [AddCommGroup M] [Finite ι] (N : Submodule ℤ M) (b : Module.Basis ι ℤ M) (bN : Module.Basis ι ℤ ↥N) (a : ι → ℤ) (hdiag : ∀ (i : ι), ↑(bN i) = a i • b i) (x : M) (i : ι) : (N.quotientEquivPiZModOfBasis b bN a hdiag) (Quotient.mk x) i = ↑((b.repr x) i)

The diagonal quotient equivalence sends a representative to its coordinates modulo the corresponding diagonal coefficients.