The fixed points of the q-power map over a finite field

For a finite field K with q elements and any commutative domain L that is a K-algebra, an element of L is fixed by the q-power map exactly when it comes from K:

a ^ q = a ↔ a ∈ Set.range (algebraMap K L).

So an element outside K is moved by the map. In a quadratic extension the map is moreover an involution, since L then has q² elements, and it therefore exchanges the two roots of the minimal polynomial of such an element; in particular it keeps it outside K. Those statements are what the elliptic conjugacy classes of GL₂(𝔽_q) are read off from.

Main results

• TauCeti.FiniteField.pow_card_eq_self_iff_mem_range_algebraMap: the criterion above, with TauCeti.FiniteField.pow_natCard_eq_self_iff_mem_range_algebraMap its Nat.card spelling.
• TauCeti.algebraMap_bijective_of_pow_card_eq_self: its immediate global consequence, that a domain over K all of whose elements are fixed by the q-power map is K itself.
• TauCeti.FiniteField.pow_natCard_pow_natCard: in a quadratic extension the q-power map is an involution, with TauCeti.FiniteField.pow_natCard_ne and TauCeti.FiniteField.pow_natCard_notMem_range_algebraMap its two consequences for an element outside K.
• TauCeti.FiniteField.units_map_algebraMap_pow_natCard and TauCeti.FiniteField.units_pow_natCard_pow_natCard: the fixed-point and involution statements as equalities of units, the form in which a character of Lˣ consumes them, with TauCeti.FiniteField.units_powMonoidHom_comp_powMonoidHom the involution as an equality of monoid homomorphisms.

Mathlib has the easy direction (FiniteField.pow_card) but not the equivalence. IsGalois.mem_range_algebraMap_iff_fixed characterises the base field of a Galois extension by being fixed, but it needs [FiniteDimensional F E] and quantifies over the whole Galois group rather than the single q-power map.

L need not be a field: a commutative domain is enough, which covers polynomial rings over K, and the coordinate ring of an integral affine curve such as a Weierstrass curve, as well as field extensions. Nor need L be algebraically closed, which is the only case the source states.

This is the elementary field-theoretic input to the Silverman V.1 route to the Hasse bound: it says that the K-rational coordinates are exactly the Frobenius-fixed ones.

Provenance

Ported from the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0, dev/hasse-weil @ 513e83879e2f), HasseWeil/Curves/FrobeniusFixedLocus.lean, declaration frobenius_fixed_iff_mem_baseField.

Changes from the source. It is stated there only for L = AlgebraicClosure K; here L is an arbitrary commutative domain over K, since nothing in the argument uses algebraic closedness or inverses. The source builds the root-set transport by hand, through a separability argument and a finset count; here that is Mathlib's Splits.image_rootSet applied to FiniteField.isSplittingField_sub. And the source's other public theorem is stated in terms of its own private finsets, so it cannot be applied from outside; it is not reproduced. Nine declarations become one.

@[simp]

theorem TauCeti.FiniteField.pow_card_eq_self_iff_mem_range_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [Fintype K] [CommRing L] [IsDomain L] [Algebra K L] (a : L) : a ^ Fintype.card K = a ↔ a ∈ Set.range ⇑(algebraMap K L)

An element of a domain over a finite field is fixed by the q-power map exactly when it comes from the base field, where q is the cardinality of the base.

theorem TauCeti.FiniteField.pow_natCard_eq_self_iff_mem_range_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [Finite K] [CommRing L] [IsDomain L] [Algebra K L] (a : L) : a ^ Nat.card K = a ↔ a ∈ Set.range ⇑(algebraMap K L)

The Nat.card spelling of TauCeti.FiniteField.pow_card_eq_self_iff_mem_range_algebraMap, for a base field given as Finite rather than as a Fintype.

This is deliberately not a simp lemma: after synthesizing a Fintype K instance, simp rewrites Nat.card K to Fintype.card K and applies the preceding criterion, making this rule redundant.

theorem TauCeti.FiniteField.pow_natCard_ne {K : Type u_1} {L : Type u_2} [Field K] [Finite K] [CommRing L] [IsDomain L] [Algebra K L] {a : L} (ha : a ∉ Set.range ⇑(algebraMap K L)) : a ^ Nat.card K ≠ a

An element outside the base field is not fixed by the q-power map.

theorem TauCeti.FiniteField.units_map_algebraMap_pow_natCard {K : Type u_1} {L : Type u_2} [Field K] [Finite K] [CommRing L] [IsDomain L] [Algebra K L] (a : Kˣ) : (Units.map ↑(algebraMap K L)) a ^ Nat.card K = (Units.map ↑(algebraMap K L)) a

A unit of the base field is fixed by the q-power map, as an equality in Lˣ.

Quadratic extensions

theorem TauCeti.FiniteField.pow_natCard_pow_natCard {K : Type u_1} {L : Type u_2} [Field K] [Finite K] [DivisionRing L] [Algebra K L] [Algebra.IsQuadraticExtension K L] (a : L) : (a ^ Nat.card K) ^ Nat.card K = a

In a quadratic extension of a field with q elements the q-power map is an involution: L has q² elements, so a ^ (q²) = a.

This is deliberately not a simp lemma: in a context with a Fintype K instance, Nat.card K is not in simp normal form.

theorem TauCeti.FiniteField.units_pow_natCard_pow_natCard {K : Type u_1} {L : Type u_2} [Field K] [Finite K] [DivisionRing L] [Algebra K L] [Algebra.IsQuadraticExtension K L] (a : Lˣ) : (a ^ Nat.card K) ^ Nat.card K = a

In a quadratic extension the q-power map is an involution on units, the units-level form of TauCeti.FiniteField.pow_natCard_pow_natCard.

theorem TauCeti.FiniteField.units_powMonoidHom_comp_powMonoidHom {K : Type u_1} {L : Type u_2} [Field K] [Finite K] [Field L] [Algebra K L] [Algebra.IsQuadraticExtension K L] : (powMonoidHom (Nat.card K)).comp (powMonoidHom (Nat.card K)) = MonoidHom.id Lˣ

In a quadratic extension the q-power map on units is an involution, as an equality of monoid homomorphisms Lˣ →* Lˣ. This is TauCeti.FiniteField.units_pow_natCard_pow_natCard read at the level of the maps themselves, the form in which it cancels against a character Lˣ →* M precomposed with the q-power map.

As for its pointwise forms, this is deliberately not a simp lemma: in a context with a Fintype K instance, Nat.card K is not in simp normal form, so the exponent on the left-hand side here never survives simp normalization.

theorem TauCeti.FiniteField.pow_natCard_notMem_range_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [Finite K] [Field L] [Algebra K L] [Algebra.IsQuadraticExtension K L] {a : L} (ha : a ∉ Set.range ⇑(algebraMap K L)) : a ^ Nat.card K ∉ Set.range ⇑(algebraMap K L)

In a quadratic extension the q-th power of an element outside the base field is again outside it: the q-power map is an involution there, so a fixed value would force a itself to be fixed.

@[simp]

theorem AlgHom.frobeniusAlgHom_comm {K : Type u_1} {L : Type u_2} {Ω : Type u_3} [Field K] [Fintype K] [CommRing L] [Algebra K L] [CommRing Ω] [Algebra K Ω] (σ : L →ₐ[K] Ω) : σ.comp (FiniteField.frobeniusAlgHom K L) = (FiniteField.frobeniusAlgHom K Ω).comp σ

A K-algebra homomorphism commutes with the finite-base-field Frobenius. Applying the homomorphism and raising to the #K-th power can be done in either order, a ring homomorphism carrying q-th powers to q-th powers.

theorem TauCeti.algebraMap_bijective_of_pow_card_eq_self {K : Type u_1} {L : Type u_2} [Field K] [Fintype K] [CommRing L] [IsDomain L] [Algebra K L] (h : ∀ (x : L), x ^ Fintype.card K = x) : Function.Bijective ⇑(algebraMap K L)

A domain over K all of whose elements satisfy x ^ |K| = x is K itself. Every element is then in the range of the algebra map by TauCeti.FiniteField.pow_card_eq_self_iff_mem_range_algebraMap, which is injective.