Theorems · Theorem · commutative algebra

Module.equiv_free_prod_directSum

• 1000+ list: Structure theorem for finitely generated modules over a principal ideal domain

∀ (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],
  ∃ n ι x p,
    ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (M ≃ₗ[R] (Fin n →₀ R) × DirectSum ι fun i => R ⧸ R ∙ p i ^ e i)

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.

Defined in

Mathlib.Algebra.Module.PID

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingIsPrincipalIdealRingAddCommGroupModuleIsDomainModule.Finite