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}
[add_comm_group M]
[module R M]
[is_dedekind_domain R]
{I : ideal R}
(hI : I ≠ ⊥)
(hM : module.is_torsion_by_set R M ↑I) :
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}
[add_comm_group M]
[module R M]
[is_dedekind_domain R]
[module.finite R M]
(hM : module.is_torsion R M) :
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.