The Frobenius over a finite base field

Let K be a finite field with q elements. Over any K-algebra A the q-power map is the algebra endomorphism FiniteField.frobeniusAlgHom K A; its iterates raise every element to a q ^ n-th power, and the elements they fix form a K-subalgebra. Both statements hold for every K-algebra, with no characteristic hypothesis on A: TauCeti.frobeniusFixedSubring is the same subset when A has exponential characteristic p and q is a power of p, but that hypothesis fails for the zero ring, which a subgroup scheme still has to be evaluated at.

For a field extension L of K the range of the q-power map is a subfield over which L is purely inseparable: every x : L has x ^ q in that image, and q is a power of the exponential characteristic.

On a finite field of order p ^ 2 the Frobenius automorphism frobeniusEquiv K p, sending x to x ^ p, is an involution. This is the field automorphism behind Hermitian duality of codes over the field of four elements.

Main definitions

• TauCeti.FiniteField.frobeniusFixedSubalgebra: the subalgebra fixed by an iterate of the Frobenius.

Main results

• TauCeti.FiniteField.frobeniusAlgHom_pow_apply: the n-th iterate is the q ^ n-power map.
• TauCeti.FiniteField.sub_pow_natCard: the q-power map is additive, (x - y) ^ q = x ^ q - y ^ q.
• TauCeti.FiniteField.mem_frobeniusFixedSubalgebra: membership in the fixed subalgebra is the equation a ^ q ^ n = a.
• TauCeti.FiniteField.isPurelyInseparable_fieldRange_frobeniusAlgHom: L is purely inseparable over the field range of FiniteField.frobeniusAlgHom K L.
• TauCeti.FiniteField.frobeniusEquiv_involutive: on a field of order p ^ 2, the Frobenius automorphism x ↦ x ^ p is an involution.

Mathematical context

This is the field-theoretic input to proving that the Frobenius isogeny π_q is purely inseparable of degree q. Stating it before specializing to a curve keeps the argument independent of the particular function field, just as the degree computation first identifies the field range of the same q-power map.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.2.

theorem TauCeti.FiniteField.sub_pow_natCard (K : Type u_1) (A : Type u_2) [Field K] [Finite K] [CommRing A] [Algebra K A] (x y : A) : (x - y) ^ Nat.card K = x ^ Nat.card K - y ^ Nat.card K

Raising to the order of a finite base field is additive: in a K-algebra, (x - y) ^ q = x ^ q - y ^ q for q the number of elements of K.

theorem TauCeti.FiniteField.frobeniusAlgHom_pow_apply (K : Type u_1) (A : Type u_2) [Field K] [Fintype K] [CommRing A] [Algebra K A] (n : ℕ) (x : A) : (FiniteField.frobeniusAlgHom K A ^ n) x = x ^ Nat.card K ^ n

The n-th iterate of the Frobenius over a finite base field raises every element to the (Nat.card K) ^ n-th power.

def TauCeti.FiniteField.frobeniusFixedSubalgebra (K : Type u_1) (A : Type u_2) [Field K] [Fintype K] [CommRing A] [Algebra K A] (n : ℕ) : Subalgebra K A

The subalgebra fixed by an iterate of the Frobenius over a finite base field, the equalizer of that iterate with the identity, that is, the solutions of a ^ (Nat.card K) ^ n = a.

For K = 𝔽_q, A an algebraic closure of K and 0 < n this is the subfield of q ^ n elements, but nothing of the sort is asserted here. Unlike TauCeti.frobeniusFixedSubring, which reads the same subset off iterateFrobenius, this needs no exponential characteristic on A.

Equations

• TauCeti.FiniteField.frobeniusFixedSubalgebra K A n = (FiniteField.frobeniusAlgHom K A ^ n).equalizer (AlgHom.id K A)

theorem TauCeti.FiniteField.frobeniusFixedSubalgebra_def (K : Type u_1) (A : Type u_2) [Field K] [Fintype K] [CommRing A] [Algebra K A] (n : ℕ) : frobeniusFixedSubalgebra K A n = (FiniteField.frobeniusAlgHom K A ^ n).equalizer (AlgHom.id K A)

The Frobenius-fixed subalgebra is the equalizer of the n-th Frobenius iterate with the identity.

@[simp]

theorem TauCeti.FiniteField.mem_frobeniusFixedSubalgebra {K : Type u_1} {A : Type u_2} [Field K] [Fintype K] [CommRing A] [Algebra K A] {n : ℕ} {a : A} : a ∈ frobeniusFixedSubalgebra K A n ↔ a ^ Nat.card K ^ n = a

Membership in the Frobenius-fixed subalgebra is the equation a ^ (Nat.card K) ^ n = a.

theorem TauCeti.FiniteField.isPurelyInseparable_fieldRange_frobeniusAlgHom {K : Type u_3} {L : Type u_4} [Field K] [Fintype K] [Field L] [Algebra K L] : IsPurelyInseparable (↥(FiniteField.frobeniusAlgHom K L).fieldRange) L

A field is purely inseparable over the image of its finite-base-field Frobenius (the field-theoretic statement in Silverman II.2.11(b)). Every element has its q-th power in the image, where q = Nat.card K is a power of the exponential characteristic.

The Frobenius of a field of order p ^ 2

theorem TauCeti.FiniteField.frobeniusEquiv_involutive {K : Type u_5} [Field K] [Finite K] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] (hK : Nat.card K = p ^ 2) : Function.Involutive ⇑(frobeniusEquiv K p)

On a field of order p ^ 2, the Frobenius automorphism x ↦ x ^ p is an involution.