Frobenius ψ along a normal subextension

Let K ⊆ M ⊆ L be number fields with L / K and M / K Galois. Restriction to M is a group homomorphism Gal(L/K) → Gal(M/K), it carries the Artin class of a prime 𝔭 of 𝓞 K to the Artin class of 𝔭 for M / K with no power taken (NumberField.artinSymbol_map_restrictNormalHom), and it commutes with powers of conjugacy classes. So a prime power 𝔭 ^ j counted by frobeniusPsi K L D for a class D of Gal(L/K) is counted by frobeniusPsi K M C for the single class C = ConjClasses.map _ D, and the classes D lying over a fixed C contribute to it disjointly.

This file records that refinement. Pointwise, the Frobenius weights of the classes over C add up to the Frobenius weight of C itself, except at prime powers based at a prime ramifying in L, where the upper weights all vanish while the lower one need not. Summing over prime powers, any family of distinct classes over C gives a lower bound for frobeniusPsi K M C, and the full family misses only the finitely many primes of ramifiedPrimes K L, hence accounts for frobeniusPsi K M C up to O(log x).

The lower bound is the shape the cyclotomic crossing consumes: over the compositum M(μ_q) of M with an auxiliary cyclotomic field, the classes of the tagged elements (σ, τ) for distinct τ are distinct classes over the class of σ, so the weighted asymptotics of their fibres add up to a lower bound for the weighted asymptotics of the fibre of σ.

There is no companion upper bound for a proper subfamily, and none is needed: the crossing closes by summing the lower bounds over all of Gal(M/K) against ψ_M, which NumberField.Chebotarev.primePsi_univ_sub_sum_frobeniusPsi_isBigO_log supplies.

Main results

• NumberField.Chebotarev.sum_frobeniusPrimePowerWeight_map_restrictNormalHom: at a single prime power, the Frobenius weights of the classes of Gal(L/K) over C add up to the Frobenius weight of C, unless the base ramifies in L, in which case they add up to 0.
• NumberField.Chebotarev.sum_frobeniusPsi_le_frobeniusPsi: the Frobenius ψ functions of any finite family of distinct classes over C add up to at most frobeniusPsi K M C.
• NumberField.Chebotarev.frobeniusPsi_sub_sum_frobeniusPsi_le_primePsi: over the full family, the defect is at most ψ of the finite set ramifiedPrimes K L.
• NumberField.Chebotarev.frobeniusPsi_sub_sum_frobeniusPsi_isBigO_log: hence the defect is O(log x).

References

• J. Neukirch, Algebraic Number Theory, Chapter I, §9 and Chapter VII, §13.
• R. Sharifi, Algebraic Number Theory, the proof of Theorem 7.2.2, where the weighted count over an auxiliary compositum is bounded by the weighted count downstairs.

theorem NumberField.Chebotarev.sum_frobeniusPrimePowerWeight_map_restrictNormalHom {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [NumberField K] [Field L] [NumberField L] [Field M] [NumberField M] [Algebra K L] [Algebra K M] [Algebra M L] [IsScalarTower K M L] [IsGalois K L] [IsGalois K M] (C : ConjClasses Gal(M/K)) (A : TauCeti.IdealPrimePower K) : ∑ D : ConjClasses Gal(L/K) with ConjClasses.map (AlgEquiv.restrictNormalHom M) D = C, frobeniusPrimePowerWeight K L D A = {B : TauCeti.IdealPrimePower K | TauCeti.primePowerBase B ∉ ramifiedPrimes K L}.indicator (frobeniusPrimePowerWeight K M C) A

The Frobenius weights over a class add up to its own weight. For a tower K ⊆ M ⊆ L with both L / K and M / K Galois and a conjugacy class C of Gal(M/K), the powered Frobenius weights at a prime power 𝔭 ^ j of the classes of Gal(L/K) restricting to C add up to the powered Frobenius weight of C, provided 𝔭 is unramified in L; if 𝔭 ramifies in L they add up to 0, whatever the weight of C is.

At most one summand is ever nonzero, namely the one indexed by the j-th power of the Artin class of 𝔭 in L / K; restriction carries it to the j-th power of the Artin class of 𝔭 in M / K.

theorem NumberField.Chebotarev.sum_frobeniusPsi_le_frobeniusPsi {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [NumberField K] [Field L] [NumberField L] [Field M] [NumberField M] [Algebra K L] [Algebra K M] [Algebra M L] [IsScalarTower K M L] [IsGalois K L] [IsGalois K M] (C : ConjClasses Gal(M/K)) (S : Finset (ConjClasses Gal(L/K))) (hS : ∀ D ∈ S, ConjClasses.map (AlgEquiv.restrictNormalHom M) D = C) (x : ℝ) : ∑ D ∈ S, frobeniusPsi K L D x ≤ frobeniusPsi K M C x

Distinct classes over C give a lower bound for its Frobenius ψ. For a tower K ⊆ M ⊆ L with both L / K and M / K Galois, the Frobenius ψ functions of a finite family of distinct conjugacy classes of Gal(L/K), each restricting to C, add up to at most the Frobenius ψ function of C.

This is the form the cyclotomic crossing uses: the tagged classes over an auxiliary compositum are distinct and all restrict to the class being counted, so their weighted contributions add.

theorem NumberField.Chebotarev.frobeniusPsi_sub_sum_frobeniusPsi_le_primePsi {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [NumberField K] [Field L] [NumberField L] [Field M] [NumberField M] [Algebra K L] [Algebra K M] [Algebra M L] [IsScalarTower K M L] [IsGalois K L] [IsGalois K M] (C : ConjClasses Gal(M/K)) (x : ℝ) : frobeniusPsi K M C x - ∑ D : ConjClasses Gal(L/K) with ConjClasses.map (AlgEquiv.restrictNormalHom M) D = C, frobeniusPsi K L D x ≤ TauCeti.primePsi K (↑(ramifiedPrimes K L)) x

The classes over C account for its Frobenius ψ up to the ramified primes. The prime powers counted by frobeniusPsi K M C and by no class of Gal(L/K) over C can only be based at a prime of ramifiedPrimes K L, so the resulting defect is at most ψ of that finite set.

theorem NumberField.Chebotarev.frobeniusPsi_sub_sum_frobeniusPsi_isBigO_log {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [NumberField K] [Field L] [NumberField L] [Field M] [NumberField M] [Algebra K L] [Algebra K M] [Algebra M L] [IsScalarTower K M L] [IsGalois K L] [IsGalois K M] (C : ConjClasses Gal(M/K)) : (fun (x : ℝ) => frobeniusPsi K M C x - ∑ D : ConjClasses Gal(L/K) with ConjClasses.map (AlgEquiv.restrictNormalHom M) D = C, frobeniusPsi K L D x) =O[Filter.atTop] Real.log

The classes over C account for its Frobenius ψ up to O(log x). Only the prime powers based at the finitely many primes of ramifiedPrimes K L are missed.