Quotient of submodules of full rank in free finite modules over PIDs

Main results

• Submodule.quotientEquivPiSpan: M ⧸ N, if M is free finite module over a PID R and N is a submodule of full rank, can be written as a product of quotients of R by principal ideals.

noncomputable def Submodule.quotientEquivPiSpan {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [IsDomain R] [IsPrincipalIdealRing R] [Finite ι] (N : Submodule R M) (b : Module.Basis ι R M) (h : Module.finrank R ↥N = Module.finrank R M) : (M ⧸ N) ≃ₗ[R] (i : ι) → R ⧸ Ideal.span {smithNormalFormCoeffs b h i}

We can write the quotient by a submodule of full rank over a PID as a product of quotients by principal ideals.

Equations

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

noncomputable def Submodule.quotientEquivPiZMod {ι : Type u_1} {M : Type u_3} [AddCommGroup M] [Finite ι] (N : Submodule ℤ M) (b : Module.Basis ι ℤ M) (h : Module.finrank ℤ ↥N = Module.finrank ℤ M) : M ⧸ N ≃+ ((i : ι) → ZMod (smithNormalFormCoeffs b h i).natAbs)

Quotients by submodules of full rank of free finite ℤ-modules are isomorphic to a direct product of ZMod.

Equations

• N.quotientEquivPiZMod b h = (↑(N.quotientEquivPiSpan b h)).trans (AddEquiv.piCongrRight fun (i : ι) => ↑(Submodule.smithNormalFormCoeffs b h i).quotientSpanEquivZMod)

theorem Submodule.finiteQuotientOfFreeOfRankEq {M : Type u_3} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (N : Submodule ℤ M) (h : Module.finrank ℤ ↥N = Module.finrank ℤ M) : Finite (M ⧸ N)

A submodule of full rank of a free finite ℤ-module has a finite quotient. It can't be an instance because of the side condition Module.finrank ℤ N = Module.finrank ℤ M.

theorem Submodule.finiteQuotient_iff {M : Type u_3} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (N : Submodule ℤ M) : Finite (M ⧸ N) ↔ Module.finrank ℤ ↥N = Module.finrank ℤ M

noncomputable def Submodule.quotientEquivDirectSum {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [IsDomain R] [IsPrincipalIdealRing R] [Finite ι] (F : Type u_4) [CommRing F] [Algebra F R] [Module F M] [IsScalarTower F R M] (b : Module.Basis ι R M) {N : Submodule R M} (h : Module.finrank R ↥N = Module.finrank R M) : (M ⧸ N) ≃ₗ[F] DirectSum ι fun (i : ι) => R ⧸ Ideal.span {smithNormalFormCoeffs b h i}

Decompose M⧸N as a direct sum of cyclic R-modules (quotients by the ideals generated by Smith coefficients of N).

Equations

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

theorem Submodule.finrank_quotient_eq_sum {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [IsDomain R] [IsPrincipalIdealRing R] (F : Type u_4) [CommRing F] [Algebra F R] [Module F M] [IsScalarTower F R M] {N : Submodule R M} {ι : Type u_5} [Fintype ι] (b : Module.Basis ι R M) [Nontrivial F] (h : Module.finrank R ↥N = Module.finrank R M) [∀ (i : ι), Module.Free F (R ⧸ Ideal.span {smithNormalFormCoeffs b h i})] [∀ (i : ι), Module.Finite F (R ⧸ Ideal.span {smithNormalFormCoeffs b h i})] : Module.finrank F (M ⧸ N) = ∑ i : ι, Module.finrank F (R ⧸ Ideal.span {smithNormalFormCoeffs b h i})