Theorems · Theorem · commutative algebra

Module.equiv_directSum_of_isTorsion

∀ {R : Type u} [inst : CommRing R] [IsPrincipalIdealRing R] {M : Type v} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [IsDomain R] [h' : Module.Finite R M],
  Module.IsTorsion R M →
    ∃ ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (M ≃ₗ[R] DirectSum ι fun i => R ⧸ R ∙ p i ^ e i)

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.

Defined in

Mathlib.Algebra.Module.PID

Cited by

2 results in Mathlib

Foundations

Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsPrincipalIdealRingAddCommGroupModuleIsDomainModule.Finite