Chebotarev density for abelian extensions

Let L / K be a finite Galois extension of number fields with abelian group G. For every σ ∈ G, the primes of 𝓞 K whose Frobenius in L is σ have Dirichlet density 1 / #G.

Main results

• NumberField.Chebotarev.hasDirichletDensity_abelianFrobenius: the Frobenius fibre of any element of an abelian Galois group G has Dirichlet density 1 / #G.

References

• R. Sharifi, Algebraic Number Theory, Theorem 7.2.2.
• J. Neukirch, Algebraic Number Theory, Chapter VII, Section 13.
• The same Deuring crossing argument is formalized as Chebotarev.chebotarev_abelian in AINTLIB, https://github.com/CBirkbeck/aintlib (Apache-2.0), commit 8102fa09bbf570f3e991adfdb2d6d70b48cb5b5e, file projects/Chebotarev/CebotarevDensity/Abelian.lean.

theorem NumberField.Chebotarev.hasDirichletDensity_abelianFrobenius (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)) : Set.HasDirichletDensity (frobeniusPrimeSet K L (ConjClasses.mk σ)) (1 / ↑(Nat.card Gal(L/K)))

Chebotarev density for abelian extensions. If Gal(L/K) is abelian, then for every σ ∈ Gal(L/K) the primes of 𝓞 K whose Frobenius in L is σ have Dirichlet density 1 / #Gal(L/K).