The finite subfields of a separably closed field of positive characteristic

TauCeti.frobeniusFixedSubfield K p n is the subfield of solutions of a ^ p ^ n = a, defined for an arbitrary field of exponential characteristic p. When the field is separably closed and n ≠ 0 it is the field of q = p ^ n elements sitting inside it.

The counting is the standard one: a ^ q = a says exactly that a is a root of X ^ q - X, a polynomial whose derivative is -1 and which therefore has no repeated roots, so over a separably closed field it splits and has as many roots as its degree. In any field of characteristic p a subfield with q elements is the Frobenius-fixed one, since being fixed by the q-power map characterises the elements of a finite subfield of order q. In the other direction every element of an algebraic closure of ZMod p lies in one of these subfields, since it generates a finite extension of the prime field.

Main results

• TauCeti.finite_frobeniusFixedSubfield and TauCeti.finite_frobeniusFixedSubring: over any field of characteristic p and for n ≠ 0 it is finite, being a set of roots of X ^ p ^ n - X.
• TauCeti.card_frobeniusFixedSubfield: over a separably closed field and for n ≠ 0 it has exactly p ^ n elements.
• TauCeti.eq_frobeniusFixedSubfield_of_natCard: it is the unique subfield with that many elements.
• TauCeti.nonempty_frobeniusFixedSubfield_ringEquiv_galoisField: it is therefore a copy of GaloisField p n.
• TauCeti.exists_mem_frobeniusFixedSubfield: an algebraic closure of the prime field is the union of these subfields.

References

This is the field-theoretic half of "the fixed points of the q-power Frobenius are the 𝔽_q-points", the ring-theoretic half being TauCeti.frobeniusFixedSubring itself. It supplies the finite-field input for studying points over an algebraically closed field and for ordinary and graph-twisted Steinberg maps, which start from the q-power Frobenius of an algebraic closure of ZMod p.

• S. Lang, Algebra, 3rd ed., V.5.
• R. Lidl and H. Niederreiter, Finite Fields, §2.1.

The root set of X ^ q - X

theorem TauCeti.coe_frobeniusFixedSubfield_eq_rootSet (K : Type u_1) [Field K] (p n : ℕ) [Fact (Nat.Prime p)] [CharP K p] (hn : n ≠ 0) : ↑(frobeniusFixedSubfield K p n) = (Polynomial.X ^ p ^ n - Polynomial.X).rootSet K

Over any field of characteristic p and for n ≠ 0, being fixed by the p ^ n-power Frobenius is being a root of X ^ p ^ n - X. That polynomial is then separable of degree p ^ n, which is where the count below comes from. At n = 0 the two sides differ: the subfield is the whole of K while X ^ 1 - X = 0 has empty root set.

theorem TauCeti.finite_frobeniusFixedSubfield (K : Type u_1) [Field K] (p n : ℕ) [Fact (Nat.Prime p)] [CharP K p] (hn : n ≠ 0) : Finite ↥(frobeniusFixedSubfield K p n)

The Frobenius-fixed subfield of a field of characteristic p is finite once n ≠ 0, being a set of roots of a nonzero polynomial. This is not an instance: at n = 0 the subfield is the whole of K, which need not be finite.

theorem TauCeti.finite_frobeniusFixedSubring (K : Type u_1) [Field K] (p n : ℕ) [Fact (Nat.Prime p)] [CharP K p] (hn : n ≠ 0) : Finite ↥(frobeniusFixedSubring K p n)

The Frobenius-fixed subring of a field of characteristic p is finite once n ≠ 0. This is TauCeti.finite_frobeniusFixedSubfield read through TauCeti.toSubring_frobeniusFixedSubfield, the two having the same elements; it is the form a consumer working with TauCeti.frobeniusFixedSubring over a field asks for. Not an instance, for the reason given at TauCeti.finite_frobeniusFixedSubfield.

theorem TauCeti.eq_frobeniusFixedSubfield_of_natCard (K : Type u_1) [Field K] (p n : ℕ) [Fact (Nat.Prime p)] [CharP K p] {F : Subfield K} (hF : Nat.card ↥F = p ^ n) : F = frobeniusFixedSubfield K p n

Uniqueness of the subfield of q elements. A subfield with p ^ n elements of a field of characteristic p is the subfield fixed by the p ^ n-power Frobenius.

An element of the ambient field satisfies a ^ q = a exactly when it lies in a subfield with q elements, by TauCeti.FiniteField.pow_card_eq_self_iff_mem_range_algebraMap; no counting, and no algebraic closedness, is involved.

theorem TauCeti.card_frobeniusFixedSubfield (K : Type u_1) [Field K] [IsSepClosed K] (p n : ℕ) [Fact (Nat.Prime p)] [CharP K p] (hn : n ≠ 0) : Nat.card ↥(frobeniusFixedSubfield K p n) = p ^ n

The field of q elements inside a separably closed field. For q = p ^ n with n ≠ 0, the elements of a separably closed field of characteristic p fixed by the q-power Frobenius form a subfield with exactly q elements.

The count is the number of roots of the separable polynomial X ^ q - X, which is its degree.

theorem TauCeti.nonempty_frobeniusFixedSubfield_ringEquiv_galoisField (K : Type u_1) [Field K] [IsSepClosed K] (p n : ℕ) [Fact (Nat.Prime p)] [CharP K p] (hn : n ≠ 0) : Nonempty (↥(frobeniusFixedSubfield K p n) ≃+* GaloisField p n)

The Frobenius-fixed subfield of a separably closed field is a copy of Mathlib's GaloisField p n, the two being finite fields of the same cardinality. The isomorphism is not canonical, which is why only its existence is recorded.

Exhaustion over an algebraic prime field

theorem TauCeti.exists_mem_frobeniusFixedSubfield (K : Type u_1) [Field K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] [Algebra (ZMod p) K] [Algebra.IsAlgebraic (ZMod p) K] (x : K) : ∃ (n : ℕ), n ≠ 0 ∧ x ∈ frobeniusFixedSubfield K p n

An algebraic extension of ZMod p is the union of its Frobenius-fixed subfields. Every element generates a finite extension of the prime field, and so is fixed by the p ^ n-power Frobenius for the degree n of that extension.

Only algebraicity over the prime field is used, so the statement covers an algebraic closure of ZMod p without assuming algebraic closedness.