Local constancy of root counts over a nonarchimedean local field

Let K be a nonarchimedean local field and f a monic polynomial over 𝒪[K] that is separable over K. This file proves that the number of roots of f in a finite extension L of K does not change when the coefficients of f are perturbed slightly, and that one threshold for the size of the perturbation works for all finite extensions at once: there is T > 0 such that every monic g over 𝒪[K] with g.coeff i - f.coeff i ∈ 𝓂[K] ^ T for all i has exactly as many roots as f, counted with multiplicity, in every finite intermediate field of a fixed extension Ω / K (for instance a separable closure of K).

This is the form of continuity of roots needed to count extensions by integrating over coefficient space, as in Serre's mass formula: the root count is then a locally constant function of the coefficients near a separable polynomial. It is a statement about counts, uniform over all finite extensions; Krasner's lemma, by contrast, compares the fields generated by single roots.

Main results

• TauCeti.card_aroots_eq_of_addVal_lt_coeff_sub: for an extension L / K of nonarchimedean local fields and a Bézout certificate U f + V f' = β, a monic g whose coefficients differ from those of f by elements of order larger than 2 v(β) has as many roots as f in L.
• TauCeti.exists_card_aroots_eq: one threshold T > 0 makes the root counts of f and of every coefficientwise 𝓂[K] ^ T-close monic g agree in every finite intermediate field of a fixed extension of K.

Implementation notes

The threshold comes from a Bézout certificate U f + V f' = β over 𝒪[K], which exists since f and f' are coprime over K: the resultant of f and f' is such a β. A coefficientwise perturbation of order larger than 2 v(β) stays larger than twice the order of β in the ring of integers of every finite extension, so Polynomial.card_roots_eq_of_addVal_lt_coeff_sub applies there; the roots in L of a monic polynomial over 𝒪[K] are integral, hence lie in 𝒪[L] (TauCeti.aroots_eq_map_roots_integerRing).

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.

theorem TauCeti.card_aroots_eq_of_addVal_lt_coeff_sub {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] {f g U V : Polynomial ↥(ValuativeRel.valuation K).integer} {β : ↥(ValuativeRel.valuation K).integer} (hf : f.Monic) (hg : g.Monic) (hβ : U * f + V * Polynomial.derivative f = Polynomial.C β) (hfg : ∀ (i : ℕ), (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation K).integer) β + (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation K).integer) β < (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation K).integer) ((g - f).coeff i)) : ((Polynomial.map (algebraMap (↥(ValuativeRel.valuation K).integer) K) g).aroots L).card = ((Polynomial.map (algebraMap (↥(ValuativeRel.valuation K).integer) K) f).aroots L).card

Nearby monic polynomials have equally many roots in L. Let L / K be an extension of nonarchimedean local fields, f and g monic over 𝒪[K], and U f + V f' = β a Bézout certificate for f and its derivative. If every coefficient of g - f has order larger than 2 v(β), then g and f have the same number of roots in L, counted with multiplicity.

theorem TauCeti.exists_card_aroots_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] {f : Polynomial ↥(ValuativeRel.valuation K).integer} (hf : f.Monic) (hfsep : (Polynomial.map (algebraMap (↥(ValuativeRel.valuation K).integer) K) f).Separable) : ∃ (T : ℕ), 0 < T ∧ ∀ (M : IntermediateField K Ω) [Module.Finite K ↥M] (g : Polynomial ↥(ValuativeRel.valuation K).integer), g.Monic → (∀ (i : ℕ), g.coeff i - f.coeff i ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ T) → ((Polynomial.map (algebraMap (↥(ValuativeRel.valuation K).integer) K) g).aroots ↥M).card = ((Polynomial.map (algebraMap (↥(ValuativeRel.valuation K).integer) K) f).aroots ↥M).card

Local constancy of the root count. For a monic f over 𝒪[K] that is separable over K, there is a threshold T > 0 such that every monic g over 𝒪[K] with g.coeff i - f.coeff i ∈ 𝓂[K] ^ T for all i has as many roots as f, counted with multiplicity, in every finite intermediate field of Ω / K. The threshold depends only on f.