Goal
Package the basic invariants of a finite extension L/K of p-adic fields: ramification index e, residue degree f (with ef = [L:K]), the residue field, and the discriminant exponent d = v_K(disc(L/K)).
What already exists
- mathlib:
Padic, PadicInt, IsLocalRing/DVR API, Ideal.ramificationIdx, Ideal.inertiaDeg, IsDedekindDomain discriminant/differentIdeal.
What's missing
- The
p-adic-field-facing packaging: e, f, residue field, and the discriminant exponent as a single invariant of L/K, with ef = [L:K] and d = 0 ⟺ L/K unramified (and d = e − 1 in the tame case).
Test cases
ℚ_p unramified extensions (f = n, e = 1, d = 0); ℚ_p(p^{1/e}) totally tamely ramified (d = e − 1); a wildly ramified ℚ_2 extension.
LMFDB targets
New area, not yet in the Verso blueprint — links go to the LMFDB knowls.
Goal
Package the basic invariants of a finite extension
L/Kofp-adic fields: ramification indexe, residue degreef(withef = [L:K]), the residue field, and the discriminant exponentd = v_K(disc(L/K)).What already exists
Padic,PadicInt,IsLocalRing/DVR API,Ideal.ramificationIdx,Ideal.inertiaDeg,IsDedekindDomaindiscriminant/differentIdeal.What's missing
p-adic-field-facing packaging:e,f, residue field, and the discriminant exponent as a single invariant ofL/K, withef = [L:K]andd = 0 ⟺ L/Kunramified (andd = e − 1in the tame case).Test cases
ℚ_punramified extensions (f = n,e = 1,d = 0);ℚ_p(p^{1/e})totally tamely ramified (d = e − 1); a wildly ramifiedℚ_2extension.LMFDB targets
lf.discriminant_exponentlf.ramification_indexlf.residue_fieldlf.unramified_degreeNew area, not yet in the Verso blueprint — links go to the LMFDB knowls.