Cyclotomic Frobenius fibres and arithmetic progressions

Away from the cyclotomic level, the fibre of an automorphism is the set of primes whose norm reduces to its cyclotomic character. This identifies the arithmetic Frobenius convention with arithmetic progressions: the residue is the character itself, not its inverse.

For a cyclotomic extension of ℚ of nonzero level n with n % 4 ≠ 2, the identification holds at every prime: primes dividing the level ramify and their residues are not units. The restriction excludes levels twice an odd number, where 2 is unramified. In particular, the four Frobenius fibres of ℚ(ζ₅) are precisely the four invertible residue classes modulo five. At every nonzero level the symmetric difference is finite, which suffices to transfer density from Frobenius fibres to arithmetic progressions.

References

• L. Washington, Introduction to Cyclotomic Fields, Chapter 2.
• The Frobenius computation is the existing mem_frobeniusPrimeSet_mk_iff_restrictNormal_autToPow, specialized to a trivial lower extension.

theorem NumberField.Chebotarev.mem_frobeniusPrimeSet_mk_iff_autToPow_eq_absNorm {K : Type u_1} [Field K] [NumberField K] {m : ℕ} [NeZero m] {F : Type u_2} [Field F] [NumberField F] [Algebra K F] [IsGalois K F] [IsCyclotomicExtension {m} K F] {ζ : F} (hζ : IsPrimitiveRoot ζ m) (σ : Gal(F/K)) {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)} (hm : ↑m ∉ 𝔭.asIdeal) : 𝔭 ∈ frobeniusPrimeSet K F (ConjClasses.mk σ) ↔ ↑((IsPrimitiveRoot.autToPow K hζ) σ) = ↑(Ideal.absNorm 𝔭.asIdeal)

Away from the level, the cyclotomic Frobenius fibre is characterized by the norm modulo that level. Unramifiedness follows from the condition on the level.

theorem NumberField.Chebotarev.mem_frobeniusPrimeSet_galEquivZMod_symm_iff (F : Type u_1) [Field F] [NumberField F] (n : ℕ) [NeZero n] [IsCyclotomicExtension {n} ℚ F] [IsGalois ℚ F] {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers ℚ)} (hm : ↑n ∉ 𝔭.asIdeal) (a : (ZMod n)ˣ) : 𝔭 ∈ frobeniusPrimeSet ℚ F (ConjClasses.mk ((IsCyclotomicExtension.Rat.galEquivZMod n F).symm a)) ↔ ↑(Ideal.absNorm 𝔭.asIdeal) = ↑a

Away from the level, a prime of 𝓞 ℚ lies in the cyclotomic Frobenius fibre tagged by a unit a modulo n exactly when its norm is congruent to a modulo n.

@[simp]

theorem NumberField.Chebotarev.frobeniusPrimeSet_galEquivZMod_symm_eq_setOf_natCast_absNorm_eq (F : Type u_1) [Field F] [NumberField F] (n : ℕ) [NeZero n] [IsCyclotomicExtension {n} ℚ F] [IsGalois ℚ F] (hn : n % 4 ≠ 2) (a : (ZMod n)ˣ) : frobeniusPrimeSet ℚ F (ConjClasses.mk ((IsCyclotomicExtension.Rat.galEquivZMod n F).symm a)) = {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers ℚ) | ↑(Ideal.absNorm 𝔭.asIdeal) = ↑a}

At a nonzero level not congruent to two modulo four, a cyclotomic Frobenius fibre over ℚ is exactly an invertible arithmetic progression. Primes dividing the level belong to neither side.

theorem NumberField.Chebotarev.finite_symmDiff_frobeniusPrimeSet_galEquivZMod_symm (F : Type u_1) [Field F] [NumberField F] (n : ℕ) [NeZero n] [IsCyclotomicExtension {n} ℚ F] [IsGalois ℚ F] (a : (ZMod n)ˣ) : (symmDiff (frobeniusPrimeSet ℚ F (ConjClasses.mk ((IsCyclotomicExtension.Rat.galEquivZMod n F).symm a))) {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers ℚ) | ↑(Ideal.absNorm 𝔭.asIdeal) = ↑a}).Finite

At every nonzero level, the cyclotomic Frobenius fibre differs from its arithmetic progression at only finitely many primes. This includes levels congruent to two modulo four, where the prime above two can lie in the Frobenius fibre without lying in the progression.