Finitely generated modules over a PID

TheoremStructure theorem#

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.

Module.equiv_free_prod_directSum.{u, v} (R : Type u) [CommRing R] [IsPrincipalIdealRing R]
  (M : Type v) [AddCommGroup M] [_root_.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)

Sources

• Mathlib documentation: Module.equiv_free_prod_directSum
• Source of Module.equiv_free_prod_directSum in Mathlib/Algebra/Module/PID.lean
• Mathlib overview: Linear algebra › Finitely generated modules over a PID
• 1000+ theorems list: Q7888360
• 1000+ theorems project: Q7888360
• Wikipedia: Structure theorem for finitely generated modules over a principal ideal domain
• Wikidata: Q7888360

MathlibModule.equiv_free_prod_directSum

Uses 22

Statement usesFinitely supported function · Irreducible element · Linear map · Principal ideal domain · Product of vector spaces · Quotient space (Fundamentals)

Proof usesAssociative algebra over a commutative ring · Basis · Direct sum · Isomorphism · Kernel of a linear map · Linear independence · Localization · Maximal ideal · Noetherian module · Noetherian ring · Polynomial in one indeterminate · Prime ideal · Range of a linear map · Small category · The category of modules over a ring · The Fundamental Theorem of Arithmetic

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.