Eisenstein coefficient fibres over balls of uniformizers

Let L / K be an extension of nonarchimedean local fields with ramification index n. When a ball v_L(z - c) ≥ r is centred at a uniformizer c and has order r ≥ 2, every root in the ball is a uniformizer. A monic polynomial over 𝒪[K] of degree e(L/K) with a uniformizer as a root is Eisenstein, so the part of the Eisenstein region whose polynomial has a root in the ball is the image of the set of all integral coefficient vectors whose polynomial has a root there. This is the form of the fibre on which the local root criterion at the centre and the volume computation in power-basis coordinates operate.

Main results

• TauCeti.eisensteinSet_inter_setOf_exists_aeval_monicOfCoeff_eq_zero_le_addVal_eq_image: over a ball of order at least 2 centred at a uniformizer, the fibre of the Eisenstein region is the image of the corresponding integral coefficient fibre.

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, §3, Lemmas 2–3.

theorem TauCeti.eisensteinSet_inter_setOf_exists_aeval_monicOfCoeff_eq_zero_le_addVal_eq_image {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] {n : ℕ} (hn : ramificationIndex K L = n) {r : ℕ} (hr : 1 < r) {c : ↥(ValuativeRel.valuation L).integer} (hc : (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation L).integer) c = 1) : eisensteinSet K n ∩ {a : Fin n → K | ∃ (z : ↥(ValuativeRel.valuation L).integer), (Polynomial.aeval ↑z) (Polynomial.monicOfCoeff a) = 0 ∧ ↑r ≤ (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation L).integer) (z - c)} = (fun (b : Fin n → ↥(ValuativeRel.valuation K).integer) (i : Fin n) => ↑(b i)) '' {b : Fin n → ↥(ValuativeRel.valuation K).integer | ∃ (z : ↥(ValuativeRel.valuation L).integer), (Polynomial.aeval z) (Polynomial.monicOfCoeff b) = 0 ∧ ↑r ≤ (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation L).integer) (z - c)}

Coefficient fibres at a uniformizer are integral. Let n = e(L/K), let c be a uniformizer of L, and let 1 < r. A coefficient vector in the Eisenstein region whose polynomial has a root in the ball v_L(z - c) ≥ r is the coefficient vector of a monic polynomial over 𝒪[K] with a root in that ball. Conversely, every root in that ball is a uniformizer, so every monic polynomial of degree e(L/K) over 𝒪[K] with such a root is Eisenstein. Hence this part of the Eisenstein region is the image of the corresponding set of integral coefficient vectors.