Goal
Define the higher ramification filtration of a p-adic field extension and the LMFDB ramification data: ramification breaks/slopes, the Herbrand function ψ_{L/K}/φ_{L/K}, and the ramification polygon (the Newton polygon of the ramification polynomial of an Eisenstein uniformiser).
What already exists
- mathlib:
Padic, valuations, Eisenstein polynomials (Polynomial.IsEisensteinAt), Newton polygon (Polynomial.newtonPolygon?). Higher ramification groups may be partially present — confirm.
What's missing
- Lower/upper-numbering ramification groups
G_i/G^u, the Herbrand functions ψ, φ and G^{φ(i)} = G_i, ramification breaks, and the ramification polygon of L/K.
Test cases
- Tamely ramified: a single break at
0. ℚ_2(√2), ℚ_p(ζ_{p^2}): explicit breaks / Herbrand function.
LMFDB targets
New area, not yet in the Verso blueprint — links go to the LMFDB knowls.
Goal
Define the higher ramification filtration of a
p-adic field extension and the LMFDB ramification data: ramification breaks/slopes, the Herbrand functionψ_{L/K}/φ_{L/K}, and the ramification polygon (the Newton polygon of the ramification polynomial of an Eisenstein uniformiser).What already exists
Padic, valuations, Eisenstein polynomials (Polynomial.IsEisensteinAt), Newton polygon (Polynomial.newtonPolygon?). Higher ramification groups may be partially present — confirm.What's missing
G_i/G^u, the Herbrand functionsψ, φandG^{φ(i)} = G_i, ramification breaks, and the ramification polygon ofL/K.Test cases
0.ℚ_2(√2),ℚ_p(ζ_{p^2}): explicit breaks / Herbrand function.LMFDB targets
lf.ramification_polygonlf.herbrand_functionlf.slopeslf.wild_inertia_groupNew area, not yet in the Verso blueprint — links go to the LMFDB knowls.