Contracting Frobenius ϑ and ψ from a cyclic fixed field

Let L / K be a finite Galois extension of number fields, let C be a conjugacy class of Gal(L/K), choose sigma ∈ C, and put E = L ^ <sigma>. This file proves the exact identity

∑_{𝔓 ∈ S_E, N 𝔓 ≤ x} log N 𝔓 = (#G / (#C * orderOf sigma)) * ϑ_C(x),

where S_E is the set of primes 𝔓 of E whose relative Artin class in L / E is represented by sigma, that do not lie above ramifiedPrimes K L, and that have residue degree one over K.

There is no error term. Away from the ramified primes, a prime 𝔓 of the relative fibre has residue degree one over K exactly when the prime 𝔭 of K below it lies in the Frobenius fibre of C (NumberField.Chebotarev.inertiaDeg_eq_one_iff_under_mem_frobeniusPrimeSet); then N 𝔓 = N 𝔭, and over each such 𝔭 there are exactly #G / (#C * orderOf sigma) of them (NumberField.Chebotarev.fixedField_frobenius_fiber_card).

The identity concerns ϑ at residue degree one only. The other primes of the relative fibre have residue degree at least two over ℚ or lie above ramifiedPrimes K L, so they are majorized by the unrestricted sums appearing in NumberField.Chebotarev.frobeniusDiscard_isLittleO over L ^ <sigma>. In general there is no such identity for ψ: a prime power 𝔓 ^ m with m ≥ 2 is selected by the m-th power of its Frobenius, and the prime of K below it need not have class C. So the transfer of ψ is only asymptotic,

ψ_sigma^{L/E}(x) = (#G / (#C * orderOf sigma)) * ψ_C^{L/K}(x) + o(x),

obtained by removing the prime powers with m ≥ 2 on both sides, applying the exact identity to what remains, and discarding the relative primes of higher residue degree or above ramifiedPrimes K L.

Main results

• NumberField.Chebotarev.primeTheta_fixedField_eq_mul_frobeniusTheta: the residue-degree-one part of the relative Frobenius ϑ over L ^ <sigma>, away from the primes above ramifiedPrimes K L, is the fixed-field multiplicity times frobeniusTheta K L C.
• NumberField.Chebotarev.frobeniusPsi_fixedField_sub_mul_frobeniusPsi_isLittleO: the relative Frobenius ψ of sigma over L ^ <sigma> is the fixed-field multiplicity times frobeniusPsi K L C, up to o(x).
• NumberField.Chebotarev.frobeniusPsi_fixedField_asymptotic_iff: hence the relative Frobenius ψ of sigma is δ x + o(x) exactly when frobeniusPsi K L C is δ x + o(x) divided by the fixed-field multiplicity.
• NumberField.Chebotarev.frobeniusPsi_asymptotic_of_fixedField: its specialisation at the cyclic value δ = 1 / orderOf sigma, which lands the Chebotarev value #C / #G over K.

References

• J. Neukirch, Algebraic Number Theory, Chapter VII, §13.
• S. Lang, Algebraic Number Theory, Chapter I, §5.

theorem NumberField.Chebotarev.primeTheta_fixedField_eq_mul_frobeniusTheta {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (C : ConjClasses Gal(L/K)) (sigma : Gal(L/K)) (hsigma : sigma ∈ C.carrier) (x : ℝ) : TauCeti.primeTheta ↥(IntermediateField.fixedField (Subgroup.zpowers sigma)) {P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers ↥(IntermediateField.fixedField (Subgroup.zpowers sigma))) | P ∈ frobeniusPrimeSet (↥(IntermediateField.fixedField (Subgroup.zpowers sigma))) L (ConjClasses.mk sigma.toFixedFieldAlgEquiv) ∧ P ∉ primesAboveRamifiedPrimes K L ↥(IntermediateField.fixedField (Subgroup.zpowers sigma)) ∧ P.asIdeal.inertiaDeg (RingOfIntegers K) = 1} x = ↑(Nat.card Gal(L/K) / (Nat.card ↑C.carrier * orderOf sigma)) * frobeniusTheta K L C x

The exact residue-degree-one contraction of Frobenius ϑ. Let sigma represent C and let E = L ^ <sigma>. Sum log N 𝔓 over the primes 𝔓 of E of norm at most x whose relative Artin class in L / E is represented by sigma.toFixedFieldAlgEquiv, that do not lie above a prime of K ramified in L, and that have residue degree one over K. The result is exactly

(#Gal(L/K) / (#C * orderOf sigma)) * frobeniusTheta K L C x.

The natural-number division is exact by ConjClasses.card_carrier_mul_orderOf_dvd.

theorem NumberField.Chebotarev.frobeniusPsi_fixedField_sub_mul_frobeniusPsi_isLittleO {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (C : ConjClasses Gal(L/K)) (sigma : Gal(L/K)) (hsigma : sigma ∈ C.carrier) : (fun (x : ℝ) => frobeniusPsi (↥(IntermediateField.fixedField (Subgroup.zpowers sigma))) L (ConjClasses.mk sigma.toFixedFieldAlgEquiv) x - ↑(Nat.card Gal(L/K) / (Nat.card ↑C.carrier * orderOf sigma)) * frobeniusPsi K L C x) =o[Filter.atTop] fun (x : ℝ) => x

The weighted contraction of Frobenius ψ. Let sigma represent C and let E = L ^ <sigma>. The relative Frobenius ψ of sigma in L / E is the fixed-field multiplicity #Gal(L/K) / (#C * orderOf sigma) times frobeniusPsi K L C, up to o(x).

Unlike primeTheta_fixedField_eq_mul_frobeniusTheta, this is not an identity: the error collects the prime powers with exponent at least two on both sides, the relative primes of residue degree above one over K, and the relative primes above ramifiedPrimes K L.

theorem NumberField.Chebotarev.frobeniusPsi_fixedField_asymptotic_iff {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (C : ConjClasses Gal(L/K)) (sigma : Gal(L/K)) (hsigma : sigma ∈ C.carrier) {δ : ℝ} : ((fun (x : ℝ) => frobeniusPsi (↥(IntermediateField.fixedField (Subgroup.zpowers sigma))) L (ConjClasses.mk sigma.toFixedFieldAlgEquiv) x - δ * x) =o[Filter.atTop] fun (x : ℝ) => x) ↔ (fun (x : ℝ) => frobeniusPsi K L C x - δ / ↑(Nat.card Gal(L/K) / (Nat.card ↑C.carrier * orderOf sigma)) * x) =o[Filter.atTop] fun (x : ℝ) => x

Linear asymptotics of Frobenius ψ across the cyclic fixed field. Let sigma represent C and put E = L ^ <sigma>. The relative Frobenius ψ of sigma.toFixedFieldAlgEquiv over E is δ x + o(x) exactly when frobeniusPsi K L C is (δ / (#G / (#C * orderOf sigma))) x + o(x).

This is the weighted counterpart of hasDirichletDensity_frobeniusPrimeSet_fixedField_iff. It carries an asymptotic for the fibre of sigma in the cyclic extension L / E down to the class C over K, and conversely.

theorem NumberField.Chebotarev.frobeniusPsi_asymptotic_of_fixedField {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (C : ConjClasses Gal(L/K)) (sigma : Gal(L/K)) (hsigma : sigma ∈ C.carrier) (h : (fun (x : ℝ) => frobeniusPsi (↥(IntermediateField.fixedField (Subgroup.zpowers sigma))) L (ConjClasses.mk sigma.toFixedFieldAlgEquiv) x - 1 / ↑(orderOf sigma) * x) =o[Filter.atTop] fun (x : ℝ) => x) : (fun (x : ℝ) => frobeniusPsi K L C x - ↑(Nat.card ↑C.carrier) / ↑(Nat.card Gal(L/K)) * x) =o[Filter.atTop] fun (x : ℝ) => x

Chebotarev's weighted value, from the cyclic fibre. If the relative Frobenius ψ of sigma over E = L ^ <sigma> is x / orderOf sigma + o(x), the value for a fibre of the cyclic extension L / E of degree orderOf sigma, then frobeniusPsi K L C x = (#C / #G) x + o(x).

This is the weighted counterpart of hasDirichletDensity_frobeniusPrimeSet_of_fixedField: it reduces the prime-number-theorem form of Chebotarev for an arbitrary class to the cyclic extension L / E.