Theorems · Theorem · commutative algebra

Module.torsion_by_prime_power_decomposition

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

A finitely generated p ^ ∞-torsion module over a PID is isomorphic to a direct sum of some R ⧸ R ∙ (p ^ e i) for some e i.

Defined in

Mathlib.Algebra.Module.PID

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsPrincipalIdealRingAddCommGroupModuleIsDomainModule.Finite