# mathlibdocumentation

algebra.module.dedekind_domain

# Modules over a Dedekind domain #

Over a Dedekind domain, a 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.is_internal_prime_power_torsion_of_is_torsion_by_ideal {R : Type u} [comm_ring R] [is_domain R] {M : Type v} [ M] {I : ideal R} (hI : I ) (hM : I) :
∃ (P : finset (ideal R)) [_inst_6 : [_inst_7 : ∀ (p : ideal R), p Pprime p] (e : P → ), direct_sum.is_internal (λ (p : P), (p ^ e p))

Over a Dedekind domain, a 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.is_internal_prime_power_torsion {R : Type u} [comm_ring R] [is_domain R] {M : Type v} [ M] [ M] (hM : M) :
∃ (P : finset (ideal R)) [_inst_7 : [_inst_8 : ∀ (p : ideal R), p Pprime p] (e : P → ), direct_sum.is_internal (λ (p : P), (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.