# mathlibdocumentation

algebra.module.pid

# Structure of finitely generated modules over a PID #

## Main statements #

• module.equiv_direct_sum_of_is_torsion : 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_direct_sum : 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 a 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.is_internal_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.is_internal_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 linear_algebra/free_module/pid.lean.)

## Tags #

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

theorem submodule.is_internal_prime_power_torsion_of_pid {R : Type u} [comm_ring R] [is_domain R] {M : Type v} [ M] [ M] (hM : M) :
∃ (ι : Type u) [_inst_9 : fintype ι] [_inst_10 : (p : ι → R) (h : ∀ (i : ι), irreducible (p i)) (e : ι → ), direct_sum.is_internal (λ (i : ι), (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.torsion_of_eq_span_pow_p_order {R : Type u} [comm_ring R] [is_domain R] {M : Type v} [ M] {p : R} (hp : irreducible p) (hM : ) [dec : Π (x : M), decidable (x = 0)] (x : M) :
x = ideal.span {p ^ x}
theorem module.p_pow_smul_lift {R : Type u} [comm_ring R] [is_domain R] {M : Type v} [ M] {p : R} (hp : irreducible p) (hM : ) [dec : Π (x : M), decidable (x = 0)] {x y : M} {k : } (hM' : (p ^ y)) (h : p ^ k x {y}) :
∃ (a : R), p ^ k x = p ^ k a y
theorem module.exists_smul_eq_zero_and_mk_eq {R : Type u} [comm_ring R] [is_domain R] {M : Type v} [ M] {p : R} (hp : irreducible p) (hM : ) [dec : Π (x : M), decidable (x = 0)] {z : M} (hz : (p ^ z)) {k : } (f : R {p ^ k} →ₗ[R] M {z}) :
∃ (x : M), p ^ k x = 0
theorem module.torsion_by_prime_power_decomposition {R : Type u} [comm_ring R] [is_domain R] {N : Type (max u v)} [ N] {p : R} (hp : irreducible p) (hN : ) [h' : N] :
∃ (d : ) (k : fin d), nonempty (N ≃ₗ[R] direct_sum (fin d) (λ (i : fin d), 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_direct_sum_of_is_torsion {R : Type u} [comm_ring R] [is_domain R] {N : Type (max u v)} [ N] [h' : N] (hN : N) :
∃ (ι : Type u) [_inst_8 : fintype ι] (p : ι → R) (h : ∀ (i : ι), irreducible (p i)) (e : ι → ), nonempty (N ≃ₗ[R] (λ (i : ι), 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_direct_sum {R : Type u} [comm_ring R] [is_domain R] {N : Type (max u v)} [ N] [h' : N] :
∃ (n : ) (ι : Type u) [_inst_8 : fintype ι] (p : ι → R) (h : ∀ (i : ι), irreducible (p i)) (e : ι → ), nonempty (N ≃ₗ[R] (fin n →₀ R) × (λ (i : ι), 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.