Monogenicity of a finite extension of discrete valuation rings

Let S be a discrete valuation ring, finite over a discrete valuation subring R, and assume the residue extension 𝓀(S)/𝓀(R) is separable. This file proves that S = R[β] for a single β : S. Both the ramified and the unramified case are covered; Mathlib's IsLocalRing.exists_adjoin_eq_top covers only the unramified (finite étale) case, where the generator may be taken to be any lift of a primitive element of the residue extension.

The proof is Serre's: pick a lift a of a primitive element of the residue extension and a polynomial g : R[X] lifting its minimal polynomial. Then g(a) lies in the maximal ideal and g'(a) is a unit, so one Newton step, replacing a by a + π for a uniformizer π when that is needed, arranges that g(β) generates the maximal ideal. The subring R[β] then meets every residue class modulo 𝓂(S) and contains a uniformizer, hence meets every residue class modulo 𝓂(S) ^ n; taking n large enough that 𝓂(S) ^ n ⊆ 𝓂(R) S, Nakayama's lemma gives R[β] = S.

Nothing in that argument needs the two rings to be discrete valuation rings: it runs for a module-finite extension of local rings in which the maximal ideal of S is principal, and it is developed in that generality in TauCeti.RingTheory.LocalRing.Monogenic. Being a discrete valuation ring enters here only through IsDiscreteValuationRing.exists_irreducible, which supplies the uniformizer generating 𝓂(S).

Main results

• TauCeti.IsDiscreteValuationRing.exists_adjoin_eq_top: a finite extension of discrete valuation rings with separable residue extension is monogenic.
• TauCeti.IsDiscreteValuationRing.nonempty_powerBasis: the integral basis a generator produces, via Mathlib's PowerBasis.ofAdjoinEqTop'.
• TauCeti.IsDiscreteValuationRing.exists_powerBasis_intermediateField_adjoin_eq_top: that integral basis can be chosen with its generator a primitive element of the fraction field of S over an intermediate base field.

References

• J.-P. Serre, Corps locaux, Chapter III, §6, Proposition 12.

theorem TauCeti.IsDiscreteValuationRing.exists_adjoin_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [IsDiscreteValuationRing R] [IsDiscreteValuationRing S] [Algebra R S] [Module.Finite R S] [FaithfulSMul R S] [Algebra.IsSeparable (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)] : ∃ (β : S), R[β] = ⊤

Local monogenicity. A finite extension of discrete valuation rings whose residue extension is separable is generated by a single element. Completeness of R is not needed: it enters the classical statement only to guarantee that the integral closure of R in a finite field extension is again a discrete valuation ring, which is here a hypothesis on S.

theorem TauCeti.IsDiscreteValuationRing.nonempty_powerBasis {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [IsDiscreteValuationRing R] [IsDiscreteValuationRing S] [Algebra R S] [Module.Finite R S] [FaithfulSMul R S] [Algebra.IsSeparable (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)] : Nonempty (PowerBasis R S)

A finite extension of discrete valuation rings with separable residue extension admits a power basis: the integral basis 1, β, …, β ^ (n - 1) attached to a generator β.

theorem TauCeti.IsDiscreteValuationRing.exists_powerBasis_intermediateField_adjoin_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [IsDiscreteValuationRing R] [IsDiscreteValuationRing S] [Algebra R S] [Module.Finite R S] [FaithfulSMul R S] [Algebra.IsSeparable (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)] (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra R K] [Algebra R L] [Algebra S L] [Algebra K L] [IsScalarTower R S L] [IsScalarTower R K L] [IsFractionRing S L] : ∃ (pb : PowerBasis R S), K⟮(algebraMap S L) pb.gen⟯ = ⊤

The integral power basis of TauCeti.IsDiscreteValuationRing.nonempty_powerBasis can be chosen so that its generator is at the same time a primitive element of the fraction field L of S over any field K between R and L: a generator of S over R also generates L over K, by TauCeti.IntermediateField.adjoin_eq_top_of_algebra_adjoin_eq_top.