Dirichlet density across a cyclic fixed field

Let L / K be a finite Galois extension with group G, let C be a conjugacy class in G and sigma a member of it, and put E = L ^ <sigma>. This file transfers Dirichlet density between the relative Frobenius fibre of sigma over E and the Frobenius fibre of C over K.

Contraction is exact away from the finitely many ramified primes: each prime of K in the class C carries exactly #G / (#C * orderOf sigma) primes of E in the relative fibre, and those are precisely the primes of the relative fibre with residue degree one over K. Feeding that count to the generic density contraction gives

density_E (relative fibre) = δ
  ↔  density_K (frobeniusPrimeSet K L C) = δ * #C * orderOf sigma / #G.

The point of the equivalence is the direction that reduces the general case to a cyclic one: Gal(L/E) is generated by sigma, so the relative fibre is a fibre in a cyclic extension, where the density 1 / orderOf sigma is what a cyclic Chebotarev theorem delivers. Specialising to that value gives #C / #G over K, which is the Chebotarev value. No analytic input enters here — the transfer is exact, and only the cyclic density it consumes is analytic.

Main results

• NumberField.Chebotarev.hasDirichletDensity_frobeniusPrimeSet_fixedField_iff: the transfer, as an iff.
• NumberField.Chebotarev.hasDirichletDensity_frobeniusPrimeSet_of_fixedField: its specialisation at 1 / orderOf sigma, landing the value #C / #G.

References

• R. Sharifi, Algebraic Number Theory, Theorem 7.2.2, Step 1.
• J. Neukirch, Algebraic Number Theory, Chapter VII, Section 13.
• C. Birkbeck and R. Brasca, Chebotarev density, CebotarevDensity/FixedFieldDensity.lean, theorem density_lift_through_fixedField, at commit 8575c9df1ae0a61120ab5c964c7911414254bec7 (Apache-2.0). The statement follows that theorem; the proof here assembles results this repository already had.

theorem NumberField.Chebotarev.hasDirichletDensity_frobeniusPrimeSet_fixedField_iff {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)) (sigma : Gal(L/K)) (hsigma : sigma ∈ C.carrier) {δ : ℝ} : Set.HasDirichletDensity (frobeniusPrimeSet (↥(IntermediateField.fixedField (Subgroup.zpowers sigma))) L (ConjClasses.mk sigma.toFixedFieldAlgEquiv)) δ ↔ Set.HasDirichletDensity (frobeniusPrimeSet K L C) (δ / ↑(Nat.card Gal(L/K) / (Nat.card ↑C.carrier * orderOf sigma)))

Dirichlet density across the cyclic fixed field. Let sigma represent the conjugacy class C and put E = L ^ <sigma>. The relative Frobenius fibre of sigma.toFixedFieldAlgEquiv over E has Dirichlet density δ exactly when the Frobenius fibre of C over K has density δ / (#G / (#C * orderOf sigma)).

theorem NumberField.Chebotarev.hasDirichletDensity_frobeniusPrimeSet_of_fixedField {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)) (sigma : Gal(L/K)) (hsigma : sigma ∈ C.carrier) (h : Set.HasDirichletDensity (frobeniusPrimeSet (↥(IntermediateField.fixedField (Subgroup.zpowers sigma))) L (ConjClasses.mk sigma.toFixedFieldAlgEquiv)) (1 / ↑(orderOf sigma))) : Set.HasDirichletDensity (frobeniusPrimeSet K L C) (↑(Nat.card ↑C.carrier) / ↑(Nat.card Gal(L/K)))

Chebotarev's value, from the cyclic fibre. If the relative Frobenius fibre of sigma over E = L ^ <sigma> has the density 1 / orderOf sigma that a cyclic extension gives, then the Frobenius fibre of C over K has density #C / #G.

This is the contraction half of the Chebotarev density theorem: it carries a density statement about the cyclic extension L / E down to the general conjugacy class over K, and it is the only step of that reduction.