Totally ramified extensions of local fields are Eisenstein

Let L/K be a totally ramified extension of nonarchimedean local fields, e(L/K) = [L : K]. Every uniformizer ϖ of L then generates 𝒪[L] as an 𝒪[K]-algebra, hence L over K, and its minimal polynomial over 𝒪[K] is Eisenstein. Conversely, by TauCeti.NumberTheory.LocalField.Eisenstein.PowerBasis, an extension generated by a root of an Eisenstein polynomial over 𝒪[K] is totally ramified, the root is a uniformizer, and so it also generates 𝒪[L] over 𝒪[K]. This characterizes the totally ramified extensions as those generated, as fields or equivalently as integer rings, by a root of an Eisenstein polynomial.

The Eisenstein property of the minimal polynomial is an instance of a criterion that needs no total ramification: a polynomial of degree e(L/K) over 𝒪[K] with unit leading coefficient that has a uniformizer of L as a root is Eisenstein.

Main results

• TauCeti.isEisensteinAt_of_isRoot_of_irreducible: a polynomial of degree e(L/K) over 𝒪[K] with unit leading coefficient and a uniformizer of L as a root is Eisenstein.
• TauCeti.IsTotallyRamified.isEisensteinAt_minpoly: in a totally ramified extension, the minimal polynomial over 𝒪[K] of a uniformizer of L is Eisenstein.
• TauCeti.IsTotallyRamified.exists_eisenstein_adjoin_eq_top: a totally ramified extension is generated, over 𝒪[K] and over K, by a root of an Eisenstein polynomial over 𝒪[K].
• TauCeti.isTotallyRamified_of_eisenstein_adjoin_eq_top and TauCeti.algebra_adjoin_eq_top_of_eisenstein_adjoin_eq_top: an extension generated by a root of an Eisenstein polynomial is totally ramified, and that root generates 𝒪[L] over 𝒪[K].
• TauCeti.isTotallyRamified_iff_exists_eisenstein_generator: an extension is totally ramified if and only if it is generated over K by a root of an Eisenstein polynomial over 𝒪[K]; TauCeti.isTotallyRamified_iff_exists_eisenstein_integral_generator is the same statement with 𝒪[L] generated over 𝒪[K].

References

• J.-P. Serre, Local Fields, Chapter I, §6, Propositions 17 and 18.

theorem TauCeti.isEisensteinAt_of_isRoot_of_irreducible {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] {g : Polynomial ↥(ValuativeRel.valuation K).integer} (hg : g.leadingCoeff ∉ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) (hdeg : g.natDegree = ramificationIndex K L) {ϖ : ↥(ValuativeRel.valuation L).integer} (hϖ : Irreducible ϖ) (hroot : (Polynomial.map (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) g).IsRoot ϖ) : g.IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer)

A polynomial over 𝒪[K] of degree e(L/K) with unit leading coefficient that has a uniformizer of L as a root is Eisenstein at the maximal ideal of 𝒪[K].

theorem TauCeti.IsTotallyRamified.isEisensteinAt_minpoly {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (h : IsTotallyRamified K L) {ϖ : ↥(ValuativeRel.valuation L).integer} (hϖ : Irreducible ϖ) : (minpoly (↥(ValuativeRel.valuation K).integer) ϖ).IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer)

In a totally ramified extension of nonarchimedean local fields, the minimal polynomial over 𝒪[K] of any uniformizer of L is Eisenstein at the maximal ideal of 𝒪[K].

theorem TauCeti.IsTotallyRamified.exists_eisenstein_adjoin_eq_top {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (h : IsTotallyRamified K L) : ∃ (f : Polynomial ↥(ValuativeRel.valuation K).integer) (π : ↥(ValuativeRel.valuation L).integer), f.IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) ∧ (Polynomial.map (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) f).IsRoot π ∧ (↥(ValuativeRel.valuation K).integer)[π] = ⊤ ∧ K⟮↑π⟯ = ⊤

Totally ramified extensions are Eisenstein. A totally ramified extension L/K of nonarchimedean local fields is generated, both as an extension of integer rings and as a field extension, by a root of an Eisenstein polynomial over 𝒪[K]: namely by any uniformizer of L, a root of its minimal polynomial.

theorem TauCeti.isTotallyRamified_of_eisenstein_adjoin_eq_top {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] {f : Polynomial ↥(ValuativeRel.valuation K).integer} (hf : f.IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer)) {π : ↥(ValuativeRel.valuation L).integer} (hroot : (Polynomial.map (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) f).IsRoot π) (hgen : K⟮↑π⟯ = ⊤) : IsTotallyRamified K L

Eisenstein extensions are totally ramified. An extension L/K of nonarchimedean local fields generated by a root of an Eisenstein polynomial over 𝒪[K] is totally ramified.

theorem TauCeti.algebra_adjoin_eq_top_of_eisenstein_adjoin_eq_top {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] {f : Polynomial ↥(ValuativeRel.valuation K).integer} (hf : f.IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer)) {π : ↥(ValuativeRel.valuation L).integer} (hroot : (Polynomial.map (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) f).IsRoot π) (hgen : K⟮↑π⟯ = ⊤) : (↥(ValuativeRel.valuation K).integer)[π] = ⊤

A root π of an Eisenstein polynomial over 𝒪[K] that generates L over K also generates 𝒪[L] as an 𝒪[K]-algebra.

theorem TauCeti.isTotallyRamified_iff_exists_eisenstein_generator (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : IsTotallyRamified K L ↔ ∃ (f : Polynomial ↥(ValuativeRel.valuation K).integer) (π : ↥(ValuativeRel.valuation L).integer), f.IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) ∧ (Polynomial.map (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) f).IsRoot π ∧ K⟮↑π⟯ = ⊤

Totally ramified is equivalent to Eisenstein. An extension L/K of nonarchimedean local fields is totally ramified, e(L/K) = [L : K], if and only if L = K(π) for a root π of an Eisenstein polynomial over 𝒪[K].

theorem TauCeti.isTotallyRamified_iff_exists_eisenstein_integral_generator (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : IsTotallyRamified K L ↔ ∃ (f : Polynomial ↥(ValuativeRel.valuation K).integer) (π : ↥(ValuativeRel.valuation L).integer), f.IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) ∧ (Polynomial.map (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) f).IsRoot π ∧ (↥(ValuativeRel.valuation K).integer)[π] = ⊤

Totally ramified is equivalent to Eisenstein, integrally. An extension L/K of nonarchimedean local fields is totally ramified if and only if 𝒪[L] is generated as an 𝒪[K]-algebra by a root of an Eisenstein polynomial over 𝒪[K].