English
Every finitely generated torsion module over a Dedekind domain can be expressed as an internal direct sum of p^e torsion submodules with appropriate prime ideals p and exponents e.
Русский
Каждый конечнопорожденный torsion-модуль над областью Дедекнда может быть выражен как внутренний прямой сумма p^e-тorsion‑частей по подходящим простым идеалам p и степеням e.
LaTeX
$$$\exists P \; (\text{finite set of primes}) \; \forall p \in P, \text{Prime}(p) ∧ e(p) \in \mathbb{N}, \; DirectSum.IsInternal (p \mapsto \mathrm{torsionBySet}(R,M,p^{e(p)}))$$$
Lean4
/-- 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`. -/
theorem exists_isInternal_prime_power_torsion [Module.Finite R M] (hM : Module.IsTorsion R M) :
∃ (P : Finset <| Ideal R) (_ : DecidableEq P) (_ : ∀ p ∈ P, Prime p) (e : P → ℕ),
DirectSum.IsInternal fun p : P => torsionBySet R M (p ^ e p : Ideal R) :=
by
classical
exact ⟨_, _, fun p hp => prime_of_factor p (Multiset.mem_toFinset.mp hp), _, isInternal_prime_power_torsion hM⟩
