How many primes carry a given Frobenius element

Let L / K be a finite Galois extension of number fields, 𝔭 an ideal of 𝓞 K and σ an element of Gal(L/K). The primes of 𝓞 L above 𝔭 at which σ is an arithmetic Frobenius form the fiber of σ, and Ideal.frobenius_fiber_card_eq_of_isConj shows that conjugate elements have fibers of the same size. This file computes that size, at a prime where σ is a Frobenius and L / K is unramified:

#(fiber of σ) * orderOf σ = #Centralizer_{Gal(L/K)}(σ)

The reason is that the fiber is a single orbit. Gal(L/K) acts transitively on the primes above 𝔭, and the Frobenius at τ • Q is τ σ τ⁻¹, so the elements carrying Q to another member of the fiber are exactly those commuting with σ. The stabilizer of Q inside that centralizer is the decomposition group ⟨σ⟩, whose order is orderOf σ, and the orbit-stabilizer theorem gives the count.

The identity is stated as a product rather than as #Centralizer(σ) / orderOf σ so that it says something without a separate divisibility: orderOf σ divides the centralizer's order because ⟨σ⟩ is a subgroup of it, and ConjClasses.card_carrier_mul_orderOf_dvd records the companion divisibility for a whole conjugacy class.

Main results

• Ideal.frobenius_fiber_eq_orbit_centralizer: the fiber of σ above 𝔭 is the orbit of any of its members under the centralizer of σ.
• Ideal.frobenius_fiber_card_mul_orderOf_eq_card_centralizer: its size, times orderOf σ, is the order of that centralizer.
• HeightOneSpectrum.frobeniusFiberEquiv: the height-one-prime and ideal representations of the fiber are equivalent.

References

• Sharifi, Algebraic Number Theory, Theorem 7.2.2 (p. 143).
• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter I, §9.

theorem Ideal.frobenius_fiber_eq_orbit_centralizer {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (𝔭 : Ideal (NumberField.RingOfIntegers K)) {σ : Gal(L/K)} (Q : Ideal (NumberField.RingOfIntegers L)) [IsGalois K L] [Q.IsPrime] [Q.LiesOver 𝔭] [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q] (hσ : IsArithFrobAt (NumberField.RingOfIntegers K) σ Q) : {P : Ideal (NumberField.RingOfIntegers L) | ∃ (_ : P.IsPrime) (_ : P.LiesOver 𝔭) (_ : P ≠ ⊥), IsArithFrobAt (NumberField.RingOfIntegers K) σ P} = MulAction.orbit (↥(Subgroup.centralizer {σ})) Q

The Frobenius fiber is an orbit of the centralizer. Let Q be a prime of 𝓞 L above an ideal 𝔭 of 𝓞 K, unramified over 𝓞 K, with σ an arithmetic Frobenius at Q. Then the primes above 𝔭 admitting σ as a Frobenius are exactly the translates of Q by elements commuting with σ.

Both inclusions come from Ideal.isArithFrobAt_pointwise_smul_iff_eq_conj, which says the Frobenius elements at τ • Q are the conjugates τ σ τ⁻¹: an element of Gal(L/K) carries Q into the fiber exactly when conjugation by it fixes σ. Transitivity of the action on the primes above 𝔭 is what makes every member of the fiber such a translate.

theorem Ideal.frobenius_fiber_card_mul_orderOf_eq_card_centralizer {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (𝔭 : Ideal (NumberField.RingOfIntegers K)) {σ : Gal(L/K)} (Q : Ideal (NumberField.RingOfIntegers L)) [IsGalois K L] [Q.IsPrime] [Q.LiesOver 𝔭] [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q] (hσ : IsArithFrobAt (NumberField.RingOfIntegers K) σ Q) : Nat.card { P : Ideal (NumberField.RingOfIntegers L) // ∃ (_ : P.IsPrime) (_ : P.LiesOver 𝔭) (_ : P ≠ ⊥), IsArithFrobAt (NumberField.RingOfIntegers K) σ P } * orderOf σ = Nat.card ↥(Subgroup.centralizer {σ})

The size of a Frobenius fiber. At an unramified prime Q above an ideal 𝔭 with arithmetic Frobenius σ, the number of primes above 𝔭 admitting σ as a Frobenius, times the order of σ, is the order of the centralizer of σ in Gal(L/K).

This is the orbit-stabilizer theorem applied to frobenius_fiber_eq_orbit_centralizer: the stabilizer of Q in the centralizer is the decomposition group ⟨σ⟩, of order orderOf σ.

Compare Ideal.frobenius_fiber_card_eq_of_isConj, which says fibers of conjugate elements have equal size without saying what that size is.

noncomputable def IsDedekindDomain.HeightOneSpectrum.frobeniusFiberEquiv {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : HeightOneSpectrum (NumberField.RingOfIntegers K)) (sigma : Gal(L/K)) : { Q : HeightOneSpectrum (NumberField.RingOfIntegers L) // under (NumberField.RingOfIntegers K) Q = p ∧ IsArithFrobAt (NumberField.RingOfIntegers K) sigma Q.asIdeal } ≃ { Q : Ideal (NumberField.RingOfIntegers L) // ∃ (_ : Q.IsPrime) (_ : Q.LiesOver p.asIdeal) (_ : Q ≠ ⊥), IsArithFrobAt (NumberField.RingOfIntegers K) sigma Q }

The equivalence between the height-one-prime and ideal representations of a Frobenius fiber above p, induced by HeightOneSpectrum.asIdeal.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.frobeniusFiberEquiv_apply {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : HeightOneSpectrum (NumberField.RingOfIntegers K)) (sigma : Gal(L/K)) (Q : { Q : HeightOneSpectrum (NumberField.RingOfIntegers L) // under (NumberField.RingOfIntegers K) Q = p ∧ IsArithFrobAt (NumberField.RingOfIntegers K) sigma Q.asIdeal }) : ↑((p.frobeniusFiberEquiv sigma) Q) = (↑Q).asIdeal

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.frobeniusFiberEquiv_symm_apply_asIdeal {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : HeightOneSpectrum (NumberField.RingOfIntegers K)) (sigma : Gal(L/K)) (Q : { Q : Ideal (NumberField.RingOfIntegers L) // ∃ (_ : Q.IsPrime) (_ : Q.LiesOver p.asIdeal) (_ : Q ≠ ⊥), IsArithFrobAt (NumberField.RingOfIntegers K) sigma Q }) : (↑((p.frobeniusFiberEquiv sigma).symm Q)).asIdeal = ↑Q

theorem IsDedekindDomain.HeightOneSpectrum.frobenius_fiber_card_eq_card_centralizer_div_orderOf {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : HeightOneSpectrum (NumberField.RingOfIntegers K)) {σ : Gal(L/K)} (Q : Ideal (NumberField.RingOfIntegers L)) [IsGalois K L] [Q.IsPrime] [Q.LiesOver p.asIdeal] [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q] (hσ : IsArithFrobAt (NumberField.RingOfIntegers K) σ Q) : Nat.card { R : HeightOneSpectrum (NumberField.RingOfIntegers L) // under (NumberField.RingOfIntegers K) R = p ∧ IsArithFrobAt (NumberField.RingOfIntegers K) σ R.asIdeal } = Nat.card ↥(Subgroup.centralizer {σ}) / orderOf σ

The absolute Frobenius fibre, counted. The primes of L over p at which σ is an arithmetic Frobenius form a single orbit of the centralizer of σ, whose stabilizer is ⟨σ⟩, so there are #Centralizer(σ) / orderOf σ of them.

This is Ideal.frobenius_fiber_card_mul_orderOf_eq_card_centralizer solved for the fibre and re-indexed: that theorem states the product and is indexed by ideals lying over p.asIdeal, while counting arguments over a number field index by HeightOneSpectrum primes contracting to p. HeightOneSpectrum.frobeniusFiberEquiv bridges the two indexings, and the division is exact because orderOf σ is the size of a stabilizer inside the acting group.