Auxiliary file: the uniformizer parametrization #
The algebraic layer of the §3 change of variables (equations (5)–(13)), stated in the coordinates
of the monogenic basis of integers L ([Serre 1978, §3, pp.1032–1033][Serre1978]). L carries no
topology in this project (see the header of RootLifting.lean), so the paper's map from the
uniformizers of L to the Eisenstein coefficients cannot be integrated over directly: the source of
the parametrization is the coefficient space Fin n → K of the power basis of an Eisenstein
generator (monogenicity and Newton lifting), and both source and target are the same measured space.
This file supplies the dictionary between the two pictures; the measure-theoretic assembly lives in
First.lean, on top of the scaling law of HaarScaling.lean.
The file has four layers:
- Orthogonality of a power basis. In
integers L, generated over𝒪[K]by an Eisenstein generatorξ, the terms of a combination of thec i * ξ ^ ifori < nhave pairwise distinct valuations—thei-th term has valuationn * v (c i) + i, and the exponents are distinct modulonbecausei < n. So no cancellation is possible and the valuation of the sum is the minimum of the terms' (le_addVal_sum_iff). A ball ofintegers Lis therefore a box in coordinates, and at a radius that is a multiple ofnit is the cube of radiusπ ^ ρ(le_addVal_mul_iff)—which is what keeps the volume bookkeeping of eq. (13) free of ceilings. Orthogonality also gives the power basis at every uniformizer, not just at the Eisenstein generator (powersBasis): the transition matrix between two such bases is triangular with unit diagonal modulo𝓂[K], so its determinant is a unit. - The matrix of a multiplication. A ball of
integers Lof arbitrary radius is the ideal generated by a suitablez, and in coordinates that ideal is the image lattice of the matrix of multiplication byz(toCoeff_equivFun_mem_imageLattice_iff), whose determinant is the norm ofz(det_leftMulMatrix). Someasure_integerBox_eq_pow_mulgives its volume as1 / qto the order of that norm—and it is this, not a Jacobian, that carries the factor1 / q ^ d Lof equations (11)–(13). - The order of the norm of the derivative. That order, for
zthe derivative ofgatξ, isd L(associated_norm_derivative): that norm is the discriminant of the power basis up to sign, hence generatesdiscIdeal(discIdeal_eq_span), whose multiplicity at𝓂[K]isd Lby definition. This is Serre's Lemma 2 and equation (11) with no conjugates, no Vandermonde, and no square roots. Since for a totally ramified extension the norm computes the valuation (addVal_norm), the samed Lis also the valuation of that derivative inintegers L(addVal_derivative_eq_d)—which is the exponent the fiber count below is stated with. - The local fiber count. The cube around
ξof radiusπ ^ ρcontains exactly one root of a monicFof degreenprecisely when the valuation ofFatξis at leastn * ρ + δ(existsUnique_isRoot_iff)—Newton (exists_isRoot) in one direction, the factorization ofFatξas(ξ - y) * h ξin the other. So the image of a cube under the minimal-polynomial map is the exact level set of the valuation offatξ, an affine condition on the coefficients offand hence a lattice translate, which is what replaces Lemmas 1 and 3 of the paper.
Everything except the specializations is stated for an abstract pair of discrete valuation rings in
which π is associated to ξ ^ n, since nothing about local fields, integral closures, or
Eisenstein polynomials enters it.
References #
- [Serre1978] 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 286 (1978), Série A, 1031–1036.
Orthogonality of a power basis over a discrete valuation ring #
R and A are discrete valuation rings, A an R-algebra in which the uniformizer π of R is
an associate of ξ ^ n for a uniformizer ξ of A—the interleaving equating (ξ) ^ n with π
times integers L that a totally ramified extension of degree n produces
(span_integralGen_pow_eq).
Associated elements of a discrete valuation ring have equal additive valuation.
Through the interleaving associating π with ξ ^ n, the valuation of an element of R is
multiplied by n upstairs—the totally ramified normalization of the valuation on R.
The valuation of one term of a power-basis combination.
Orthogonality of a power basis: a combination of the c i * ξ ^ i for i < n has valuation at
least m exactly when each of its terms does. One direction is the ultrametric inequality; the
other is the absence of cancellation, the terms having pairwise distinct valuations
n * v (c i) + i by fin_eq_of_mul_add_eq, so that the smallest one survives in the sum.
The matrix of a multiplication #
The image of the ideal z A in coordinates is the lattice of the matrix of multiplication by z,
whose determinant is the norm of z—the pair of facts that lets the scaling law of
HaarScaling.lean compute the volume of a ball of integers L.
The lattice of a multiplication matrix: the coordinate vector of y lies in the range of the
matrix of multiplication by z exactly when z divides y, the matrix acting on coordinates as
the multiplication does on elements.
The determinant of the matrix of a multiplication is the norm—the classical definition of the norm, read backwards.
A ball of A is a box in power-basis coordinates: the orthogonality relation, read on the
coordinates of an element rather than on a given combination.
A ball of radius a multiple of n is a cube: an element lies in π ^ ρ * A exactly when every
one of its power-basis coordinates lies in π ^ ρ * R—the offset i < n of the i-th coordinate
cannot bridge a gap of n, so the n coordinatewise conditions all read ρ ≤ v (c i). This is the
form the volume computation of equation (13) uses: on such radii no ceiling ever appears.
The value at ξ of the base change of a polynomial of degree < n, as a combination of the
powers—the shape the orthogonality relation consumes.
The power basis at an arbitrary uniformizer #
The cubes decomposing the set of uniformizers in the change of variables are centered at arbitrary
uniformizers of integers L, and each carries its own affine chart—the coordinates of the powers of
its center. So the power basis is needed not only at the Eisenstein generator of
integers_eq_adjoin but at every uniformizer. Orthogonality supplies it: since η ^ j has
valuation exactly j, the j-th coordinate of η ^ j in the basis of the powers of ξ is a unit
while the earlier ones lie in the maximal ideal of R, so the transition matrix is triangular with
unit diagonal modulo that ideal and its determinant is a unit.
The coordinates, in a power basis, of the powers of another uniformizer.
Instances For
The transition matrix has unit determinant: modulo the maximal ideal of R it is triangular
with unit diagonal, so its determinant is nonzero in the residue field, hence a unit in the local
ring R.
The power basis at an arbitrary uniformizer: once the powers of one uniformizer form an
R-basis of A, so do the powers of every uniformizer, the transition matrix between the two
families having unit determinant.
Equations
- MassFormula.powersBasis hπ hξ hn hass b hb hη = b.map (Matrix.toLinearEquiv b (MassFormula.transition b η) ⋯)
Instances For
The order of the derivative is an invariant of A #
The exponent δ of the fiber count below is the valuation of the derivative of G at ξ, for G
the monic degree-n annihilator of a uniformizer ξ. The change of variables sums over cubes
centered at different uniformizers, so it needs δ to be the same for all of them—classically,
δ is the valuation of the different, an invariant of integers L over 𝒪[K]. The proof here is
elementary and stays inside A: writing η = P ξ and ξ = Q η with P and Q over R (possible
since the powers of either uniformizer form a basis), the chain rule turns each of the identities
presenting G at η composed with P, and G at ξ composed with Q, as multiples of the other
annihilator, into a divisibility between the two derivatives, while the divisibility of
Q.comp P - X by G at ξ makes the product of the two expansion derivatives congruent to 1—so
both are units and the two divisibilities are equalities.
The polynomial expanding y in a power basis.
Equations
- MassFormula.expand b y = ∑ i : Fin n, Polynomial.C ((b.repr y) i) * Polynomial.X ^ ↑i
Instances For
The monic degree-n annihilator of y read off a power basis at y: y ^ n minus its
expansion in the lower powers.
Equations
- MassFormula.annih b y = Polynomial.X ^ n - MassFormula.expand b (y ^ n)
Instances For
The order of the derivative of a monic annihilator is an invariant of A, not of the
uniformizer used to present it—classically, the valuation of the different. This is what lets the
change of variables use one exponent for all of its cubes.
The local fiber count of the minimal-polynomial map #
The analytic heart of the change of variables, still over an abstract pair of discrete valuation
rings. For a uniformizer ξ of A annihilated by a monic G of degree n over R, and δ the
valuation of the derivative of G at ξ, the cube around ξ of radius π ^ ρ contains exactly
one root of a monic F of degree n when the valuation of F at ξ is at least n * ρ + δ, and
none otherwise.
The paper gets this from the étaleness of the parametrization (Lemma 1) and the change-of-variables
formula (Lemma 3). Here one direction is Newton's method (exists_isRoot) and the other the
factorization of F at ξ as (ξ - y) * h ξ at a root y, with the orthogonality above
converting "the value at ξ is small" into "the coefficients are close" (coeff_mem_span_pow).
That conversion is what makes the image of the cube the exact level set of the valuation of f at
ξ—an affine condition on the coefficients of f, hence a lattice—rather than a linear image up to
higher order.
Two monic polynomials of the same positive degree differ in degree < n.
The fiber, the forward direction: a root of F in the cube around ξ forces the value of F
at ξ to have valuation at least n * ρ + δ. The factorization F = (X - y) * h gives that value
as (ξ - y) * h ξ, and h ξ has valuation at least δ because it agrees with the derivative of
F at ξ modulo ξ - y.
The fiber, the backward direction: if the value of F at ξ has valuation at least
n * ρ + δ, then F has a root in the cube around ξ. Newton's method (exists_isRoot) applies
because that valuation exceeds twice δ, which is the valuation of the derivative of F at ξ,
and it lands the root at distance of order at least n * ρ.
The order of the derivative at a nearby root: if a monic F of degree n has a root y in the
cube around ξ, then the derivative of F at y has valuation δ. Applied to the minimal
polynomial of another uniformizer of the same cube, this says that δ depends only on the cube
and not on the generator used to describe it—which is what lets the volume bookkeeping of the change
of variables use a single exponent for every cube.
The fiber is at most a singleton: two roots of F in the same cube coincide.
Distinct roots are no farther apart than the order of the derivative (addVal_sub_le_of_isRoot),
which is δ at either of them, and δ < n * ρ.
The local fiber count behind the change of variables, the quantitative form of Lemma 1 and the
surjectivity of the parametrization: the cube around ξ of radius π ^ ρ contains exactly one root
of F precisely when the value of F at ξ has valuation at least n * ρ + δ. So the image of
the cube under the minimal-polynomial map is the exact level set of that condition, an affine
condition on the coefficients of F and hence a translate of a lattice
([Serre 1978, Lemma 1, p.1033][Serre1978]).
The coordinate dictionary at an Eisenstein generator #
The specialization of the layer above to integers L at an Eisenstein generator, through the
monogenic power basis basisOfEisenstein.
The Eisenstein generator is a uniformizer of integers L: it generates the maximal ideal
(isMaximal_span_integralGen).
The interleaving equating (ξ) ^ n with π times integers L, from
span_integralGen_pow_eq, in the associate form the orthogonality layer consumes.
The coordinate dictionary at an Eisenstein generator: an element of integers L lies in
π ^ ρ times integers L exactly when all of its coordinates in the monogenic basis
(basisOfEisenstein) lie in π ^ ρ times 𝒪[K], so a ball of integers L whose radius is a
multiple of n is a cube in coordinates. This is the dictionary that turns the source side of the
paper's parametrization (equations (6)–(7)) into a subset of the same measured coefficient space as
its target.
The power basis of integers L at an arbitrary uniformizer—the affine chart that each cube of
the decomposition of the set of uniformizers carries, being centered at a uniformizer of its own.
Equations
- MassFormula.powersBasisIntegers hπ hint hei hη = MassFormula.powersBasis hπ ⋯ ⋯ ⋯ (MassFormula.basisOfEisenstein hπ hint hei) ⋯ hη
Instances For
A ball of integers L is the coordinate lattice of a multiplication matrix: the coordinate
vector of y lies in the lattice of the matrix of multiplication by z exactly when the valuation
of z is at most that of y—in the discrete valuation ring integers L divisibility is the
valuation inequality, and the ball of radius the valuation of z is the ideal generated by z.
With det_leftMulMatrix and measure_integerBox_eq_pow_mul this computes the volume of such a ball
in coordinates as 1 / q to the order of the norm of z—the step that replaces the paper's
Jacobian ([Serre 1978, Lemma 2, p.1033][Serre1978]).
The coordinate embedding of integers L into the coefficient space, in the monogenic basis
(basisOfEisenstein): the chart in which the balls of integers L become the lattices of
HaarScaling.lean.
Equations
- MassFormula.coord hπ hint hei y = MassFormula.toCoeff ((MassFormula.basisOfEisenstein hπ hint hei).equivFun y)
Instances For
A ball of integers L is a lattice in coordinates: the image under the chart of the ball of
radius the valuation of z—that is, of the ideal generated by z—is the image lattice of the
matrix of multiplication by z.
The order of the norm of the derivative #
Lemma 2 of the paper computes the Jacobian of the parametrization as a Vandermonde times the
determinant of the embeddings on a basis, and equation (11) reads off that its valuation is d L
from the fact that the square of each factor generates the discriminant. In the route of this file
no Jacobian occurs: what carries the factor 1 / q ^ d L is the lattice of multiplication by the
derivative of g at ξ, whose index is the order of the norm of that derivative—and that norm is
the discriminant of the power basis up to sign, so its order is d L by the definition of
discIdeal. Neither conjugates nor square roots enter.
The norm over 𝒪[K], computed after base change: the norm over 𝒪[K] of an element of
integers L maps to its norm over K—the two are determinants of the same multiplication, on an
𝒪[K]-basis and on its base change, and L is the localization of integers L at the
nonzerodivisors of 𝒪[K].
Lemma 2 in elementary form: the norm of the derivative of g at ξ is an associate of
π ^ d L. That norm is the discriminant of the power basis up to sign, so it generates
discIdeal (discIdeal_eq_span), whose multiplicity at 𝓂[K] is d L by definition
(associated_pow_d) ([Serre 1978, Lemma 2, eq. (11), p.1033][Serre1978]).
The norm of the Eisenstein generator is an associate of the uniformizer: it is the constant
coefficient of the minimal polynomial up to sign (PowerBasis.norm_gen_eq_coeff_zero_minpoly), and
that coefficient is an associate of π (associated_pi_coeff_zero).
The norm of a power of the Eisenstein generator is an associate of the same power of π.
The norm computes the valuation: for the totally ramified integers L over 𝒪[K], the
π-adic order of the norm of z is the valuation of z in integers L—every z is a unit times
a power of the generator, the norm of a unit is a unit, and the norm of the generator is an
associate of π. This is the classical statement that the valuation of K composed with the norm
is the valuation of L, for a totally ramified extension (cf. the header of
Discriminant.lean).
The fiber exponent is the discriminant exponent: the valuation in integers L of the derivative
of g at ξ is d L. The fiber condition of existsUnique_isRoot_iff is stated with that
valuation, while the volume of the corresponding lattice is governed by the order of its norm
(associated_norm_derivative)—and addVal_norm identifies the two.
Equation (5): the volume of the uniformizers #
The one volume of the set of uniformizers that the assembly of equation (13) needs. In the chart,
that set is the ideal generated by ξ minus the ideal generated by ξ ^ 2, the difference of two
lattices of determinant orders 1 and 2—the norms of ξ and ξ ^ 2—so their volumes are 1 / q
and 1 / q ^ 2.
The lattice of multiplication by an element has volume prescribed by its norm.
The volume of the ball of radius k of integers L in the chart is 1 / q ^ k: it is the
lattice of multiplication by ξ ^ k, whose determinant, the norm of ξ ^ k, has order k.
The uniformizers of integers L have volume (1 / q) * (1 - 1 / q) in the chart of the
monogenic basis. The set of uniformizers is the difference of the balls of radii 1 and 2, whose
volumes measure_image_coord_ball computes as 1 / q and 1 / q ^ 2
([Serre 1978, eq. (5), p.1032][Serre1978]).