Prime sums of Galois characters

For a finite Galois extension L / K of number fields and a character χ of Gal(L/K), the prime sum P_χ(t) = ∑_𝔭 χ(Frob 𝔭) N𝔭^{-t} of the ideal weight MonoidHom.galoisCharacterWeight χ is the input to character-sum proofs of Chebotarev density. This file records how these prime sums combine. When Gal(L/K) is abelian, character orthogonality turns ∑_χ χ(σ)⁻¹ P_χ(t) into #Gal(L/K) times the prime zeta sum over the Frobenius fibre of σ. The trivial character contributes the prime zeta sum over the unramified primes.

Main results

• AlgEquiv.sum_inv_mul_galoisCharacterWeight_apply_eq_ite: character orthogonality at every height-one prime, ramified or not.
• MonoidHom.primeSum_galoisCharacterWeight_one: the prime sum of the trivial character is the prime zeta sum over the unramified primes.
• AlgEquiv.natCard_mul_primeIdealZetaSum_frobeniusPrimeSet: for t > 1, #Gal(L/K) times the prime zeta sum over the Frobenius fibre of σ is ∑_χ χ(σ)⁻¹ P_χ(t).

theorem MonoidHom.primeSum_galoisCharacterWeight_one (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (t : ℝ) : (galoisCharacterWeight 1).primeSum ↑t = ↑(NumberField.Set.primeIdealZetaSum (↑(NumberField.Chebotarev.ramifiedPrimes K L))ᶜ t)

The prime sum of the trivial character is the prime zeta sum over the unramified primes.

theorem AlgEquiv.sum_inv_mul_galoisCharacterWeight_apply_eq_ite {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsMulCommutative Gal(L/K)] (σ : Gal(L/K)) (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : ∑ χ : Gal(L/K) →* ℂˣ, ↑(χ σ)⁻¹ * χ.galoisCharacterWeight P.asIdeal = if P ∈ NumberField.Chebotarev.frobeniusPrimeSet K L (ConjClasses.mk σ) then ↑(Nat.card Gal(L/K)) else 0

Character orthogonality at every prime. For L / K abelian, the sum of χ(σ)⁻¹ · galoisCharacterWeight χ 𝔭 over the characters χ of Gal(L/K) is #Gal(L/K) when 𝔭 lies in the Frobenius fibre of σ, and 0 otherwise, ramified primes included.

theorem AlgEquiv.natCard_mul_primeIdealZetaSum_frobeniusPrimeSet {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsMulCommutative Gal(L/K)] (σ : Gal(L/K)) {t : ℝ} (ht : 1 < t) : ↑(Nat.card Gal(L/K)) * ↑(NumberField.Set.primeIdealZetaSum (NumberField.Chebotarev.frobeniusPrimeSet K L (ConjClasses.mk σ)) t) = ∑ χ : Gal(L/K) →* ℂˣ, ↑(χ σ)⁻¹ * χ.galoisCharacterWeight.primeSum ↑t

The Frobenius fibre by orthogonality. For L / K abelian and t > 1, #Gal(L/K) times the prime zeta sum over the Frobenius fibre of σ is ∑_χ χ(σ)⁻¹ P_χ(t).