Galois theory of finite fields: Frobenius cycle pattern = decomposition type

Proved

ChebotarevDensity.frobeniusCyclePattern_eq_factorDegrees

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

algebraic-number-theorynumber-theory

Let $p$ be a prime and let $g\in\mathbb F_p[X]$ be squarefree. Let $L$ be a splitting field of $g$ over $\mathbb F_p$ , and let $\mathrm{Frob}:L\to L$ , $x\mapsto x^p$ , be the Frobenius automorphism, which permutes the zeros of $g$ in $L$ . Then the cycle pattern of $\mathrm{Frob}$ on these zeros (cycles of length $1$ included) is the decomposition type of $g$ :

\text{cycle lengths of Frob on }\{g=0\}\;=\;\{\deg h : h \text{ a monic irreducible factor of } g\}\quad\text{(as multisets).}

Applied to $g=f\bmod p$ , this is what links Frobenius substitutions to factorizations of $f$ modulo $p$ .

Formalization Note Degrees of the normalized (monic) irreducible factors are taken with multiplicity; for squarefree $g$ all multiplicities are $1$ .

Preamble

import Definitions.Def_ChebotarevDensity_Defs

open Polynomial NumberField

Formal statement

namespace ChebotarevDensity

theorem frobeniusCyclePattern_eq_factorDegrees (p : ℕ) [Fact p.Prime] (g : (ZMod p)[X])
    (hg : Squarefree g) :
    frobeniusCyclePattern p g =
      (UniqueFactorizationMonoid.normalizedFactors g).map natDegree := 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: "Galois theory for finite fields comes down to the statement that the cycle pattern of Frob, viewed as a permutation of the zeros of g, is the same as the decomposition type of g over F_p. This is true for any polynomial g with coefficients in F_p that has no repeated factors."

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 prime $p$ (supplied as a typeclass fact) and every polynomial $g\in\mathbb F_p[X]$ that is squarefree (no square of a non-unit divides $g$ ; in particular $g\neq0$ ): let $L$ be Mathlib's splitting field of $g$ over $\mathbb F_p$ and $\phi$ the automorphism $x\mapsto x^{p}$ of $L$ over $\mathbb F_p$ . Then the multiset of cycle lengths, fixed points included, of the permutation of the set of distinct roots of $g$ in $L$ induced by $\phi$ equals the multiset

\{\deg h : h\in\mathrm{normalizedFactors}(g)\},

the degrees of the monic irreducible factors of $g$ counted with multiplicity. For $g$ a nonzero constant both sides are empty.

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