TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Frobenius cycle type and prime splitting

Statement

Let $F \in Z [T]$ be monic separable with splitting field L, and let p be a rational prime not dividing $Disc (F)$ . Then p is unramified in L and $\overset{ˉ}{F} \in F_{p} [T]$ is squarefree. The degrees of its monic irreducible factors, with each distinct factor counted once, are exactly the cycle lengths of arithmetic Frobenius on the roots of F.

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Good polynomial reduction kills inertia: Let $F \in Z [T]$ be monic separable with splitting field L. If a rational prime p does not divide $Disc (F)$ , the integral roots of F have distinct reductions at every $P ∣ p$ . The inertia group I(P/p) is trivial, so p is unramified in L.

[F2]

Frobenius elements above a prime are conjugate: In a finite Galois extension L/K let the nonzero prime p be unramified. If $σ P = P^{'}$ above p, then ${Frob}_{P^{'}} = σ {Frob}_{P} σ^{- 1} .$ Thus p determines one conjugacy class. If the Galois group is abelian, the element is independent of P.

[F3]

A finite extension of a finite field of order $q$ is Galois with cyclic Galois group generated by $x \mapsto x^{q}$ : Let $F_{q}$ be a finite field of order $q$ and let $E$ be a finite field having $F_{q}$ as a subfield, with $[E : F_{q}] = n$ (def-extension-degree-and-finite-extension). Then $E / F_{q}$ is a finite Galois extension (def-finite-galois-extension-and-galois-group) and $Gal (E / F_{q}) = ⟨ σ_{q} ⟩$ is cyclic of order $n$ , generated by the relative Frobenius $σ_{q} ⁣ : x \mapsto x^{q}$ (def-relative-frobenius-of-a-finite-field-extension).

[F4]

Unramified frobenius element exists uniquely: For an unramified prime $P ∣ p$ , the arithmetic Frobenius is the unique element of $D (P / p)$ satisfying ${Frob}_{P} (a) \equiv a^{N p} (m o d P)$ for every $a \in O_{L}$ .

Proof

1.1F1F4

Good reduction gives unramifiedness and distinct reductions of all roots in $κ (P)$ at any chosen $P ∣ p$ . Since the polynomial is monic, those $\deg F$ reductions are all its roots and are distinct; hence $\overset{ˉ}{F}$ is squarefree. The reduction map is therefore a bijection of root sets. For every integral root $a$ , [F4] gives ${Frob}_{P} (a) \equiv a^{p} (m o d P)$ , so this bijection intertwines ${Frob}_{P}$ with $x \mapsto x^{p}$ .

1.2F3

For a root a in the finite field $κ (P)$ let its p-power orbit have length d. The orbit polynomial $H (T) = \prod_{j = 0}^{d - 1} (T - a^{p^{j}})$ has coefficients fixed by Frobenius, hence in $F_{p}$ by the finite-field Galois theorem. Every polynomial in $F_{p} [T]$ vanishing at a vanishes at all these d distinct elements. Its degree is therefore at least d unless it is zero. The minimal polynomial divides H and has degree at least d, so equals H. Thus each orbit corresponds to one irreducible factor of degree d.

2.1F2step 1.1step 1.2∎

The bijection of root sets identifies these orbit lengths with the Frobenius cycles. Changing P conjugates Frobenius and so preserves cycle lengths. Empty root sets give empty factor and cycle lists; degree one gives a single fixed root.

Depends on

Used by

Frobenius cycle type needs good reduction Counterexample
Frobenius in a small cyclotomic field Example
Gaussian and eisenstein frobenius Example
Nonabelian frobenius conjugacy class Example

Dependency tree · two levels

18 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Chapter 8, Proposition 8.21, Corollary 8.22, Theorem 8.23, pp.144–145 (standard reference, not scraped)