The Chebotarev density theorem, for Chebyshev's ψ

Let L / K be a finite Galois extension of number fields with group G, and let C be a conjugacy class of G. This file proves the prime-number-theorem form of Chebotarev's theorem,

ψ_C(x) = (#C / #G) x + o(x),

where ψ_C = frobeniusPsi K L C sums log N𝔭 over the prime powers 𝔭 ^ j of K with 𝔭 unramified in L and Frob(𝔭) ^ j ∈ C.

The proof is the weighted form of the cyclotomic crossing behind NumberField.Chebotarev.hasDirichletDensity_frobeniusPrimeSet; in particular, the tagged-class crossing follows the proof of NumberField.Chebotarev.hasDirichletDensity_abelianFrobenius.

• For abelian G and σ ∈ G of order f, pick an auxiliary prime q with f ^ r ∣ q - 1 and cross with M = L(μ_q), so that Gal(M/K) ≃ G × (ZMod q)ˣ. For each tag τ with f ∣ orderOf τ, the field E_τ fixed by (σ, τ) has M as a q-th cyclotomic extension, so the cyclotomic weighted theorem over E_τ and the contraction across the cyclic fixed field give ψ_{(σ, τ)}(x) = x / #Gal(M/K) + o(x) over K. The tagged classes are distinct classes over the class of σ, so their ψ functions add up to at most ψ_σ: for a fixed q, the limit in x gives liminf ψ_σ(x) / x ≥ (1 - 2 ^ (-r)) ^ #f.primeFactors / #G, and only then does r grow, giving liminf ψ_σ(x) / x ≥ 1 / #G.
• Summing the cyclotomic weighted theorem over the Galois group of K(μ₃)/K and restoring its finitely many ramified primes gives ψ_K(x) = x + o(x). The ψ functions of all classes of Gal(L/K) account for this total up to O(log x), so their lower bounds saturate the total and each of them is the limit.
• For a general class C ∋ σ, the extension L / L ^ ⟨σ⟩ is cyclic, and the contraction across the cyclic fixed field carries the abelian result down to C.

Main results

• NumberField.Chebotarev.frobeniusPsi_asymptotic_of_mul_comm: for abelian G and σ ∈ G, ψ_σ(x) = x / #G + o(x).
• NumberField.Chebotarev.frobeniusPsi_asymptotic: for every conjugacy class C of G, ψ_C(x) = (#C / #G) x + o(x).
• NumberField.Chebotarev.tendsto_frobeniusPsi: the same, as ψ_C(x) / x → #C / #G.

References

• J. Neukirch, Algebraic Number Theory, Chapter VII, §13.
• S. Lang, Algebraic Number Theory, Chapter XV.
• H. W. Lenstra Jr. and P. Stevenhagen, "Chebotarëv and his density theorem", Math. Intelligencer 18 (1996), 26–37, for the cyclotomic crossing.

theorem NumberField.Chebotarev.frobeniusPsi_asymptotic_of_mul_comm {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (hab : ∀ (σ τ : Gal(L/K)), σ * τ = τ * σ) (σ : Gal(L/K)) : (fun (x : ℝ) => frobeniusPsi K L (ConjClasses.mk σ) x - 1 / ↑(Nat.card Gal(L/K)) * x) =o[Filter.atTop] fun (x : ℝ) => x

Weighted Chebotarev for abelian extensions. If Gal(L/K) is abelian, then for every σ ∈ Gal(L/K) the Frobenius ψ function of σ satisfies ψ_σ(x) = x / #Gal(L/K) + o(x).

theorem NumberField.Chebotarev.frobeniusPsi_asymptotic (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)) : (fun (x : ℝ) => frobeniusPsi K L C x - ↑(Nat.card ↑C.carrier) / ↑(Nat.card Gal(L/K)) * x) =o[Filter.atTop] fun (x : ℝ) => x

The Chebotarev density theorem, for Chebyshev's ψ. For a finite Galois extension L / K of number fields and a conjugacy class C of Gal(L/K), the Frobenius ψ function of C satisfies ψ_C(x) = (#C / #Gal(L/K)) x + o(x).

theorem NumberField.Chebotarev.tendsto_frobeniusPsi (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)) : Filter.Tendsto (fun (x : ℝ) => frobeniusPsi K L C x / x) Filter.atTop (nhds (↑(Nat.card ↑C.carrier) / ↑(Nat.card Gal(L/K))))

The Chebotarev density theorem, for Chebyshev's ψ, as a limit. For a finite Galois extension L / K of number fields and a conjugacy class C of Gal(L/K), ψ_C(x) / x → #C / #Gal(L/K).