The arithmetic Frobenius on roots of unity #
Let K be a number field, F an extension field of K, π a height-one prime of π K, and
Q an ideal of π F lying over π. An arithmetic Frobenius at Q is a Ο with
Ο x β‘ x ^ ππ (mod Q) for every x : π F (Mathlib's IsArithFrobAt). This file records what
such a Ο does to a root of unity: if ΞΆ is an m-th root of unity in F and π does not
divide m, then
Ο ΞΆ = ΞΆ ^ ππ.
Over β this reads ΞΆ_m β¦ ΞΆ_m ^ p, so the cyclotomic character sends the Frobenius at p to
p mod m. The exponent is ππ itself and not ππβ»ΒΉ: the inverse describes the geometric
Frobenius, and using it would reverse the arithmetic progression a character reads off.
Some hypothesis relating m to π is genuinely necessary rather than an artifact of the proof.
In the intended setting F = K(ΞΌ_m), taking ΞΌ_m β K collapses F to K, making every Ο the
identity; the formula would then force ππ β‘ 1 (mod m) for every prime. Here the hypothesis is
(m : π K) β π.asIdeal, that is π β€ m, imposed at the base prime where a caller can check
it rather than at Q.
Main results #
AlgHom.IsArithFrobAt.apply_eq_pow_absNorm_of_pow_eq_one: an arithmetic Frobenius at an ideal ofπ Foverπraises anm-th root of unity to the powerππ, whenπ β€ m.AlgHom.IsArithFrobAt.autToPow_eq_absNorm: equivalently, the cyclotomic characterIsPrimitiveRoot.autToPowsends such a Frobenius toππ mod m.TauCeti.NumberField.isArithFrobAt_iff_galEquivZMod_eq_unitOfCoprime: overβ, an automorphism is an arithmetic Frobenius at a prime abovepexactly whengalEquivZModsends it top mod n.TauCeti.NumberField.galEquivZMod_arithFrobAt_eq_unitOfCoprime: the corresponding formula for Mathlib's chosen arithmetic Frobenius.
Implementation notes #
The statement takes an element Ο together with IsArithFrobAt (π K) Ο Q rather than a chosen
Frobenius. It therefore applies to every arithmetic Frobenius at Q, needs no finiteness of the
residue ring π F β§Έ Q (which a chosen Frobenius needs in order to exist), and lets a consumer
supply whichever representative it holds.
ΞΆ is asked only for ΞΆ ^ m = 1, not for IsPrimitiveRoot ΞΆ m. Primitivity plays no part: the
underlying IsArithFrobAt.apply_of_pow_eq_one is itself stated for any root of unity, and a
caller holding hΞΆ : IsPrimitiveRoot ΞΆ m passes hΞΆ.pow_eq_one. Nor is [NeZero m] assumed β
hm already forces m β 0, since every ideal contains 0. Being a root of unity is also what
makes ΞΆ an algebraic integer here (IsIntegral.of_pow), so no cyclotomic structure is needed to
package it into π F.
The statement uses the monoid-action IsArithFrobAt, whose head symbol unfolds to
AlgHom.IsArithFrobAt; the theorem lives in that namespace so a caller can write
hΟ.apply_eq_pow_absNorm_of_pow_eq_one, matching Mathlib's own apply_of_pow_eq_one. Inside
that namespace the bare name IsArithFrobAt would resolve to the two-argument AlgHom form,
so the hypothesis names the monoid-action abbrev as _root_.IsArithFrobAt.
There is likewise no cyclotomic hypothesis on F / K. IsCyclotomicExtension {m} K F is the
ambient setting in which the result gets used, but the proof never looks at it, so assuming it
would leave an unused hypothesis on the statement. For the same reason F is not assumed to be a
number field: only K has to be one, so that π has an absolute norm. And Q, which in use is a
prime above π, is only required to lie over it: IsArithFrobAt reads as a congruence modulo Q
for any ideal, and nothing below needs Q to be prime.
References #
Adapted from cyclotomic_frobenius_acts_as_norm_power in
CebotarevDensity/CyclotomicNormResidue.lean of
CBirkbeck/chebotarev-density (Apache-2.0,
Birkbeck--Brasca) at commit 8575c9df1ae0a61120ab5c964c7911414254bec7, where the result is stated
over a source-local unramifiedness predicate and a chosen Frobenius. The mathematics is Sharifi,
Algebraic Number Theory, Proposition 7.2.1 step (i), p. 142.
An arithmetic Frobenius raises a root of unity to the norm of the prime below it. Let ΞΆ
be an m-th root of unity in an extension field F of a number field K, let π be a
height-one prime of π K not dividing m, and let Ο be an arithmetic Frobenius at an ideal
Q of π F lying over π.
Then Ο ΞΆ = ΞΆ ^ ππ.
The exponent is the absolute norm of π, not its inverse: over β this is ΞΆ_m β¦ ΞΆ_m ^ p.
The cyclotomic character of an arithmetic Frobenius is the norm. Let ΞΆ be a primitive
m-th root of unity in an extension field F of a number field K, let π be a height-one
prime of π K not dividing m, and let Ο be an arithmetic Frobenius at an ideal Q of π F
lying over π. Then the cyclotomic character IsPrimitiveRoot.autToPow sends Ο to the residue
of ππ modulo m.
This is apply_eq_pow_absNorm_of_pow_eq_one read through the character: over β it says that
the Frobenius at p corresponds to p mod m, not to its inverse.
In a cyclotomic extension, an automorphism is an arithmetic Frobenius exactly when its cyclotomic exponent is the norm of the prime below.
In a rational cyclotomic extension, the cyclotomic exponent identifies the arithmetic Frobenius at an unramified prime with the norm of the prime below it.
Cyclotomic Frobenius is the residue class of the rational prime. In a rational
cyclotomic extension of conductor n, an automorphism is an arithmetic Frobenius at a prime
above p, for p coprime to n, exactly when galEquivZMod sends it to the unit represented
by p modulo n.
This is the rational-prime form of isArithFrobAt_iff_galEquivZMod_eq_absNorm.
Mathlib's chosen arithmetic Frobenius at a prime above p in a rational cyclotomic
extension corresponds to the unit p mod n.