Roots in small balls at a uniformizer

Let ξ be a uniformizer of a totally ramified separable extension L/K of degree n, and let d be its discriminant exponent. For a monic polynomial g of degree n over 𝒪[K], and d < r, the ball v_L(y - ξ) ≥ r contains a root of g if and only if v_L(g(ξ)) ≥ r + d, and then contains exactly one root.

This is the local fibre count used to integrate the number of roots of Eisenstein polynomials. No coefficient-closeness hypothesis on g is needed: orthogonality of the powers of ξ forces the derivative order to equal d whenever either condition holds. The radius order need not be divisible by the ramification index.

References

• J.-P. Serre, Une « formule de masse » pour les extensions totalement ramifiées de degré donné d'un corps local, C. R. Acad. Sci. Paris Sér. A 286 (1978), 1031–1036, Lemma 1.

theorem TauCeti.IsTotallyRamified.existsUnique_isRoot_le_addVal_iff {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] [Algebra.IsSeparable K L] (h : IsTotallyRamified K L) {ξ : ↥(ValuativeRel.valuation L).integer} (hξ : Irreducible ξ) {g : Polynomial ↥(ValuativeRel.valuation K).integer} (hg : g.Monic) (hdeg : g.natDegree = ramificationIndex K L) {r : ℕ} (hr : discriminantExponent K L < r) : (∃! z : ↥(ValuativeRel.valuation L).integer, (Polynomial.aeval z) g = 0 ∧ ↑r ≤ (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation L).integer) (z - ξ)) ↔ ↑(r + discriminantExponent K L) ≤ (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation L).integer) ((Polynomial.aeval ξ) g)

The local fibre count. A monic polynomial of degree [L : K] has exactly one root in a sufficiently small uniformizer ball precisely when its value at the center has the extra order given by the discriminant exponent.

theorem TauCeti.IsTotallyRamified.exists_isRoot_le_addVal_iff {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] [Algebra.IsSeparable K L] (h : IsTotallyRamified K L) {ξ : ↥(ValuativeRel.valuation L).integer} (hξ : Irreducible ξ) {g : Polynomial ↥(ValuativeRel.valuation K).integer} (hg : g.Monic) (hdeg : g.natDegree = ramificationIndex K L) {r : ℕ} (hr : discriminantExponent K L < r) : (∃ (z : ↥(ValuativeRel.valuation L).integer), (Polynomial.aeval z) g = 0 ∧ ↑r ≤ (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation L).integer) (z - ξ)) ↔ ↑(r + discriminantExponent K L) ≤ (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation L).integer) ((Polynomial.aeval ξ) g)

The existence form of the local fibre criterion. Whenever a root exists in this ball, it is unique by IsTotallyRamified.existsUnique_isRoot_le_addVal_iff.