Frobenius substitutions of an unramified prime form one conjugacy class

Proved

ChebotarevDensity.frobenius_substitutions_form_conjClass

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-number-theorynumber-theory

Let $f\in\mathbb Z[X]$ be monic with discriminant $\Delta(f)\neq0$ , let $K$ be its splitting field and $G=\mathrm{Gal}(K/\mathbb Q)$ . Let $p$ be a prime with $p\nmid\Delta(f)$ . Then the set of Frobenius substitutions of $p$ ,

\{\sigma\in G:\ \exists\,\mathfrak Q\subset\mathcal O_K \text{ prime}, p\in\mathfrak Q,\ \sigma(x)\equiv x^p \ (\mathrm{mod}\ \mathfrak Q)\ \forall x\in\mathcal O_K\},

is exactly one conjugacy class of $G$ .

This is what makes the Frobenius substitution $\sigma_p$ well defined up to conjugacy. It packages the basic facts (a)–(c) about places over $p$ stated in the source: places over $p$ exist, any two differ by an element of $G$ , and this element is unique when $p\nmid\Delta(f)$ .

Formalization Note The source phrases the facts in terms of places $K\to\overline{\mathbb F}_p\cup\{\infty\}$ ; the formal statement uses the equivalent language of prime ideals of $\mathcal O_K$ above $p$ .

Preamble

import Definitions.Def_ChebotarevDensity_Defs

open Polynomial NumberField

Formal statement

namespace ChebotarevDensity

theorem frobenius_substitutions_form_conjClass (f : ℤ[X]) (hf : f.Monic) (hdisc : f.discr ≠ 0)
    (p : ℕ) (hp : p.Prime) (hpd : ¬ (p : ℤ) ∣ f.discr) :
    ∃ C : ConjClasses (GalGroup f), {σ : GalGroup f | IsFrobeniusAt f p σ} = C.carrier := by sorry

end ChebotarevDensity

Source

P. Stevenhagen and H. W. Lenstra, Jr., "Chebotarëv and his density theorem", The Mathematical Intelligencer 18 (1996), no. 2, 26–37, https://doi.org/10.1007/BF03027290, p. 33: basic facts (a)–(c) about places, and "if φ varies over the places over a fixed prime p, then Frob_φ ranges over a conjugacy class in G"

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - non-blind, same agent that drafted the statements

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statements (Aristotle, by Harmonic), at the proposal owner's explicit request. It is not independent testimony: the author knew the intended meaning when writing it. Reviewers should compare it against the Lean code themselves rather than rely on it as a blind audit.

For every $f\in\mathbb Z[X]$ that is monic and has discriminant $\Delta(f)\neq0$ , and every prime $p\in\mathbb N$ with $p\nmid\Delta(f)$ (divisibility in $\mathbb Z$ ): there exists a conjugacy class $C$ of $G_f=\mathrm{Aut}_{\mathbb Q}(K_f)$ ( $K_f$ the splitting field of $f$ over $\mathbb Q$ ) such that

\{\sigma\in G_f:\ \mathrm{IsFrobeniusAt}(f,p,\sigma)\}=C,

where $\mathrm{IsFrobeniusAt}(f,p,\sigma)$ means: there is a prime ideal $\mathfrak Q$ of $\mathcal O_{K_f}$ containing $p$ with $\sigma(x)-x^{p}\in\mathfrak Q$ for all $x\in\mathcal O_{K_f}$ . In particular the statement asserts both that this set is nonempty and that it is closed under conjugation and contains no two non-conjugate elements.

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph