Documentation

TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Frobenius

Invertible matrices fixed by the entrywise Frobenius #

Let A be a commutative ring of exponential characteristic p. Raising every entry to the p ^ k-th power is a group endomorphism Matrix.GeneralLinearGroup.map (iterateFrobenius A p k) of GL ι A, and this file describes its fixed points: an invertible matrix is fixed exactly when all of its entries lie in TauCeti.frobeniusFixedSubring A p k. In the motivating case, p prime, 0 < k, A an algebraic closure of ZMod p and q = p ^ k, the fixed subgroup is GLₙ(𝔽_q) inside GLₙ(A), and the divisibility statement below is the inclusion GLₙ(𝔽_{p ^ m}) ⊆ GLₙ(𝔽_{p ^ l}).

Nothing here needs A to be a field, algebraically closed, or finite, and no coordinate ring or Hopf-algebra theory is involved. Characteristic-free descent to subalgebras and the equalizers of entrywise algebra endomorphisms are treated in TauCeti/LinearAlgebra/Matrix/GeneralLinearGroup/Subalgebra.lean; the group-scheme reading is TauCeti/Algebra/AlgebraicGroup/Frobenius/GeneralLinear.lean.

Main results #

References #

These are the matrix-coordinate form of the Frobenius-fixed points used to construct the finite groups of Lie type; see R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17.

source
@[simp]
theorem Matrix.GeneralLinearGroup.map_iterateFrobenius_eq_self_iff {ι : Type u_1} [DecidableEq ι] [Fintype ι] (p : ℕ) {A : Type u_2} [CommRing A] [ExpChar A p] (k : ℕ) (g : GL ι A) :
(map (iterateFrobenius A p k)) g = g ↔ ∀ (i j : ι), ↑g i j ∈ TauCeti.frobeniusFixedSubring A p k

An invertible matrix is fixed by the entrywise p ^ k-power Frobenius exactly when every one of its entries lies in the Frobenius-fixed subring.

source
theorem Matrix.GeneralLinearGroup.fixedSubgroup_map_iterateFrobenius_zero {ι : Type u_1} [DecidableEq ι] [Fintype ι] (p : ℕ) {A : Type u_2} [CommRing A] [ExpChar A p] :
TauCeti.fixedSubgroup (map (iterateFrobenius A p 0)) = ⊤

The zeroth Frobenius iterate fixes every invertible matrix.

source
theorem Matrix.GeneralLinearGroup.fixedSubgroup_map_iterateFrobenius_le_of_dvd {ι : Type u_1} [DecidableEq ι] [Fintype ι] (p : ℕ) {A : Type u_2} [CommRing A] [ExpChar A p] {m l : ℕ} (hml : m ∣ l) :
TauCeti.fixedSubgroup (map (iterateFrobenius A p m)) ≤ TauCeti.fixedSubgroup (map (iterateFrobenius A p l))

The subgroups of entrywise Frobenius-fixed matrices grow along divisibility of the exponent. In the motivating case this is the inclusion GLₙ(𝔽_{p ^ m}) ⊆ GLₙ(𝔽_{p ^ l}).