The field Frobenius of a Lie-type index

On the ordinary and graph-twisted branches of the CFSG list the Steinberg endomorphism starts from the map x ↦ x ^ q on the algebraic closure of the prime field, where q is the Frobenius parameter recorded by the index; on the Suzuki--Ree and Tits branches the Steinberg map is instead an odd power of a half-Frobenius, whose square is that same x ↦ x ^ q. Either way 𝔽_q is the field of definition, so the map is worth having for every valid index. This file constructs it, TauCeti.ValidLieTypeIndex.frobeniusEquiv, and identifies the field it fixes.

The construction is Mathlib's iterated Frobenius. Writing q = p ^ e with TauCeti.LieTypeIndex.fieldExponent, the map is the e-fold iterate of the p-power Frobenius of TauCeti.ValidLieTypeIndex.Closure, which is a ring automorphism because an algebraically closed field is perfect. Its fixed field is the copy of 𝔽_q inside the closure: it has exactly q elements, it is the unique subfield with that many, and every element of the closure is fixed by some positive iterate. So the ambient field of a group of Lie type is the union of the finite fields that its Frobenius powers cut out, and the field of definition attached to the index is the one cut out by frobeniusEquiv itself.

Nothing here concerns a group. The graph-twisted branches compose this map with a diagram automorphism and the Suzuki--Ree branches replace it by an odd power of a half-Frobenius, and both of those act on a group and not on the field; the field-level map is the same x ↦ x ^ q on every branch, which is why it is defined for every valid index and not only for the untwisted ones.

Main definitions

• TauCeti.ValidLieTypeIndex.frobeniusEquiv: the q-power Frobenius automorphism of the closure.
• TauCeti.ValidLieTypeIndex.fixedField: the subfield it fixes.

Main results

• TauCeti.ValidLieTypeIndex.frobeniusEquiv_apply and TauCeti.ValidLieTypeIndex.iterate_frobeniusEquiv_apply: the Frobenius and its iterates raise to the corresponding powers of q.
• TauCeti.ValidLieTypeIndex.card_fixedField: the fixed field has q elements.
• TauCeti.ValidLieTypeIndex.eq_fixedField_of_natCard: it is the only subfield with q elements.
• TauCeti.ValidLieTypeIndex.nonempty_fixedField_ringEquiv_galoisField: it is a copy of GaloisField p e.
• TauCeti.ValidLieTypeIndex.galoisFieldEmbedding: a chosen embedding of that GaloisField into the closure, with image exactly the fixed field.
• TauCeti.ValidLieTypeIndex.mem_frobeniusFixedSubfield_iff_iterate_frobeniusEquiv_eq: the k-th iterate fixes the subfield at exponent e * k, which for k ≠ 0 is the field of q ^ k elements.
• TauCeti.ValidLieTypeIndex.exists_iterate_frobeniusEquiv_eq: every element of the closure is fixed by some positive iterate.

Roadmap

This is the field-level half of Frob_q in milestone L1 of TauCetiRoadmap/CFSGStatement/README.md, which sets "Frob_q the endomorphism induced on points by x ↦ x ^ d.fieldOrder on the algebraic closure". The endomorphism of points that L1 asks for is induced by this map once milestone L0 supplies the ambient pinned group, which waits on Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md; the map being induced from is this one. The fieldExponent data it uses belongs to the numbered conventions of milestone I0.

References

• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17.
• D. Gorenstein, R. Lyons, and R. Solomon, The Classification of the Finite Simple Groups, Number 3, §2.

The Frobenius automorphism

noncomputable def TauCeti.ValidLieTypeIndex.frobeniusEquiv (d : ValidLieTypeIndex) : d.Closure ≃+* d.Closure

The q-power Frobenius of the algebraic closure attached to a valid Lie-type index, where q = d.fieldOrder.

It is the fieldExponent-fold iterate of the p-power Frobenius, and is an automorphism rather than merely an endomorphism because an algebraically closed field is perfect.

Equations

• d.frobeniusEquiv = iterateFrobeniusEquiv d.Closure d.characteristic d.fieldExponent

@[simp]

theorem TauCeti.ValidLieTypeIndex.frobeniusEquiv_apply (d : ValidLieTypeIndex) (x : d.Closure) : d.frobeniusEquiv x = x ^ d.fieldOrder

The Frobenius attached to an index raises to the power recorded by the index.

theorem TauCeti.ValidLieTypeIndex.coe_frobeniusEquiv (d : ValidLieTypeIndex) : ⇑d.frobeniusEquiv = fun (x : d.Closure) => x ^ d.fieldOrder

The Frobenius attached to an index is the q-power map. This is the form iteration and composition arguments use, frobeniusEquiv_apply being the pointwise one.

This is not a simp lemma: simp only [coe_frobeniusEquiv] already proves frobeniusEquiv_apply, so annotating it would make that lemma a simpNF violation.

theorem TauCeti.ValidLieTypeIndex.iterate_frobeniusEquiv_apply (d : ValidLieTypeIndex) (k : ℕ) (x : d.Closure) : (⇑d.frobeniusEquiv)^[k] x = x ^ d.fieldOrder ^ k

Iterating the Frobenius attached to an index raises to the corresponding power of q. This is the form the graph-twisted branches use: their Steinberg map has an r-th power equal to the plain Frob_{q ^ r}, with r the order of the diagram automorphism.

The field of definition

noncomputable def TauCeti.ValidLieTypeIndex.fixedField (d : ValidLieTypeIndex) : Subfield d.Closure

The subfield of the algebraic closure fixed by the Frobenius attached to a valid Lie-type index: the copy of 𝔽_q inside the closure, with q = d.fieldOrder.

Equations

• d.fixedField = TauCeti.frobeniusFixedSubfield d.Closure d.characteristic d.fieldExponent

theorem TauCeti.ValidLieTypeIndex.fixedField_def (d : ValidLieTypeIndex) : d.fixedField = frobeniusFixedSubfield d.Closure d.characteristic d.fieldExponent

The fixed field is the Frobenius-fixed subfield at the exponent recorded by the index.

@[simp]

theorem TauCeti.ValidLieTypeIndex.mem_fixedField {d : ValidLieTypeIndex} {x : d.Closure} : x ∈ d.fixedField ↔ x ^ d.fieldOrder = x

Membership in the fixed field is the equation x ^ q = x.

theorem TauCeti.ValidLieTypeIndex.mem_fixedField_iff_frobeniusEquiv_eq {d : ValidLieTypeIndex} {x : d.Closure} : x ∈ d.fixedField ↔ d.frobeniusEquiv x = x

The fixed field is the fixed-point set of the Frobenius, which is what makes it the field of definition of the group cut out by that Frobenius.

instance TauCeti.ValidLieTypeIndex.instFiniteSubtypeClosureMemSubfieldFixedField (d : ValidLieTypeIndex) : Finite ↥d.fixedField

The fixed field is finite. The exponent is positive on every branch of the index, so unlike the general statement this needs no side condition.

theorem TauCeti.ValidLieTypeIndex.card_fixedField (d : ValidLieTypeIndex) : Nat.card ↥d.fixedField = d.fieldOrder

The field of definition has q elements. The subfield of the algebraic closure fixed by the Frobenius attached to a valid Lie-type index has exactly d.fieldOrder elements.

This is not a simp lemma: mem_fixedField already rewrites the membership under the coercion, so the left-hand side is not in simp-normal form.

theorem TauCeti.ValidLieTypeIndex.eq_fixedField_of_natCard (d : ValidLieTypeIndex) {F : Subfield d.Closure} (hF : Nat.card ↥F = d.fieldOrder) : F = d.fixedField

The fixed field is the unique subfield of the closure with d.fieldOrder elements, so the index determines it without reference to the Frobenius that cut it out.

theorem TauCeti.ValidLieTypeIndex.nonempty_fixedField_ringEquiv_galoisField (d : ValidLieTypeIndex) : Nonempty (↥d.fixedField ≃+* GaloisField d.characteristic d.fieldExponent)

The fixed field is a copy of Mathlib's GaloisField, non-canonically.

noncomputable def TauCeti.ValidLieTypeIndex.galoisFieldEquivFixedField (d : ValidLieTypeIndex) : GaloisField d.characteristic d.fieldExponent ≃+* ↥d.fixedField

A chosen isomorphism from Mathlib's finite field of order d.fieldOrder to the fixed field inside the closure. There is no canonical such isomorphism; this choice is used only to compare matrix constructions whose coefficients live in the two realizations of the same finite field.

Equations

• d.galoisFieldEquivFixedField = (Classical.choice ⋯).symm

noncomputable def TauCeti.ValidLieTypeIndex.galoisFieldEmbedding (d : ValidLieTypeIndex) : GaloisField d.characteristic d.fieldExponent →+* d.Closure

The embedding of Mathlib's finite field of order d.fieldOrder into the algebraic closure, obtained from a chosen isomorphism with the Frobenius-fixed field.

Equations

• d.galoisFieldEmbedding = d.fixedField.subtype.comp d.galoisFieldEquivFixedField.toRingHom

@[simp]

theorem TauCeti.ValidLieTypeIndex.galoisFieldEmbedding_apply (d : ValidLieTypeIndex) (x : GaloisField d.characteristic d.fieldExponent) : d.galoisFieldEmbedding x = ↑(d.galoisFieldEquivFixedField x)

The finite-field embedding is the inclusion of the chosen fixed-field representative.

theorem TauCeti.ValidLieTypeIndex.range_galoisFieldEmbedding (d : ValidLieTypeIndex) : d.galoisFieldEmbedding.range = d.fixedField.toSubring

The image of the chosen finite-field embedding is exactly the Frobenius-fixed field, viewed as a subring of the closure.

theorem TauCeti.ValidLieTypeIndex.mem_range_galoisFieldEmbedding_iff {d : ValidLieTypeIndex} {x : d.Closure} : x ∈ d.galoisFieldEmbedding.range ↔ x ^ d.fieldOrder = x

An element of the closure belongs to the image of the chosen finite-field embedding exactly when it is fixed by the q-power Frobenius.

This is not a simp lemma: RingHom.mem_range already unfolds the left-hand side into an existential, so it is not in simp-normal form.

theorem TauCeti.ValidLieTypeIndex.mem_frobeniusFixedSubfield_iff_iterate_frobeniusEquiv_eq {d : ValidLieTypeIndex} {k : ℕ} {x : d.Closure} : x ∈ frobeniusFixedSubfield d.Closure d.characteristic (d.fieldExponent * k) ↔ (⇑d.frobeniusEquiv)^[k] x = x

The elements fixed by the k-th iterate of the Frobenius are the fixed subfield at exponent fieldExponent * k, which for k ≠ 0 is by card_frobeniusFixedSubfield the field of q ^ k elements. This identifies the field of definition of a graph-twisted family's ambient untwisted group: the degree r extension of 𝔽_q, with r the order of the diagram automorphism.

theorem TauCeti.ValidLieTypeIndex.exists_iterate_frobeniusEquiv_eq {d : ValidLieTypeIndex} (x : d.Closure) : ∃ (k : ℕ), k ≠ 0 ∧ (⇑d.frobeniusEquiv)^[k] x = x

The closure is the union of the finite fields inside it. Every element of the algebraic closure attached to a valid Lie-type index is fixed by some positive iterate of the Frobenius, hence lies in a finite subfield of the closure.

Together with card_fixedField this places the field of definition of the index inside an exhaustive tower of finite subfields, and it is why the closure, though itself infinite, carries no element that is not algebraic over a field of definition.