The local fibre count for counted subextensions

These IntermediateField theorems specialize the root-ball criterion to totally ramified subextensions of a fixed separable closure. They install each finite subextension's canonical local-field structures, so callers supply only membership in totallyRamifiedOfDegree.

For a uniformizer ξ, a monic degree-n polynomial g, and radius order r > d, where d is the discriminant exponent, the ball v_L(z - ξ) ≥ r contains a root precisely when v_L(g(ξ)) ≥ r + d, and that root is unique. This criterion supplies the local fibres used to integrate the root count of Eisenstein polynomials. For a left-invariant measure on the coefficient space normalized on the integer box, the fibre over such a ball has volume q ^ (-(r + d)), where q is the residue cardinality of K.

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 and §3.

theorem IntermediateField.exists_isRoot_le_addVal_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {L : IntermediateField K (SeparableClosure K)} (hL : L ∈ TauCeti.totallyRamifiedOfDegree K n) {ξ : ↥(ValuativeRel.valuation ↥L).integer} : Irreducible ξ → ∀ {g : Polynomial ↥(ValuativeRel.valuation K).integer}, g.Monic → g.natDegree = n → ∀ {r : ℕ}, L.discriminantExponent < r → ((∃ (z : ↥(ValuativeRel.valuation ↥L).integer), (Polynomial.aeval z) g = 0 ∧ ↑r ≤ (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation ↥L).integer) (z - ξ)) ↔ ↑(r + L.discriminantExponent) ≤ (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation ↥L).integer) ((Polynomial.aeval ξ) g))

The local fibre criterion for a counted subextension, using its canonical local-field structures. No topology or valuation on the subextension is supplied by the caller.

theorem IntermediateField.existsUnique_isRoot_le_addVal_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {L : IntermediateField K (SeparableClosure K)} (hL : L ∈ TauCeti.totallyRamifiedOfDegree K n) {ξ : ↥(ValuativeRel.valuation ↥L).integer} : Irreducible ξ → ∀ {g : Polynomial ↥(ValuativeRel.valuation K).integer}, g.Monic → g.natDegree = n → ∀ {r : ℕ}, L.discriminantExponent < r → ((∃! z : ↥(ValuativeRel.valuation ↥L).integer, (Polynomial.aeval z) g = 0 ∧ ↑r ≤ (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation ↥L).integer) (z - ξ)) ↔ ↑(r + L.discriminantExponent) ≤ (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation ↥L).integer) ((Polynomial.aeval ξ) g))

The unique-root form of the local fibre criterion for a counted subextension, with its canonical local-field structures.

theorem IntermediateField.measure_image_setOf_exists_aeval_monicOfCoeff_eq_zero_le_addVal {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {L : IntermediateField K (SeparableClosure K)} (hL : L ∈ TauCeti.totallyRamifiedOfDegree K n) [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] (μ : MeasureTheory.Measure (Fin n → K)) [μ.IsAddLeftInvariant] : μ (TauCeti.integerBox K (Fin n)) = 1 → ∀ {ξ : ↥(ValuativeRel.valuation ↥L).integer}, Irreducible ξ → ∀ {r : ℕ}, L.discriminantExponent < r → μ ((fun (c : Fin n → ↥(ValuativeRel.valuation K).integer) (i : Fin n) => ↑(c i)) '' {c : Fin n → ↥(ValuativeRel.valuation K).integer | ∃ (z : ↥(ValuativeRel.valuation ↥L).integer), (Polynomial.aeval z) (TauCeti.Polynomial.monicOfCoeff c) = 0 ∧ ↑r ≤ (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation ↥L).integer) (z - ξ)}) = 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (r + L.discriminantExponent)

The volume of a local fibre for a counted subextension L ∈ σ_K(n), with its canonical local-field structures. For a uniformizer ξ of L and d < r, where d is the discriminant exponent, and a left-invariant measure on Fin n → K normalized on the integer box, the monic polynomials of degree n over 𝒪[K] having a root in the ball v_L(z - ξ) ≥ r, identified with their lower coefficients, have volume q ^ (-(r + d)), where q = Nat.card 𝓀[K].