Raising the base field: the tower formula for arithmetic Frobenius elements #
Let K โ M โ L be number fields with L / K and L / M Galois, let Q be a prime of ๐ L
unramified over ๐ K, and write ๐ = Q โฉ ๐ M and ๐ญ = Q โฉ ๐ K. An arithmetic Frobenius
ฯ โ Gal(L/K) at Q acts on the residue field by x โฆ x ^ ๐๐ญ, while an arithmetic Frobenius
ฯ โ Gal(L/M) at Q acts by x โฆ x ^ ๐๐. Since ๐๐ = ๐๐ญ ^ f(๐/๐ญ), the two are related by
AlgEquiv.restrictScalars K ฯ = ฯ ^ f(๐/๐ญ).
The exponent is a power, the residue degree of the intermediate prime over the base, and never
an inverse. In particular ฯ ^ f(๐/๐ญ) fixes M pointwise even though M / K need not be normal
and ฯ itself need not preserve M.
This is the second of the two tower laws for Frobenius elements. The first, restriction along a
normal subextension, takes no power at all and is
IsArithFrobAt.restrictNormal in TauCeti.NumberTheory.NumberField.Frobenius.Restriction.
The two hypotheses that are not decoration #
The statement is relative to one prime Q of L. Replacing ฯ by an arbitrary conjugate โ an
arbitrary representative of the Artin class of ๐ญ โ makes it false when M / K is not normal: a
conjugate need not stabilize Q, so its f-th power need not fix M pointwise, and it is then
the restriction of no element of Gal(L/M) at all.
Unramifiedness of Q over ๐ K is likewise essential. At a ramified prime a Frobenius lift is
determined only modulo inertia, so there is no equality of automorphisms to prove; the statement
would have to be made in the quotient by the inertia subgroup, or about a coset. Here
unramifiedness enters through Ideal.stabilizerHom_injective_of_isUnramifiedAt: the decomposition
group of Q embeds into the automorphism group of the residue extension, so an element of
Gal(L/K) stabilizing Q is pinned down by its residue action, and both ฯ ^ f(๐/๐ญ) and
AlgEquiv.restrictScalars K ฯ act by x โฆ x ^ ๐๐.
Main results #
NumberField.restrictScalars_eq_pow_inertiaDeg: an arithmetic Frobenius ofGal(L/M)atQrestricts to thef(๐/๐ญ)-th power of an arithmetic Frobenius ofGal(L/K)atQ.NumberField.isArithFrobAt_iff_restrictScalars_eq_pow_inertiaDeg: that power characterizes the relative Frobenius among the elements ofGal(L/M)after restriction toGal(L/K).NumberField.restrictScalars_arithFrobAt_eq_pow_inertiaDeg: the same formula for Mathlib's coherently chosenarithFrobAt, which is what the Artin symbol is built from.NumberField.exists_isArithFrobAt_pow_inertiaDeg: the existence form of the tower formula, stated for prime ideals๐and๐ญpresented by their defining equations.NumberField.pow_inertiaDeg_apply_algebraMap: thef(๐/๐ญ)-th power ofฯfixesMpointwise.NumberField.restrictScalars_eq_of_inertiaDeg_eq_one: at residue degree one the restriction of the relative Frobenius isฯitself, with no power.NumberField.isArithFrobAt_restrictScalars_of_inertiaDeg_eq_one: the same at residue degree one, concluding that the restriction is an arithmetic Frobenius rather than assuming one.NumberField.isArithFrobAt_int_of_absNorm_eq: a relative Frobenius above an ideal of absolute normpis also a Frobenius over the ideal(p)ofโค.NumberField.isArithFrobAt_one_of_pow_eq_oneandNumberField.isArithFrobAt_eq_one_of_pow_eq_one: when an absolute Frobenius atQhas order dividingnand the residue field ofQ โฉ ๐ Mhasp ^ nelements, the relative Frobenius ofGal(L/M)atQis the identity.
References #
- [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter I, ยง9.
A relative Frobenius above an ideal of norm p is a Frobenius over (p).
Let P be an ideal of a number field K above (p) with absolute norm p. If Q lies above
P, then a Frobenius at Q relative to K is also a Frobenius relative to โค after
restricting its automorphism from K-linearity to โ-linearity.
The norm equality makes the two residue cardinalities in the definitions equal; no primality
hypothesis on p, P, or Q is required.
Raising the base field raises the Frobenius to the residue degree. For number fields
K โ M โ L with L / K and L / M Galois and Q a prime of ๐ L unramified over ๐ K, the
restriction to Gal(L/K) of an arithmetic Frobenius ฯ โ Gal(L/M) at Q is the
f(๐/๐ญ)-th power of an arithmetic Frobenius ฯ โ Gal(L/K) at Q, where
๐ = Q โฉ ๐ M and ๐ญ = Q โฉ ๐ K.
The exponent is the residue degree of ๐ over ๐ K, and it is a power: the residue field of ๐
has ๐๐ญ ^ f(๐/๐ญ) elements, so the two Frobenius elements have residue actions x โฆ x ^ ๐๐ญ and
x โฆ x ^ ๐๐ญ ^ f(๐/๐ญ). Both sides are read inside Gal(L/K), where ฯ is placed by
AlgEquiv.restrictScalars.
The relative Frobenius restricts to exactly that power. An element of Gal(L/M) is an
arithmetic Frobenius at Q precisely when its restriction to Gal(L/K) is the
f(๐/๐ญ)-th power of a fixed arithmetic Frobenius ฯ โ Gal(L/K) at Q.
The converse direction is uniqueness rather than a second computation: a Frobenius of Gal(L/M)
at Q exists, is carried to ฯ ^ f(๐/๐ญ) by restrictScalars_eq_pow_inertiaDeg, and
AlgEquiv.restrictScalars is injective.
The tower formula for Mathlib's chosen Frobenius. Mathlib's arithFrobAt picks a
Frobenius coherently across the fibre above a prime of the base; at an unramified Q the choices
over ๐ K and over ๐ M are related by the tower formula, because at such a Q there is
nothing left to choose.
This is the form the Artin symbol is built from, NumberField.artinSymbol being the conjugacy
class of arithFrobAt (๐ K) (L โโ[K] L) at a prime above ๐ญ.
The tower formula, in the form the Artin symbol consumes. For number fields K โ M โ L
with L / K and L / M Galois, a prime Q of ๐ L with ๐ = Q โฉ ๐ M and ๐ญ = Q โฉ ๐ K, and
๐ญ unramified in L, every arithmetic Frobenius ฯ โ Gal(L/K) at Q has ฯ ^ f(๐/๐ญ) as the
image in Gal(L/K) of an arithmetic Frobenius at Q in Gal(L/M).
The unramifiedness hypothesis is phrased for all primes above ๐ญ, matching the argument that
NumberField.artinSymbol takes; only its value at Q is used.
The power of the Frobenius fixes the intermediate field. Even though M / K need not be
normal, and ฯ therefore need not preserve M, its f(๐/๐ญ)-th power fixes M pointwise: it is
the image of an element of Gal(L/M).
At residue degree one the restricted Frobenius does not move. If ๐ = Q โฉ ๐ M has
residue degree one over ๐ K, then the restriction to Gal(L/K) of an arithmetic Frobenius of
Gal(L/M) at Q is the arithmetic Frobenius of Gal(L/K) at Q itself.
This is the case a fixed-field fibre count runs through: it contracts the primes of M whose
residue degree over K is one, exactly so that the restriction of the relative Frobenius is the
absolute one.
A relative Frobenius at residue degree one restricts to an absolute one. If Q โฉ ๐ M
has residue degree one over ๐ K, then the restriction to Gal(L/K) of an arithmetic Frobenius
of Gal(L/M) at Q is itself an arithmetic Frobenius at Q over ๐ K.
Residue degree one says the two residue fields have the same size, and restricting scalars does
not move the automorphism, so the two Frobenius conditions are the same condition. Neither
L / K Galois nor Q unramified is needed: this is a statement about Q alone.
Trivial relative Frobenius elements #
A prime that is already inert enough over โ has trivial relative Frobenius: if the absolute
Frobenius ฯ at Q has ฯ ^ n = 1 and the residue field of Q โฉ ๐ M has p ^ n elements, then
the residue action of the relative Frobenius, raising to the power p ^ n, is the identity.
The identity is a relative Frobenius at a prime whose base residue field absorbs the
absolute one. With M โ L number fields, Q a prime of ๐ L above the rational prime p, and
ฯ โ Gal(L/โ) an arithmetic Frobenius at Q over โค with ฯ ^ n = 1, the residue field of
Q โฉ ๐ M having p ^ n elements forces the relative residue action x โฆ x ^ p ^ n to be the
identity.
The relative Frobenius is trivial at such a prime. Under the hypotheses of
NumberField.isArithFrobAt_one_of_pow_eq_one, and with L / M unramified at Q, every
arithmetic Frobenius of Gal(L/M) at Q is the identity. No normality hypothesis on L/M
is needed.