Finitely generated modules over a discrete valuation ring

Mathlib's structure theorem Module.equiv_free_prod_directSum writes a finitely generated module over a principal ideal domain as a free module plus a direct sum of cyclic modules R ⧸ R ∙ q ^ e with q irreducible. Over a discrete valuation ring every irreducible element is associated to a fixed uniformizer ϖ, so all the cyclic summands are quotients by powers of the single ideal (ϖ). This file records that specialisation, with the free part and the torsion part written as function types indexed by Fin, and with the trivial summands R ⧸ (ϖ ^ 0) discarded, so that the exponents e i ≥ 1 are the elementary divisors of the torsion part.

Main result

• TauCeti.Module.equiv_pi_prod_pi_quotient_span_pow: a finitely generated module over a discrete valuation ring with uniformizer ϖ is R ^ n × ∏ i, R ⧸ (ϖ ^ e i) with all e i ≥ 1.

theorem TauCeti.Module.equiv_pi_prod_pi_quotient_span_pow (R : Type u) (M : Type v) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] {ϖ : R} (hϖ : Irreducible ϖ) : ∃ (n : ℕ) (m : ℕ) (e : Fin m → ℕ), (∀ (i : Fin m), 0 < e i) ∧ Nonempty (M ≃ₗ[R] (Fin n → R) × ((i : Fin m) → R ⧸ R ∙ ϖ ^ e i))

Structure theorem for finitely generated modules over a discrete valuation ring. A finitely generated module over a discrete valuation ring R with uniformizer ϖ is isomorphic to R ^ n × ∏ i : Fin m, R ⧸ (ϖ ^ e i) with every exponent e i positive.