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 elements above a prime are conjugate

Statement

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.

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Unramified frobenius element exists uniquely: For finite Galois L/K and a nonzero prime $P ∣ p$ with $e (P / p) = 1$ , there is a unique ${Frob}_{P} \in D (P / p)$ satisfying ${Frob}_{P} (a) \equiv a^{N p} (m o d P) (a \in O_{L}) .$ It is the arithmetic Frobenius element, the unique lift of the arithmetic Frobenius coset.

[F2]

Conjugacy of decomposition and inertia groups: In finite Galois L/K, if $σ P = P^{'}$ above a nonzero p, then $D (P^{'} / p) = σ D (P / p) σ^{- 1}, I (P^{'} / p) = σ I (P / p) σ^{- 1} .$ The residue actions correspond under $κ (P) \to κ (P^{'})$ , $\overset{ˉ}{a} \mapsto \overline{σ a}$ .

[F3]

Galois action on primes above a prime is transitive: Let L/K be a finite Galois extension of number fields and p a nonzero prime of $O_{K}$ . Then $G = Gal (L / K)$ acts transitively on the primes P above p.

Proof

1.1F2

Conjugation by sigma transports D(P/p) to D(P'/p) and its residue action through the isomorphism induced by sigma. A field isomorphism commutes with taking the q-th power, where $q = N p$ . Hence the conjugate of ${Frob}_{P}$ acts as that power map at P'.

2.1F1F3step 1.1∎

Unramified Frobenius is uniquely characterized by this action, proving the formula. Transitivity says every prime P' above p is obtained in this way; conversely every sigma gives such a prime. The set of elements is therefore exactly a conjugacy class. In an abelian group conjugation fixes each element.

Depends on

Used by

Nonabelian frobenius conjugacy class Example
Frobenius cycle type and prime splitting Theorem

Dependency tree · two levels

9 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.14; Stein Proposition 9.4.1 (standard reference, not scraped)