# Documentation

Mathlib.Algebra.Module.PID

# 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} [] [] {M : Type v} [] [Module R M] [] (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 : ) :
ι 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} [] [] {M : Type v} [] [Module R M] {p : R} (hp : ) (hM : Module.IsTorsion' M { x // }) [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 // }) [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, 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 // }) [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, p ^ k x = 0 = f 1
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 // }) [h' : ] :
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} [] [] {N : Type (max u v)} [] [Module R N] [h' : ] (hN : ) :
ι 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} [] [] {N : Type (max u v)} [] [Module R N] [h' : ] :
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.