Chebotarev density for splitting types in nonnormal extensions

For any intermediate extension E/K of a finite Galois extension L/K, its splitting type at a prime of K is the multiset of residue degrees of the primes of E above it. Outside the primes ramified in L, this is the full cycle type of Frobenius on Gal(L/K) ⧸ Gal(L/E). Consequently the primes with a prescribed multiset μ have Dirichlet density equal to the sum of #C / #Gal(L/K) over the conjugacy classes whose coset permutations have full cycle type μ.

The multiset records the entire splitting pattern, including multiplicities and degrees equal to one. The intermediate extension need not be normal: any finite separable extension can be realized inside its Galois closure. The density theorem includes ramified primes satisfying the same residue-degree condition; they do not change the density since only finitely many primes ramify in the Galois extension.

The arithmetic dictionary is Ideal.fullCycleType_toPerm_quotient_eq_map_inertiaDeg. The density calculation uses hasDirichletDensity_frobeniusPrimeSet, finite disjoint-union additivity, and finite symmetric-difference invariance, without any additional analytic argument.

References

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

theorem NumberField.Chebotarev.map_inertiaDeg_eq_fullCycleType_of_mem_frobeniusPrimeSet (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (E : IntermediateField K L) {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)} {σ : Gal(L/K)} (h𝔭 : 𝔭 ∈ frobeniusPrimeSet K L (ConjClasses.mk σ)) : Multiset.map (fun (P : ↑(𝔭.asIdeal.primesOver (RingOfIntegers ↥E))) => (↑P).inertiaDeg (RingOfIntegers K)) Finset.univ.val = (MulAction.toPerm σ).fullCycleType

At a prime in a Frobenius fibre, the residue-degree multiset in the fixed field equals the full cycle type of every representative of that class acting on Galois cosets.

theorem NumberField.Chebotarev.setOf_map_inertiaDeg_eq_sdiff_ramifiedPrimes (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (E : IntermediateField K L) (μ : Multiset ℕ) : {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K) | Multiset.map (fun (P : ↑(𝔭.asIdeal.primesOver (RingOfIntegers ↥E))) => (↑P).inertiaDeg (RingOfIntegers K)) Finset.univ.val = μ} \ ↑(ramifiedPrimes K L) = ⋃ C ∈ {C : ConjClasses Gal(L/K) | (MulAction.toPerm (Quotient.out C)).fullCycleType = μ}, frobeniusPrimeSet K L C

Outside ramification in the Galois extension, a splitting-type condition is exactly a disjoint union of Frobenius fibres. Fixed points and repeated cycle lengths are retained.

theorem NumberField.Chebotarev.hasDirichletDensity_setOf_map_inertiaDeg_eq (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (E : IntermediateField K L) (μ : Multiset ℕ) : Set.HasDirichletDensity {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K) | Multiset.map (fun (P : ↑(𝔭.asIdeal.primesOver (RingOfIntegers ↥E))) => (↑P).inertiaDeg (RingOfIntegers K)) Finset.univ.val = μ} (∑ C : ConjClasses Gal(L/K) with (MulAction.toPerm (Quotient.out C)).fullCycleType = μ, ↑(Nat.card ↑C.carrier) / ↑(Nat.card Gal(L/K)))

Non-Galois Chebotarev for splitting types. The primes with residue-degree multiset μ in E have density the total proportion of elements whose action on Gal(L/K) ⧸ Gal(L/E) has full cycle type μ, expressed as a sum of conjugacy-class proportions. No normality of E/K or realizability hypothesis on μ is needed.