Theorems · Theorem · commutative algebra

Submodule.exists_isInternal_prime_power_torsion_of_pid

∀ {R : Type u} [inst : CommRing R] [IsPrincipalIdealRing R] {M : Type v} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [IsDomain R] [Module.Finite R M],
  Module.IsTorsion R M →
    ∃ ι x x p,
      ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, DirectSum.IsInternal fun i => Submodule.torsionBy R M (p i ^ e i)

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.

Defined in

Mathlib.Algebra.Module.PID

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsPrincipalIdealRingAddCommGroupModuleIsDomainModule.Finite