Roots modulo p of the polynomial of a subgroup count Frobenius fixed points

Proved

ChebotarevDensity.exists_poly_rootCount_eq_fixCount

by vebis · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

galois-theorynumber-theory

Let $f\in\mathbb Z[X]$ be monic with nonzero discriminant, let $K$ be its splitting field over $\mathbb Q$ , $G=\operatorname{Gal}(K/\mathbb Q)$ , and let $H\le G$ be a subgroup. Then there are a monic polynomial $g\in\mathbb Z[X]$ , irreducible over $\mathbb Q$ , and a finite set $N$ of primes such that for every prime $p\notin N$ and every Frobenius substitution $\sigma\in G$ of $p$ ,

\#\{x\in\mathbb F_p:\ g(x)=0\}=\#\{xH\in G/H:\ \sigma xH=xH\}.

Thus the number of roots modulo $p$ of a suitable polynomial attached to $H$ (the minimal polynomial of an algebraic integer generating the fixed field $K^H$ ) equals the number of fixed points of the Frobenius substitution on $G/H$ .

Formalization Note The left side is rootCount g p and the right side is fixCount H σ; "Frobenius substitution of $p$ " is IsFrobeniusAt f p σ.

Preamble

import Definitions.Def_ChebotarevDensity_Defs
import Definitions.Def_ChebotarevDensity_Aux

open Polynomial NumberField

Formal statement

namespace ChebotarevDensity

theorem exists_poly_rootCount_eq_fixCount (f : ℤ[X]) (hf : f.Monic) (hdisc : f.discr ≠ 0)
    (H : Subgroup (GalGroup f)) :
    ∃ (g : ℤ[X]) (N : Finset ℕ), g.Monic ∧ Irreducible (g.map (Int.castRingHom ℚ)) ∧
      ∀ p : ℕ, p.Prime → p ∉ N → ∀ σ : GalGroup f, IsFrobeniusAt f p σ →
        rootCount g p = fixCount H σ := by sorry

end ChebotarevDensity

Source

Stevenhagen–Lenstra, Chebotarëv and his density theorem, Math. Intelligencer 18 (1996), no. 2, pp. 32–34 (Theorem of Frobenius, decomposition types, cycle patterns) and Appendix, pp. 35–36

View graph