# Documentation

Mathlib.Algebra.Module.DedekindDomain

# Modules over a Dedekind domain #

Over a Dedekind domain, an I-torsion module is the internal direct sum of its p i ^ e i-torsion submodules, where I = ∏ i, p i ^ e i is its unique decomposition in prime ideals. Therefore, as any finitely generated torsion module is I-torsion for some I, it is an internal direct sum of its p i ^ e i-torsion submodules for some prime ideals p i and numbers e i.

theorem Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal {R : Type u} [] [] {M : Type v} [] [Module R M] [] {I : } (hI : I ) (hM : ) :

Over a Dedekind domain, an I-torsion module is the internal direct sum of its p i ^ e i- torsion submodules, where I = ∏ i, p i ^ e i is its unique decomposition in prime ideals.

theorem Submodule.isInternal_prime_power_torsion {R : Type u} [] [] {M : Type v} [] [Module R M] [] [] (hM : ) :

A finitely generated torsion module over a Dedekind domain is an internal direct sum of its p i ^ e i-torsion submodules where p i are factors of (⊤ : Submodule R M).annihilator and e i are their multiplicities.

theorem Submodule.exists_isInternal_prime_power_torsion {R : Type u} [] [] {M : Type v} [] [Module R M] [] [] (hM : ) :
P x x_1 e, DirectSum.IsInternal fun p => Submodule.torsionBySet R M ↑(p ^ e p)

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