English
A finitely generated torsion module over a PID is isomorphic to a direct sum of prime power torsion components; i.e., there exists an index set ι, a family of irreducible p_i and exponents e_i such that M ≅ ⊕_i R/(p_i^{e_i}).
Русский
Конечнопорожденный torsion-модуль над ПИД изоморфен прямой сумме компонент p_i^{e_i}.
LaTeX
$$$\\exists ι (\\text{Fintype } ι) (p : ι \\to R) (\\forall i, Irreducible (p i)) (e : ι \\to \\mathbb{N}),\\ Nonempty\\ (M \\cong_ℓ[R] ⨁ i : ι, R \\! / \\! R \\cdot p i^{e i})$$$
Lean4
/-- A finitely generated torsion module over a PID is isomorphic to a direct sum of some
`R ⧸ R ∙ (p i ^ e i)` where the `p i ^ e i` are prime powers. -/
theorem equiv_directSum_of_isTorsion [h' : Module.Finite R M] (hM : Module.IsTorsion R M) :
∃ (ι : Type u) (_ : Fintype ι) (p : ι → R) (_ : ∀ i, Irreducible <| p i) (e : ι → ℕ),
Nonempty <| M ≃ₗ[R] ⨁ i : ι, R ⧸ R ∙ p i ^ e i :=
by
obtain ⟨I, fI, _, p, hp, e, h⟩ := Submodule.exists_isInternal_prime_power_torsion_of_pid hM
have : ∀ i, ∃ (d : ℕ) (k : Fin d → ℕ), Nonempty <| torsionBy R M (p i ^ e i) ≃ₗ[R] ⨁ j, R ⧸ R ∙ p i ^ k j := by
exact fun i =>
torsion_by_prime_power_decomposition.{u, v} (hp i)
((isTorsion'_powers_iff <| p i).mpr fun x => ⟨e i, smul_torsionBy _ _⟩)
classical
refine
⟨Σ i, Fin (this i).choose, inferInstance, fun ⟨i, _⟩ => p i, fun ⟨i, _⟩ => hp i, fun ⟨i, j⟩ =>
(this i).choose_spec.choose j,
⟨(LinearEquiv.ofBijective (DirectSum.coeLinearMap _) h).symm.trans <|
(DFinsupp.mapRange.linearEquiv fun i => (this i).choose_spec.choose_spec.some).trans <|
(DirectSum.sigmaLcurryEquiv R).symm.trans (DFinsupp.mapRange.linearEquiv fun i => quotEquivOfEq _ _ ?_)⟩⟩
simp only
