Unramified extensions of local fields via generators

An extension L/K of nonarchimedean local fields is unramified when L = K(b) for an integral element b which is a root of a polynomial p over 𝒪[K] whose derivative p'(b) is a unit. Conversely every unramified extension is of this form: 𝒪[L] is generated over 𝒪[K] by one element at which its minimal polynomial has unit derivative. This is the criterion through which unramifiedness is transported along base change and composita.

Main results

• TauCeti.isUnramified_of_adjoin_eq_top_of_isUnit_aeval_derivative: L = K(b) is unramified over K when b is a root of a polynomial over 𝒪[K] whose derivative at b is a unit.
• TauCeti.isUnramified_iff_exists_adjoin_eq_top_and_isUnit_aeval_derivative_minpoly: L/K is unramified exactly when 𝒪[L] is generated over 𝒪[K] by an element at which its minimal polynomial has unit derivative.

References

• J.-P. Serre, Corps Locaux, Chapter III, §5.
• J. Neukirch, Algebraic Number Theory, Chapter II, §7.

theorem TauCeti.isUnramified_of_adjoin_eq_top_of_isUnit_aeval_derivative {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] {b : ↥(ValuativeRel.valuation L).integer} (hb : K⟮(algebraMap (↥(ValuativeRel.valuation L).integer) L) b⟯ = ⊤) {p : Polynomial ↥(ValuativeRel.valuation K).integer} (hp : (Polynomial.aeval b) p = 0) (hu : IsUnit ((Polynomial.aeval b) (Polynomial.derivative p))) : IsUnramified K L

A simple root of an integral polynomial generates an unramified extension. If L = K(b) for an element b of 𝒪[L] which is a root of a polynomial p over 𝒪[K] whose derivative p'(b) is a unit of 𝒪[L], then L/K is unramified.

theorem TauCeti.isUnramified_iff_exists_adjoin_eq_top_and_isUnit_aeval_derivative_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] : IsUnramified K L ↔ ∃ (b : ↥(ValuativeRel.valuation L).integer), (↥(ValuativeRel.valuation K).integer)[b] = ⊤ ∧ IsUnit ((Polynomial.aeval b) (Polynomial.derivative (minpoly (↥(ValuativeRel.valuation K).integer) b)))

Unramified extensions are generated by simple roots of integral polynomials. An extension L/K of nonarchimedean local fields is unramified exactly when 𝒪[L] is generated as an 𝒪[K]-algebra by an element b at which the derivative of its minimal polynomial over 𝒪[K] is a unit.