The Frobenius ψ fibres partition Chebyshev's ψ

Let L / K be a finite Galois extension of number fields with group G. A prime power 𝔭 ^ j with 𝔭 unramified in L lies in the powered Frobenius fibre of exactly one conjugacy class of G, namely (artinSymbol 𝔭) ^ j, and a prime power based at a ramified prime lies in none. So the Frobenius ψ functions of all conjugacy classes add up to Chebyshev's ψ of K with the ramified primes removed:

∑_C ψ_C(x) + ψ_{ramifiedPrimes K L}(x) = ψ_K(x),

and the correction is O(log x) because the ramified set is finite.

These identities supply the partition input for the weighted crossing. The later squeeze also requires the cyclotomic weighted theorem and its consequence ψ_K(x) / x → 1.

Main results

• NumberField.Chebotarev.sum_frobeniusPrimePowerWeight: at a single prime power, the Frobenius weights of all classes add up to the von Mangoldt weight if the base is unramified, and to 0 otherwise.
• NumberField.Chebotarev.sum_frobeniusPsi_add_primePsi_ramifiedPrimes: the Frobenius ψ functions and ψ of the ramified primes add up to ψ_K.
• NumberField.Chebotarev.primePsi_univ_sub_sum_frobeniusPsi_isBigO_log: the Frobenius ψ functions account for ψ_K up to O(log x).

References

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

theorem NumberField.Chebotarev.sum_frobeniusPrimePowerWeight (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (A : TauCeti.IdealPrimePower K) : ∑ C : ConjClasses Gal(L/K), frobeniusPrimePowerWeight K L C A = {B : TauCeti.IdealPrimePower K | TauCeti.primePowerBase B ∉ ramifiedPrimes K L}.indicator TauCeti.primePowerWeight A

The Frobenius weights partition the von Mangoldt weight. At a prime power 𝔭 ^ j, the powered Frobenius weights of all conjugacy classes add up to log N𝔭 when 𝔭 is unramified in L, the only nonzero term being that of (artinSymbol 𝔭) ^ j, and to 0 when 𝔭 ramifies.

theorem NumberField.Chebotarev.sum_frobeniusPsi_add_primePsi_ramifiedPrimes (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (x : ℝ) : ∑ C : ConjClasses Gal(L/K), frobeniusPsi K L C x + TauCeti.primePsi K (↑(ramifiedPrimes K L)) x = TauCeti.primePsi K Set.univ x

The Frobenius ψ fibres partition Chebyshev's ψ. Summed over all conjugacy classes of Gal(L/K), the Frobenius ψ functions count every prime power based at a prime unramified in L exactly once; adding ψ of the finite set ramifiedPrimes K L gives ψ_K.

theorem NumberField.Chebotarev.primePsi_univ_sub_sum_frobeniusPsi_isBigO_log (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : (fun (x : ℝ) => TauCeti.primePsi K Set.univ x - ∑ C : ConjClasses Gal(L/K), frobeniusPsi K L C x) =O[Filter.atTop] Real.log

The Frobenius ψ fibres account for ψ_K up to O(log x). The only prime powers missed by all Frobenius fibres are those based at the finitely many primes of ramifiedPrimes K L.