The Herbrand function and the upper numbering #
Let L/K be a finite Galois extension of nonarchimedean local fields, with lower ramification
groups G_u = G_{⌈u⌉} of G = Gal(L/K) indexed by real u ≥ -1. The Herbrand function is
φ_{L/K}(u) = ∫_0^u dt / [G_0 : G_t],
for u ≥ -1. Since G_t is a subgroup of G_0 for t > -1, the integrand is
#G_t / #G_0; it equals 1 on (-1, 0], so φ(u) = u for -1 ≤ u ≤ 0. On each interval
[m, m + 1] with m : ℕ the function φ is affine of slope #G_{m+1} / #G_0, which gives the
finite-sum formula
φ(u) = (#G_1 + ⋯ + #G_m + (u - m) #G_{m+1}) / #G_0.
The integrand is positive and bounded below by 1 / #G_0, so φ is a strictly increasing
continuous bijection of [-1, ∞) onto itself. This file packages it as an order isomorphism
herbrandOrderIso K L of the domain RamificationIndexDomain = [-1, ∞), whose forward map is
herbrand K L and whose inverse is the inverse Herbrand function inverseHerbrand K L, usually
written ψ_{L/K}. Keeping the domain in the type means that no statement concerns a value
below -1.
Although φ may take non-integral values at integers, ψ maps natural numbers to natural numbers.
The resulting integral inverse Herbrand function psiNat K L : ℕ → ℕ, written ψℕ_{L/K}, is
the form in which Herbrand values serve as depths of the unit filtration, for instance when
N_{L/K}(U(L, ψℕ(i))) is compared with U(K, i). It is characterized arithmetically by
ψℕ(n) = m ↔ #G_1 + ⋯ + #G_m = n · #G_0.
The upper numbering of the ramification groups is G^v = G_{ψ(v)}, so that
G^{φ(u)} = G_u. Its point is the compatibility with quotients, (G/H)^v = G^v H / H for H
normal, which the lower numbering lacks; that theorem is not proved here.
The Herbrand function and the upper numbering are defined only for Galois L/K: for a
non-Galois extension the automorphism group does not carry the ramification of L/K, and the
classical φ_{L/K} is instead defined through a Galois closure.
Main definitions #
TauCeti.LocalFieldsRamification.RamificationIndexDomain: the interval[-1, ∞).TauCeti.LocalFieldsRamification.herbrandOrderIso: the Herbrand function as an order automorphism of[-1, ∞).TauCeti.LocalFieldsRamification.herbrand,TauCeti.LocalFieldsRamification.inverseHerbrand: its forward mapφ_{L/K}and its inverseψ_{L/K}.TauCeti.LocalFieldsRamification.psiNat: the inverse Herbrand function at natural numbers,ψℕ_{L/K} : ℕ → ℕ.TauCeti.LocalFieldsRamification.upperRamificationGroup: the upper-numbering ramification groupG^v = G_{ψ(v)}.
Main results #
TauCeti.LocalFieldsRamification.coe_herbrand: the integral formula definingφ.TauCeti.LocalFieldsRamification.coe_herbrand_of_mem_IccandTauCeti.LocalFieldsRamification.coe_herbrand_of_coe_eq_natCast: the finite-sum formula.TauCeti.LocalFieldsRamification.herbrand_of_coe_le_zeroandTauCeti.LocalFieldsRamification.inverseHerbrand_of_coe_le_zero:φandψare the identity on[-1, 0].TauCeti.LocalFieldsRamification.herbrand_inverseHerbrandandTauCeti.LocalFieldsRamification.inverseHerbrand_herbrand:φ ∘ ψ = idandψ ∘ φ = id.TauCeti.LocalFieldsRamification.coe_herbrand_sub_coe_herbrand_of_forall_eq:φis affine of slope#G_b / #G_0on an interval[a, b]where the filtration is constant.TauCeti.LocalFieldsRamification.herbrand_slope_anti_adjacent:φis concave.TauCeti.LocalFieldsRamification.continuous_herbrand,TauCeti.LocalFieldsRamification.herbrand_strictMonoand their counterparts forψ.TauCeti.LocalFieldsRamification.coe_psiNat:ψℕ(n) = ψ(n)forn : ℕ, andTauCeti.LocalFieldsRamification.psiNat_eq_iff:ψℕ(n) = m ↔ #G_1 + ⋯ + #G_m = n · #G_0.TauCeti.LocalFieldsRamification.psiNat_strictMono,TauCeti.LocalFieldsRamification.self_le_psiNat:ψℕis strictly increasing andn ≤ ψℕ(n).TauCeti.LocalFieldsRamification.psiNat_eq_self_iff,TauCeti.LocalFieldsRamification.psiNat_eq_add_card_mul_sub:ψℕ(v) = vexactly whenG_v = G_0, andψℕ(v) = t + #G_0 (v - t)forv ≥ twhen the filtration is constant throughtand trivial afterward.TauCeti.LocalFieldsRamification.upperRamificationGroup_herbrand:G^{φ(u)} = G_u.TauCeti.LocalFieldsRamification.upperRamificationGroup_antitone: the upper filtration decreases, and eachG^vis normal.
References #
- J.-P. Serre, Corps Locaux, Chapter IV, §3.
The integrand and its primitive on the real line #
The Herbrand function and its inverse #
The Herbrand function φ_{L/K}(u) = ∫_0^u dt / [G_0 : G_t] of a finite Galois extension
of local fields, as an order automorphism of [-1, ∞). Its inverse is the inverse Herbrand function
ψ_{L/K}. The integral formula is coe_herbrand. The construction does not use IsGalois;
the hypothesis restricts the Herbrand function to the Galois case, where it is meaningful.
Equations
Instances For
The Herbrand function φ_{L/K}, the forward map of herbrandOrderIso K L.
Equations
Instances For
The inverse Herbrand function ψ_{L/K}, the inverse of herbrandOrderIso K L.
Equations
Instances For
The integral formula for the Herbrand function:
φ_{L/K}(u) = ∫_0^u #G_t / #G_0 dt. For t > -1 the group G_t is a subgroup of G_0 and
#G_t / #G_0 = 1 / [G_0 : G_t], so this holds almost everywhere on the interval of integration.
The Herbrand function undoes its inverse: φ(ψ(v)) = v.
The inverse Herbrand function undoes the Herbrand function: ψ(φ(u)) = u.
The Herbrand function is strictly increasing.
The inverse Herbrand function is strictly increasing.
The Herbrand function is continuous.
The inverse Herbrand function is continuous.
The Herbrand function is concave: its slopes over two adjacent intervals decrease.
The Herbrand function is the identity on [-1, 0].
On an interval [a, b] over which the lower ramification filtration is constant, that is
G_t = G_b for every a < t ≤ b, the Herbrand function is affine of slope #G_b / #G_0:
φ(b) - φ(a) = (b - a) · #G_b / #G_0.
The Herbrand function is the identity as long as the lower ramification filtration is
constant from 0 through u.
The inverse Herbrand function is the identity on [-1, 0].
The finite-sum formula for the Herbrand function: for m : ℕ and m ≤ u ≤ m + 1,
φ(u) = (#G_1 + ⋯ + #G_m + (u - m) #G_{m+1}) / #G_0.
The Herbrand function at a natural number m: φ(m) = (#G_1 + ⋯ + #G_m) / #G_0.
The upper numbering #
The upper-numbering ramification group G^v = G_{ψ(v)} of a finite Galois extension of
local fields, for v ≥ -1, where ψ = inverseHerbrand K L.
Equations
Instances For
Membership in the upper ramification groups: σ ∈ G^v ↔ σ ∈ G_{ψ(v)}.
The upper and lower numberings are related by G^{φ(u)} = G_u.
On [-1, 0] the upper and lower numberings agree.
The upper ramification filtration is decreasing.
Every upper ramification group is normal in the automorphism group.
Herbrand values at natural numbers #
The Herbrand function may take non-integral values at integers, but its inverse does not:
ψ(n) is a natural number for every natural number n, because #G_{m+1} divides #G_i for
i ≤ m + 1.
This section packages these values as psiNat K L : ℕ → ℕ.
The integral inverse Herbrand function ψℕ_{L/K} : ℕ → ℕ: the value ψ_{L/K}(n) of the
inverse Herbrand function at a natural number n, which is itself a natural number
(coe_psiNat). These are the unit depths at which the norm of L/K is compared with the unit
filtration of K.
Equations
Instances For
The integral inverse Herbrand function computes the inverse Herbrand function:
ψℕ_{L/K}(n) = ψ_{L/K}(n).
ψℕ_{L/K}(n) = m exactly when #G_1 + ⋯ + #G_m = n · #G_0, that is when φ_{L/K}(m) = n.
ψℕ_{L/K}(0) = 0.
The integral inverse Herbrand function is strictly increasing.
n ≤ ψℕ_{L/K}(n): the inverse Herbrand function never lowers a unit depth.
ψℕ_{L/K}(v) = v exactly when G_v = G_0, that is when the lower filtration is constant
through v.
If the lower filtration is constant through t and trivial after t, that is G_t = G_0
and G_{t+1} = 1, then ψℕ_{L/K}(v) = t + #G_0 · (v - t) for every v ≥ t. For a totally
ramified cyclic extension of prime degree ℓ with jump t, this is
ψℕ(v) = t + ℓ (v - t).