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.1

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}$ .

F1F4

1.2

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.1

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.

F2step 1.1step 1.2∎

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)