Valuations in an Eisenstein power basis of a local field

Let ξ ∈ 𝒪[L] be a root of an Eisenstein polynomial f over 𝒪[K] with L = K(ξ). Comparing the normalized valuations of ξ and of its norm, which is the constant coefficient of f up to a unit, shows that ξ is a uniformizer of L and that L/K has inertia degree one, so that e(L/K) = [L : K] = deg f. By TauCeti.addVal_sum_algebraMap_mul_pow_of_irreducible, the valuation of a linear combination in the power basis 1, ξ, …, ξ^{deg f - 1} is therefore the minimum of its term valuations.

Main result

• TauCeti.irreducible_of_eisenstein_adjoin_eq_top shows that a generator of L/K satisfying an Eisenstein polynomial is a uniformizer.
• TauCeti.inertiaDegree_eq_one_of_eisenstein_adjoin_eq_top and TauCeti.ramificationIndex_eq_natDegree_of_eisenstein_adjoin_eq_top record its characteristic total-ramification consequences.
• TauCeti.addVal_sum_eisenstein_powerBasis computes the additive valuation of a linear combination of powers of an Eisenstein generator.

References

• J.-P. Serre, Local Fields, Chapter I, §6, Proposition 17.
• J.-P. Serre, Local Fields, Chapter III, §6, Proposition 12.

theorem TauCeti.irreducible_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⟮↑ξ⟯ = ⊤) : Irreducible ξ

A generator of L/K that is a root of an Eisenstein polynomial over 𝒪[K] is a uniformizer of 𝒪[L].

theorem TauCeti.inertiaDegree_eq_one_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⟮↑ξ⟯ = ⊤) : inertiaDegree K L = 1

An extension L/K generated by a root of an Eisenstein polynomial over 𝒪[K] has inertia degree one.

theorem TauCeti.ramificationIndex_eq_natDegree_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⟮↑ξ⟯ = ⊤) : ramificationIndex K L = f.natDegree

For a generator of L/K that is a root of an Eisenstein polynomial over 𝒪[K], the ramification index is the degree of that polynomial.

theorem TauCeti.addVal_sum_eisenstein_powerBasis {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⟮↑ξ⟯ = ⊤) (c : Fin f.natDegree → ↥(ValuativeRel.valuation K).integer) : (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation L).integer) (∑ i : Fin f.natDegree, (algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) (c i) * ξ ^ ↑i) = ⨅ (i : Fin f.natDegree), ramificationIndex K L • (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation K).integer) (c i) + ↑↑i

For a generator ξ of L/K that is a root of an Eisenstein polynomial f over 𝒪[K], the additive valuation of a linear combination of 1, ξ, …, ξ^{deg f - 1} with coefficients in 𝒪[K] is the least of its term valuations.