# 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.isSemisimple_torsionBy_of_irreducible {R : Type u} [] {M : Type v} [] [Module R M] {a : R} (h : ) :
IsSemisimpleModule R { x : M // x }
theorem Submodule.isInternal_prime_power_torsion_of_pid {R : Type u} [] {M : Type v} [] [Module R M] [] [DecidableEq (Ideal R)] [] (hM : ) :

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} [] {M : Type v} [] [Module R M] [] [] (hM : ) :
∃ (ι : Type u) (x : ) (x : ) (p : ιR) (_ : ∀ (i : ι), Irreducible (p i)) (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} [] {M : Type v} [] [Module R M] [] {p : R} (hp : ) (hM : Module.IsTorsion' M { x : R // }) [dec : (x : M) → Decidable (x = 0)] (x : M) :
= Ideal.span {p ^ }
theorem Module.p_pow_smul_lift {R : Type u} [] {M : Type v} [] [Module R M] [] {p : R} (hp : ) (hM : Module.IsTorsion' M { x : R // }) [dec : (x : M) → Decidable (x = 0)] {x : M} {y : M} {k : } (hM' : Module.IsTorsionBy R M (p ^ )) (h : p ^ k x Submodule.span R {y}) :
∃ (a : R), p ^ k x = p ^ k a y
theorem Module.exists_smul_eq_zero_and_mk_eq {R : Type u} [] {M : Type v} [] [Module R M] [] {p : R} (hp : ) (hM : Module.IsTorsion' M { x : R // }) [dec : (x : M) → Decidable (x = 0)] {z : M} (hz : Module.IsTorsionBy R M (p ^ )) {k : } (f : R Submodule.span R {p ^ k} →ₗ[R] M Submodule.span R {z}) :
∃ (x : M), p ^ k x = 0
theorem Module.torsion_by_prime_power_decomposition {R : Type u} [] {N : Type (max u v)} [] [Module R N] [] {p : R} (hp : ) (hN : Module.IsTorsion' N { x : R // }) [h' : ] :
∃ (d : ) (k : Fin d), Nonempty (N ≃ₗ[R] DirectSum (Fin d) fun (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} [] {N : Type (max u v)} [] [Module R N] [] [h' : ] (hN : ) :
∃ (ι : Type u) (x : ) (p : ιR) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι), Nonempty (N ≃ₗ[R] DirectSum ι fun (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} [] {N : Type (max u v)} [] [Module R N] [] [h' : ] :
∃ (n : ) (ι : Type u) (x : ) (p : ιR) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι), Nonempty (N ≃ₗ[R] (Fin n →₀ R) × DirectSum ι fun (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.