English
For a PID and a finitely generated M, there exist an index type ι, a finite structure on ι, a family of irreducibles p_i and exponents e_i such that the torsionBy components p_i^{e_i} form an internal direct sum decomposition of M.
Русский
Для ПИД и конечнопорожденного M существует индексный множество ι, конечная запись, семейство ирредуцируемых p_i и степеней e_i так, что соответствующие компоненты p_i^{e_i} образуют внутреннее разложение M в виде прямого суммы.
LaTeX
$$$\\exists (I: Type), (\\text{Fintype } I), (p : I \\to R), (\\forall i, Irreducible (p i)), (e : I \\to \\mathbb{N}),\\ DirectSum.IsInternal (\\lambda i: I,\\; \\mathrm{torsionBy}\\ R\\ M\\ (p i)^{e i})$$$
Lean4
/-- A finitely generated torsion module over a PID is an internal direct sum of its
`p i ^ e i`-torsion submodules for some primes `p i` and numbers `e i`. -/
theorem exists_isInternal_prime_power_torsion_of_pid [Module.Finite R M] (hM : Module.IsTorsion R M) :
∃ (ι : Type u) (_ : Fintype ι) (_ : DecidableEq ι) (p : ι → R) (_ : ∀ i, Irreducible <| p i) (e : ι → ℕ),
DirectSum.IsInternal fun i => torsionBy R M <| p i ^ e i :=
by
classical
refine ⟨_, ?_, _, _, ?_, _, Submodule.isInternal_prime_power_torsion_of_pid hM⟩
· exact Finset.fintypeCoeSort _
· rintro ⟨p, hp⟩
have hP := prime_of_factor p (Multiset.mem_toFinset.mp hp)
haveI := Ideal.isPrime_of_prime hP
exact (IsPrincipal.prime_generator_of_isPrime p hP.ne_zero).irreducible
