Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Frobenii of coprime-norm primes generate the Galois group

Abstract

Frobenii of coprime-norm primes generate the Galois group.

Theorem 1.1 (Frobenii of coprime-norm primes generate the Galois group).

Lean statement: D5/S3/Factorization/Galois/Chebotarev/CyclotomicNormResidue.subgroup_eq_top_of_forall_frobenius_mem_of_coprime

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

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

Commentary.

Frobenii of coprime-norm primes generate the Galois group (abelian case). A subgroup of Gal(L/K) containing the Frobenius representative of every nonzero prime of K that is unramified in L and has norm coprime to m is all of Gal(L/K). The κ-uniformity realization in ZetaProduct.lean uses this theorem for residues arising from coprime- norm ideal Frobenius values.

References