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} [CommRing R] [IsDomain R] {M : Type v} [AddCommGroup M] [Module R M] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ ⊥) (hM : Module.IsTorsionBySet R M ↑I) : DirectSum.IsInternal fun (p : { x : Ideal R // x ∈ (UniqueFactorizationMonoid.factors I).toFinset }) => Submodule.torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (UniqueFactorizationMonoid.factors I))

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} [CommRing R] [IsDomain R] {M : Type v} [AddCommGroup M] [Module R M] [IsDedekindDomain R] [Module.Finite R M] (hM : Module.IsTorsion R M) : DirectSum.IsInternal fun (p : { x : Ideal R // x ∈ (UniqueFactorizationMonoid.factors ⊤.annihilator).toFinset }) => Submodule.torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (UniqueFactorizationMonoid.factors ⊤.annihilator))

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} [CommRing R] [IsDomain R] {M : Type v} [AddCommGroup M] [Module R M] [IsDedekindDomain R] [Module.Finite R M] (hM : Module.IsTorsion R M) : ∃ (P : Finset (Ideal R)) (x : DecidableEq { x : Ideal R // x ∈ P }) (_ : ∀ p ∈ P, Prime p) (e : { x : Ideal R // x ∈ P } → ℕ), DirectSum.IsInternal fun (p : { x : Ideal R // x ∈ 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.