Chebotarev density for cyclotomic extensions

Let F = K(μ_m) be a cyclotomic extension of the number field K. For every σ ∈ Gal(F/K), the primes of 𝓞 K whose Frobenius is σ have Dirichlet density 1 / #Gal(F/K).

Main results

• NumberField.Chebotarev.hasDirichletDensity_cyclotomicFrobenius: the Frobenius fibre of any σ ∈ Gal(K(μ_m)/K) has Dirichlet density 1 / #Gal(K(μ_m)/K).
• NumberField.Chebotarev.hasDirichletDensity_frobeniusPrimeSet_galEquivZMod_symm: over ℚ, the density of the fibre tagged by any unit modulo m is 1 / φ(m).
• NumberField.Chebotarev.hasDirichletDensity_frobeniusPrimeSet_cyclotomic_five: each fibre of a fifth cyclotomic field has density 1/4.

References

• J. Neukirch, Algebraic Number Theory, Chapter VII, §13.
• The same character-orthogonality argument is formalized as Chebotarev.chebotarev_cyclotomic in AINTLIB, https://github.com/CBirkbeck/aintlib (Apache-2.0), commit 8102fa09bbf570f3e991adfdb2d6d70b48cb5b5e, file projects/Chebotarev/CebotarevDensity/Cyclotomic.lean.

theorem NumberField.Chebotarev.hasDirichletDensity_cyclotomicFrobenius (K : Type u_1) (F : Type u_2) [Field K] [NumberField K] [Field F] [NumberField F] [Algebra K F] [IsGalois K F] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} K F] (σ : Gal(F/K)) : Set.HasDirichletDensity (frobeniusPrimeSet K F (ConjClasses.mk σ)) (1 / ↑(Nat.card Gal(F/K)))

Chebotarev density for cyclotomic extensions. For F = K(μ_m) and any σ ∈ Gal(F/K), the primes of 𝓞 K whose Frobenius in F is σ have Dirichlet density 1 / #Gal(F/K).

theorem NumberField.Chebotarev.hasDirichletDensity_frobeniusPrimeSet_galEquivZMod_symm (F : Type u_3) [Field F] [NumberField F] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} ℚ F] [IsGalois ℚ F] (a : (ZMod m)ˣ) : Set.HasDirichletDensity (frobeniusPrimeSet ℚ F (ConjClasses.mk ((IsCyclotomicExtension.Rat.galEquivZMod m F).symm a))) (1 / ↑m.totient)

Over ℚ, the Frobenius fibre tagged by a unit modulo the cyclotomic level m has Dirichlet density 1 / φ(m).

theorem NumberField.Chebotarev.hasDirichletDensity_frobeniusPrimeSet_cyclotomic_five (F : Type u_3) [Field F] [NumberField F] [IsCyclotomicExtension {5} ℚ F] [IsGalois ℚ F] (a : (ZMod 5)ˣ) : Set.HasDirichletDensity (frobeniusPrimeSet ℚ F (ConjClasses.mk ((IsCyclotomicExtension.Rat.galEquivZMod 5 F).symm a))) (1 / 4)

Each of the four arithmetic Frobenius fibres of a fifth cyclotomic field has Dirichlet density 1/4.