The completely split primes have density 1 / [L : K]

Let L / K be a finite Galois extension of number fields. The primes of 𝓞 K that split completely in L — the identity fibre frobeniusPrimeSet K L 1 of the Artin class — have Dirichlet density 1 / [L : K].

For an extension E / K that need not be Galois, a prime of 𝓞 K splits completely in E exactly when it splits completely in the Galois closure N of E / K, so the primes splitting completely in E have Dirichlet density 1 / [N : K]. Here E is an intermediate field of a finite Galois extension M / K, and N is its normal closure in M.

Main results

• NumberField.Chebotarev.hasDirichletDensity_frobeniusPrimeSet_one: the completely split primes have Dirichlet density 1 / [L : K].
• NumberField.Chebotarev.hasDirichletDensity_setOf_ncard_primesOver_eq_finrank: the primes splitting completely in an intermediate field E of M / K have Dirichlet density 1 / [N : K], for N the normal closure of E in M.

References

• J. Neukirch, Algebraic Number Theory, Chapter VII, §13.

theorem NumberField.Chebotarev.hasDirichletDensity_frobeniusPrimeSet_one (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 / ↑(Module.finrank K L))

The completely split primes have density 1 / [L : K]. The primes of 𝓞 K that split completely in the finite Galois extension L have Dirichlet density 1 / [L : K]. The Chebotarev density theorem gives the same density as 1 / #Gal(L/K) (hasDirichletDensity_splitCompletely).

theorem NumberField.Chebotarev.hasDirichletDensity_setOf_ncard_primesOver_eq_finrank {K : Type u_1} [Field K] [NumberField K] {M : Type u_3} [Field M] [NumberField M] [Algebra K M] [IsGalois K M] (E : IntermediateField K M) : Set.HasDirichletDensity {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K) | (𝔭.asIdeal.primesOver (RingOfIntegers ↥E)).ncard = Module.finrank K ↥E} (1 / ↑(Module.finrank K ↥(IntermediateField.normalClosure K (↥E) M)))

The completely split primes of a non-Galois extension. Let E be an intermediate field of a finite Galois extension M / K of number fields, and let N be the normal closure of E in M, the Galois closure of E / K. The primes of 𝓞 K that split completely in E, those with [E : K] primes of 𝓞 E above them, have Dirichlet density 1 / [N : K].