Structure of finitely generated modules over a PID

Main statements

• Module.equiv_directSum_of_isTorsion : A finitely generated torsion module over a PID is isomorphic to a direct sum of some R ⧸ R ∙ (p i ^ e i) where the p i ^ e i are prime powers.
• Module.equiv_free_prod_directSum : A finitely generated module over a PID is isomorphic to the product of a free module (its torsion free part) and a direct sum of the form above (its torsion submodule).

Notation

• R is a PID and M is a (finitely generated for main statements) R-module, with additional torsion hypotheses in the intermediate lemmas.
• N is an R-module lying over a higher type universe than R. This assumption is needed on the final statement for technical reasons.
• p is an irreducible element of R or a tuple of these.

Implementation details

We first prove (Submodule.isInternal_prime_power_torsion_of_pid) that a finitely generated torsion module is the internal direct sum of its p i ^ e i-torsion submodules for some (finitely many) prime powers p i ^ e i. This is proved in more generality for a Dedekind domain at Submodule.isInternal_prime_power_torsion.

Then we treat the case of a p ^ ∞-torsion module (that is, a module where all elements are cancelled by scalar multiplication by some power of p) and apply it to the p i ^ e i-torsion submodules (that are p i ^ ∞-torsion) to get the result for torsion modules.

Then we get the general result using that a torsion free module is free (which has been proved at Module.free_of_finite_type_torsion_free' at LinearAlgebra.FreeModule.PID.)

Tags

Finitely generated module, principal ideal domain, classification, structure theorem

theorem Submodule.isInternal_prime_power_torsion_of_pid {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] (hM : Module.IsTorsion R M) : DirectSum.IsInternal fun p => Submodule.torsionBy R M (Submodule.IsPrincipal.generator ↑p ^ Multiset.count (↑p) (UniqueFactorizationMonoid.factors (Submodule.annihilator ⊤)))

A finitely generated torsion module over a PID is an internal direct sum of its p i ^ e i-torsion submodules for some primes p i and numbers e i.

theorem Submodule.exists_isInternal_prime_power_torsion_of_pid {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] (hM : Module.IsTorsion R M) : ∃ ι x x p x_1 e, DirectSum.IsInternal fun i => Submodule.torsionBy R M (p i ^ e i)

A finitely generated torsion module over a PID is an internal direct sum of its p i ^ e i-torsion submodules for some primes p i and numbers e i.

theorem Ideal.torsionOf_eq_span_pow_pOrder {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type v} [AddCommGroup M] [Module R M] {p : R} (hp : Irreducible p) (hM : Module.IsTorsion' M { x // x ∈ Submonoid.powers p }) [dec : (x : M) → Decidable (x = 0)] (x : M) : Ideal.torsionOf R M x = Ideal.span {p ^ Submodule.pOrder hM x}

theorem Module.p_pow_smul_lift {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type v} [AddCommGroup M] [Module R M] {p : R} (hp : Irreducible p) (hM : Module.IsTorsion' M { x // x ∈ Submonoid.powers p }) [dec : (x : M) → Decidable (x = 0)] {x : M} {y : M} {k : ℕ} (hM' : Module.IsTorsionBy R M (p ^ Submodule.pOrder hM y)) (h : p ^ k • x ∈ Submodule.span R {y}) : ∃ a, p ^ k • x = p ^ k • a • y

theorem Module.exists_smul_eq_zero_and_mk_eq {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type v} [AddCommGroup M] [Module R M] {p : R} (hp : Irreducible p) (hM : Module.IsTorsion' M { x // x ∈ Submonoid.powers p }) [dec : (x : M) → Decidable (x = 0)] {z : M} (hz : Module.IsTorsionBy R M (p ^ Submodule.pOrder hM z)) {k : ℕ} (f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}) : ∃ x, p ^ k • x = 0 ∧ Submodule.Quotient.mk x = ↑f 1

theorem Module.torsion_by_prime_power_decomposition {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {N : Type (max u v)} [AddCommGroup N] [Module R N] {p : R} (hp : Irreducible p) (hN : Module.IsTorsion' N { x // x ∈ Submonoid.powers p }) [h' : Module.Finite R N] : ∃ d k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i})

A finitely generated p ^ ∞-torsion module over a PID is isomorphic to a direct sum of some R ⧸ R ∙ (p ^ e i) for some e i.

theorem Module.equiv_directSum_of_isTorsion {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {N : Type (max u v)} [AddCommGroup N] [Module R N] [h' : Module.Finite R N] (hN : Module.IsTorsion R N) : ∃ ι x p x e, Nonempty (N ≃ₗ[R] ⨁ (i : ι), R ⧸ Submodule.span R {p i ^ e i})

A finitely generated torsion module over a PID is isomorphic to a direct sum of some R ⧸ R ∙ (p i ^ e i) where the p i ^ e i are prime powers.

theorem Module.equiv_free_prod_directSum {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {N : Type (max u v)} [AddCommGroup N] [Module R N] [h' : Module.Finite R N] : ∃ n ι x p x e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ Submodule.span R {p i ^ e i})

Structure theorem of finitely generated modules over a PID : A finitely generated module over a PID is isomorphic to the product of a free module and a direct sum of some R ⧸ R ∙ (p i ^ e i) where the p i ^ e i are prime powers.