theorem dvr_fg_torsionFree_is_free (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.IsTorsionFree R M] : Module.Free R M

Over a discrete valuation ring, every finitely generated torsion-free module is free.

noncomputable def dvr_fg_torsionFree_basis (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.IsTorsionFree R M] : (n : ℕ) × Module.Basis (Fin n) R M

An explicit basis (with rank) for a finitely generated torsion-free module over a DVR.

theorem dvr_torsionSplitting (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Finite R M] : Nonempty ((↥(Submodule.torsion R M) × M ⧸ Submodule.torsion R M) ≃ₗ[R] M)

Over a DVR, a finitely generated module splits as the product of its torsion submodule and its torsion-free quotient.

theorem dvr_fg_structure (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] : ∃ (n : ℕ) (ι : Type u) (x : Fintype ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ), Nonempty (M ≃ₗ[R] (Fin n →₀ R) × DirectSum ι fun (i : ι) => R ⧸ R ∙ p i ^ e i)

Structure theorem: every finitely generated module over a DVR (or, more generally, a PID) decomposes as a free part plus a direct sum of cyclic torsion modules R / (p^e) for irreducible p.

theorem dvr_quotient_torsion_free (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Finite R M] : Module.Free R (M ⧸ Submodule.torsion R M)

The quotient of a finitely generated DVR-module by its torsion is free.

theorem dvr_free_iff_torsionFree (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Finite R M] : Module.Free R M ↔ Module.IsTorsionFree R M

For a finitely generated module over a DVR, freeness is equivalent to torsion-freeness.