Finite-field coordinates for groups of Lie type

The fixed-point constructions of finite groups of Lie type use matrices over algebraic closures of prime fields, while concrete finite matrix groups are naturally written over Mathlib's GaloisField p e. This file supplies the coordinate bridge between those realizations of the field with p ^ e elements.

For a valid Lie-type index d, TauCeti.ValidLieTypeIndex.galoisFieldEmbedding embeds Mathlib's finite field into d.Closure with image the d.fieldOrder-Frobenius-fixed field. The results below lift that embedding entrywise to matrices and invertible matrices. In particular, a matrix over the closure comes from finite-field coordinates exactly when each of its entries is fixed by the field Frobenius.

The Suzuki comparison is the immediate consumer: its fixed-point carrier is defined over the closure, while the explicit four-dimensional matrix group is defined over GaloisField 2 (2 * m + 1). No group comparison is made here; these results identify only the coefficient fields and their matrix coordinates.

Main result

• Matrix.GeneralLinearGroup.mem_range_map_galoisFieldEmbedding_iff: an invertible matrix over the closure comes from the finite field exactly when its entries are Frobenius-fixed.

References

• M. Suzuki, On a class of doubly transitive groups, Annals of Mathematics 75 (1962), 105--145.

theorem Matrix.exists_map_galoisFieldEmbedding_iff_frobenius {d : TauCeti.ValidLieTypeIndex} {m : Type u_1} {n : Type u_2} (A : Matrix m n d.Closure) : (∃ (B : Matrix m n (GaloisField d.characteristic d.fieldExponent)), B.map ⇑d.galoisFieldEmbedding = A) ↔ ∀ (i : m) (j : n), A i j ^ d.fieldOrder = A i j

A matrix over the closure has finite-field coordinates exactly when every entry is fixed by the q-power Frobenius.

theorem Matrix.GeneralLinearGroup.mem_range_map_galoisFieldEmbedding_iff {d : TauCeti.ValidLieTypeIndex} {n : Type u_1} [Fintype n] [DecidableEq n] (g : GL n d.Closure) : g ∈ (map d.galoisFieldEmbedding).range ↔ ∀ (i j : n), ↑g i j ^ d.fieldOrder = ↑g i j

An invertible matrix over the closure comes by scalar extension from Mathlib's finite field exactly when every matrix entry is fixed by the q-power Frobenius.

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