The Chebotarev density theorem

Let L / K be a finite Galois extension of number fields with group G, and let C be a conjugacy class of G. The primes of 𝓞 K whose Frobenius in L lies in C have Dirichlet density #C / #G.

Main results

• NumberField.Chebotarev.hasDirichletDensity_frobeniusPrimeSet: the Chebotarev density theorem, for Dirichlet density.
• NumberField.Chebotarev.hasDirichletDensity_splitCompletely: the primes that split completely in L have Dirichlet density 1 / #Gal(L/K).
• NumberField.Chebotarev.infinite_frobeniusPrimeSet: every conjugacy class of Gal(L/K) is the Frobenius class of infinitely many primes of 𝓞 K.
• NumberField.Chebotarev.hasDirichletDensity_iff_of_finite_symmDiff_frobeniusPrimeSet: a set of primes differing from a Frobenius fibre in finitely many primes has Dirichlet density δ exactly when δ = #C / #G.

References

• R. Sharifi, Algebraic Number Theory, Theorem 7.2.2.
• J. Neukirch, Algebraic Number Theory, Chapter VII, §13.

theorem NumberField.Chebotarev.hasDirichletDensity_frobeniusPrimeSet (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)) : Set.HasDirichletDensity (frobeniusPrimeSet K L C) (↑(Nat.card ↑C.carrier) / ↑(Nat.card Gal(L/K)))

The Chebotarev density theorem. For a finite Galois extension L / K of number fields and a conjugacy class C of Gal(L/K), the primes of 𝓞 K whose Frobenius in L lies in C have Dirichlet density #C / #Gal(L/K).

theorem NumberField.Chebotarev.hasDirichletDensity_splitCompletely (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : Set.HasDirichletDensity (frobeniusPrimeSet K L 1) (1 / ↑(Nat.card Gal(L/K)))

The completely split primes have density 1 / #Gal(L/K). The primes of 𝓞 K that split completely in L, whose Frobenius class is trivial, have Dirichlet density 1 / #Gal(L/K). This is hasDirichletDensity_frobeniusPrimeSet for the class of the identity. The same density, in the form 1 / [L : K], is hasDirichletDensity_frobeniusPrimeSet_one, which is proved directly by counting primes and is used before this theorem is available.

theorem NumberField.Chebotarev.infinite_frobeniusPrimeSet (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)) : (frobeniusPrimeSet K L C).Infinite

Every Frobenius class occurs infinitely often. For every conjugacy class C of Gal(L/K), infinitely many primes of 𝓞 K are unramified in L with Frobenius class C.

theorem NumberField.Chebotarev.hasDirichletDensity_iff_of_finite_symmDiff_frobeniusPrimeSet {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {C : ConjClasses Gal(L/K)} {δ : ℝ} (hS : (symmDiff S (frobeniusPrimeSet K L C)).Finite) : Set.HasDirichletDensity S δ ↔ δ = ↑(Nat.card ↑C.carrier) / ↑(Nat.card Gal(L/K))

Chebotarev density up to finitely many primes. A set S of primes of 𝓞 K that differs from the Frobenius fibre of a conjugacy class C of Gal(L/K) in only finitely many primes has Dirichlet density δ if and only if δ = #C / #Gal(L/K).