Alphabeta MathHow 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 is an injective endomorphism in characteristic , and an automorphism for finite fields
Statement
Let be a field of characteristic . The Frobenius map
is an injective field endomorphism. If is finite, it is an automorphism. Its -fold iterate is .
Facts & Assumptions
Given: A field of positive characteristic .
The binomial theorem holds in every commutative ring (The binomial theorem over an arbitrary commutative ring).
For , the prime divides (A prime divides for ).
A positive field characteristic is prime (The characteristic of a field is zero or a prime number).
A field homomorphism preserves addition, multiplication, and (Field homomorphism and embedding).
An injection from a finite set to itself is a bijection (A subset of a finite set is finite, with , and equality holds if and only if ).
Proof
By [L1] and [L2], all intermediate terms in have coefficients divisible by and hence vanish in , so .
Commutativity gives , and , so Frobenius is an endomorphism by [L4].
If , then step 1.1 gives . A field has no nonzero nilpotents, so and the map is injective.
If is finite, [L5] turns this injection into a bijection, hence an automorphism.
Iterating and using gives , including as the identity.
Depends on
- The binomial theorem over an arbitrary commutative ring
- A prime $p$ divides $\binom pk$ for $0<k<p$
- The characteristic of a field is zero or a prime number
- Field homomorphism and embedding
- A subset of a finite set is finite, with $\lvert B\rvert \le \lvert A\rvert$, and equality holds if and only if $B = A$
Used by
- Fields of characteristic zero, finite fields, and algebraically closed fields are perfect Corollary
- Global functions on geometrically connected and geometrically reduced proper schemes Corollary
- A regular point that is not smooth: a purely inseparable thickening Counterexample
- Purely inseparable algebraic extensions Definition
- The relative Frobenius x↦ x^q of an extension of finite fields Definition
- ⋃_n≥0Fₚ(t^1/pⁿ) is an infinite perfect field of characteristic p Example
- Fₚ is the union of its finite subfields and is an infinite algebraic extension Example
- Frobenius on F₄ swaps the two non-prime-field elements Example
- A finite normal extension is separable over its purely inseparable fixed field Lemma
- Finite purely inseparable rational extensions admit a finite Frobenius envelope Lemma
- Finite-type field extensions with zero Ω Lemma
- If a is not a pth power in a characteristic-p field, then x^pⁿ-a is irreducible for every n≥1 Lemma
- If p is a prime not dividing n, a rational minimal polynomial of a primitive n-th root of unity also kills its p-th power Lemma
- In characteristic p, the roots of x^pⁿ-x form a subfield and are all simple Lemma
- Integral closure in a purely inseparable rational envelope is finite Lemma
- The elements with a pⁿth power in the base form a perfect subfield carrying the one-step root condition Lemma
- A field is perfect exactly when it has characteristic zero or its Frobenius map is surjective Theorem
- In characteristic p, every irreducible polynomial is uniquely g(x^pᵉ) with g irreducible and separable Theorem
- Pure inseparability is transitive in towers and stable under composita Theorem
Dependency tree · two levels
29 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
- K. Conrad, Finite Fields, Sections 1-2 (standard reference, not scraped)
- J. S. Milne, Fields and Galois Theory, Propositions 4.19-4.24 (standard reference, not scraped)