English
A finitely generated module M over a PID is isomorphic to the direct product of a free module of finite rank and a direct sum of torsion components: M ≅ R^n ⊕ ⊕_i R/(p_i^{e_i}).
Русский
Конечнопорожденный модуль над ПИД изоморфен прямому произведению свободного модуля и прямой суммы torsion-компонент: M ≅ R^n ⊕ ⊕_i R/(p_i^{e_i}).
LaTeX
$$$\\exists n,\\iota,\\text{finite},\\ p:\\iota \\to R,\\ (\\forall i, Irreducible (p i)),\\ e: \\iota \\to \\mathbb{N},\\ Nonempty\\ (M \\cong_ℓ[R] (\\text{Fin } n \\to_0 R) \\times \\bigoplus_{i:\\iota} R \\ / \\ R \\cdot p i^{e i})$$$
Lean4
/-- **Structure theorem of finitely generated modules over a PID** : A finitely generated
module over a PID is isomorphic to the product of a free module and a direct sum of some
`R ⧸ R ∙ (p i ^ e i)` where the `p i ^ e i` are prime powers. -/
theorem equiv_free_prod_directSum [h' : Module.Finite R M] :
∃ (n : ℕ) (ι : Type u) (_ : Fintype ι) (p : ι → R) (_ : ∀ i, Irreducible <| p i) (e : ι → ℕ),
Nonempty <| M ≃ₗ[R] (Fin n →₀ R) × ⨁ i : ι, R ⧸ R ∙ p i ^ e i :=
by
obtain ⟨I, fI, p, hp, e, ⟨h⟩⟩ := equiv_directSum_of_isTorsion.{u, v} (@torsion_isTorsion R M _ _ _)
obtain ⟨n, ⟨g⟩⟩ := @Module.basisOfFiniteTypeTorsionFree' R _ (M ⧸ torsion R M) _ _ _ _ _ _
obtain ⟨f, hf⟩ := Module.projective_lifting_property _ LinearMap.id (torsion R M).mkQ_surjective
refine
⟨n, I, fI, p, hp, e,
⟨(lequivProdOfRightSplitExact (torsion R M).injective_subtype ?_ hf).symm.trans <|
(h.prodCongr g).trans <| LinearEquiv.prodComm.{u, u} R _ (Fin n →₀ R)⟩⟩
rw [range_subtype, ker_mkQ]
