Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Disjoint cyclotomic-crossing Frobenius fibres

Abstract

Disjoint cyclotomic-crossing Frobenius fibres.

Theorem 1.1 (Disjoint cyclotomic-crossing Frobenius fibres).

Lean statement: D5/S3/Factorization/Galois/Chebotarev/CyclotomicCrossingFibres.exists_cyclotomicCrossing_fibres

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/Chebotarev/CyclotomicCrossingFibres.exists_cyclotomicCrossing_fibres (✓ std3). ∎

Citation. Chris Birkbeck and the Chebotarev density contributors (2026). Chebotarev density in Lean. URL: https://github.com/CBirkbeck/chebotarev-density/tree/a00054a0e6bbc394b0e81de750db0cd2efc8bd88.

Commentary.

For an abelian Galois extension L/K, σ in Gal(L/K), m ≥ 1 with m % 4 ≠ 2 and (disc L).natAbs coprime to m, there is a family S indexed by H_n = {τ in (ℤ/mℤ)ˣ : |Gal(L/K)| divides ord τ}. These sets are pairwise disjoint. Each lies in the unramified σ-Frobenius fibre of prime ideals of K and has Dirichlet density 1/(|Gal(L/K)|·|(ℤ/mℤ)ˣ|).

References