Frobenius fibers over cyclic fixed fields #
Let L / K be a finite Galois extension, let C be a conjugacy class in Gal(L/K), and choose
sigma in C. Put E = L ^ <sigma>. This file counts the primes of E over a prime in the
Frobenius class C whose relative Frobenius in L / E is the automorphism induced by sigma:
#G / (#C * orderOf sigma).
Contraction identifies these primes with the primes of L at which sigma itself is an
arithmetic Frobenius. The count is proved for any tau in Gal(L/E) that lies in C when read
over K, among the primes of E of residue degree one over K: the primes of L above p at
which tau is the arithmetic Frobenius form one orbit under the centralizer of tau, and since
Gal(L/E) is abelian of order orderOf sigma, each of their contractions to E lies below
orderOf sigma / orderOf tau of them. For tau = sigma the residue-degree condition is
automatic. The resulting count is the fixed-field multiplicity used when transferring prime
sums and densities between E and K.
Main results #
NumberField.Chebotarev.fixedField_frobenius_fiber_eq_image: contraction identifies the relative fiber with the image of the corresponding absolute Frobenius fiber.NumberField.Chebotarev.inertiaDeg_eq_one_iff_under_mem_frobeniusPrimeSet: away from the ramified primes, a prime of the relative fiber has residue degree one overKexactly when the prime below it lies in the Frobenius fiber ofsigma.NumberField.Chebotarev.fixedField_frobenius_fiber_card: the exact cardinality of the relative Frobenius fiber over one prime ofK.NumberField.Chebotarev.fixedField_frobenius_fiber_inertiaDeg_eq_one_card_mul: the same count for the residue-degree-one primes whose relative Frobenius is any given element of⟨sigma⟩.NumberField.Chebotarev.fixedField_frobenius_pow_fiber_card: the powered fibre count, of the residue-degree-one primes whose relative Frobenius hasm-th powersigma.
References #
- J. Neukirch, Algebraic Number Theory, Chapter I, Section 9.
- R. Sharifi, Algebraic Number Theory, Theorem 7.2.2.
- C. Birkbeck and R. Brasca,
Chebotarev density,
CebotarevDensity/FixedFieldDensity.leanat commit55a89985d47a3befcf6069aca1da250ff088b5c7(Apache-2.0).
Contraction identifies the fixed-field and absolute Frobenius fibers. Over a prime p
with Artin class represented by sigma, contraction from L to L ^ <sigma> carries exactly the
primes whose absolute Frobenius is sigma onto the primes whose relative Artin class is represented
by sigma.toFixedFieldAlgEquiv.
Residue degree one detects the absolute Frobenius class below a relative fiber. Let P
be a prime of L ^ <sigma> whose relative Artin class in L / L ^ <sigma> is represented by
sigma.toFixedFieldAlgEquiv, and suppose that the prime of K below P is unramified in L.
Then P has residue degree one over K exactly when the prime below it has Artin class [sigma].
Membership of P in the relative fiber does not by itself fix the class below. If L / K is
cyclic of degree four with generator g and sigma = g ^ 2, a prime of K with Frobenius g is
inert in L ^ <g ^ 2>, and the prime above it has relative Frobenius g ^ 2.
The unramifiedness hypothesis cannot be dropped. For K = ℚ, L = ℚ(∛2, ζ₃) and sigma a
transposition, the prime 𝔓 of ℚ(∛2) above 2 has residue degree one and relative Frobenius
sigma, although 2 ramifies in L and so has no Artin class.
Conversely, a prime of K in the class of sigma can have primes of residue degree one above it
whose relative Frobenius is another generator of <sigma>; fixedField_frobenius_fiber_card
counts those whose relative Frobenius is sigma.
Residue-degree-one fibres of the elements of ⟨σ⟩ #
The residue-degree-one fibre of one element of ⟨σ⟩, counted. Let p be a prime of K
with Artin class C, and let τ be an automorphism of L over E = L ^ ⟨σ⟩ that, read over
K, lies in C. Then the primes P of E above p with residue degree one over K and
relative Frobenius τ in L / E number #Gal(L/K) / (#C * orderOf σ); this is stated
division-free.
For τ = σ.toFixedFieldAlgEquiv the residue-degree condition is automatic, and the quotient form
is fixedField_frobenius_fiber_card.
The fixed-field Frobenius fiber count. Let sigma represent the conjugacy class C, and
let p be an unramified prime with Artin class C. The number of primes of
L ^ <sigma> above p whose relative Artin class in L / L ^ <sigma> is represented by
sigma.toFixedFieldAlgEquiv is
#Gal(L/K) / (#C * orderOf sigma).
The division is exact by ConjClasses.card_carrier_mul_orderOf_dvd.
Powered fibres #
The powered fibre count of the fixed-field contraction. Let p be a prime of K with
Artin class C, let σ ∈ Gal(L/K) and E = L ^ ⟨σ⟩, and let m be a natural number. The primes
P of E above p of residue degree one over K whose relative Frobenius Frob_{L/E}(P)
satisfies Frob_{L/E}(P) ^ m = σ number
#{w ∈ C ∩ ⟨σ⟩ | w ^ m = σ} * #Gal(L/K) / (#C * orderOf σ).
This is stated division-free; fixedField_frobenius_pow_fiber_card is the quotient form.
For m ≥ 2 the count is supported on the classes C containing an m-th root of σ in ⟨σ⟩,
which in general are not the class of σ: in a cyclic extension of degree five with generator
g, a prime with Frobenius g ^ 3 contributes to the fibre of g at m = 2, since
(g ^ 3) ^ 2 = g. This is why the ψ-transfer of the Chebotarev density theorem goes through
ϑ, with the prime powers removed on both sides first.
The relative Galois group Gal(L/E) is cyclic, so the relative Frobenius of P is a single
element, recorded as the τ with P ∈ frobeniusPrimeSet E L [τ].
The powered fibre count, as a quotient. The number of primes of L ^ ⟨σ⟩ above p, of
residue degree one over K, whose relative Frobenius has m-th power σ, is
#{w ∈ C ∩ ⟨σ⟩ | w ^ m = σ} * #Gal(L/K) / (#C * orderOf σ) for the Artin class C of p. The
division is exact by fixedField_frobenius_pow_fiber_card_mul.