The Frobenius of the short-root type-F4 carrier

TauCeti.F4ShortRoot.groupScheme is the explicit short-root type-F₄ Chevalley carrier over ℤ, the Kostant toral closure built from the 26-dimensional representation with highest weight ϖ₄ and its admissible lattice, and TauCeti.F4ShortRoot.points A realizes its A-valued points as a subgroup of GL₂₆(A). Over a commutative ring A of exponential characteristic p, entrywise p ^ k-th powers are a homomorphism of value rings, so the carrier's functoriality turns them into a group endomorphism of its points.

This file names that endomorphism TauCeti.F4ShortRoot.frobenius and records its characteristic equations:

F (g)ᵢⱼ = gᵢⱼ ^ (p ^ k),
F (xᵢ(u)) = xᵢ(u ^ (p ^ k)),
F (t(s)) = t(s ^ (p ^ k)).

The zeroth iterate is the identity, exponents add under composition and multiply under taking powers in the endomorphism monoid, and the fixed points are the points of the same carrier over the Frobenius-fixed subring of A.

The F₄ diagram has no nontrivial symmetry, so the only twist a Steinberg endomorphism built on this carrier can carry is the special isogeny of characteristic two, whose square is the ordinary two-power Frobenius, the case p = 2 and k = 1 below; that isogeny is not constructed in this file. Nothing here asserts reductivity, maximality of the weight torus, an identification of the carrier's root datum, or any finiteness or simplicity statement.

Main declarations

• TauCeti.F4ShortRoot.frobenius: the p ^ k-power Frobenius on the carrier's points.
• TauCeti.F4ShortRoot.coe_frobenius and coe_frobenius_apply: its matrix and entrywise actions.
• TauCeti.F4ShortRoot.frobenius_rootSubgroupPoints: its action on every numbered simple-root subgroup.
• TauCeti.F4ShortRoot.frobenius_weightTorusPoints: its action on the split weight torus.
• TauCeti.F4ShortRoot.frobenius_zero, frobenius_add and frobenius_pow: its iteration laws.
• TauCeti.F4ShortRoot.frobenius_eq_self_iff and TauCeti.F4ShortRoot.map_subtype_fixedSubgroup_frobenius_eq: which points it fixes, and the identification of the fixed subgroup with the points over the Frobenius-fixed subring.

References

• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17.
• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 11.3.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.
• The corresponding formal type-E₇ construction in TauCeti.Algebra.Lie.E7.Minuscule.Frobenius.

noncomputable def TauCeti.F4ShortRoot.frobenius (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] : ↥(points A) →* ↥(points A)

The p ^ k-power Frobenius endomorphism of the short-root type-F₄ carrier, the functorial map on points induced by the iterated Frobenius endomorphism of the value ring.

For p prime, 0 < k and A an algebraic closure of ZMod p, this is the q-power Frobenius of the carrier's points for q = p ^ k.

Equations

• TauCeti.F4ShortRoot.frobenius p k A = TauCeti.F4ShortRoot.pointsMap (iterateFrobenius A p k)

theorem TauCeti.F4ShortRoot.coe_frobenius (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points A)) : ↑((frobenius p k A) g) = (Matrix.GeneralLinearGroup.map (iterateFrobenius A p k)) ↑g

The Frobenius endomorphism of the short-root type-F₄ carrier acts by entrywise Frobenius.

This is not a simp lemma because coe_frobenius_apply is the canonical coefficient-level normal form.

@[simp]

theorem TauCeti.F4ShortRoot.coe_frobenius_apply (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points A)) (i j : Fin 26) : ↑↑((frobenius p k A) g) i j = ↑↑g i j ^ p ^ k

Entrywise, the Frobenius endomorphism raises each matrix coefficient to its p ^ k-th power.

@[simp]

theorem TauCeti.F4ShortRoot.frobenius_rootSubgroupPoints (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (i : Fin 4 ⊕ Fin 4) (u : Multiplicative A) : (frobenius p k A) ((rootSubgroupPoints i A) u) = (rootSubgroupPoints i A) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ p ^ k))

Frobenius raises the parameter of every numbered type-F₄ simple-root subgroup to its p ^ k-th power, on both the raising and the lowering generators.

@[simp]

theorem TauCeti.F4ShortRoot.frobenius_weightTorusPoints (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (s : Fin 4 → Aˣ) : (frobenius p k A) ((weightTorusPoints A) s) = (weightTorusPoints A) (s ^ p ^ k)

Frobenius raises every coordinate of the pinned split weight torus to its p ^ k-th power.

@[simp]

theorem TauCeti.F4ShortRoot.frobenius_zero (p : ℕ) (A : Type v) [CommRing A] [ExpChar A p] : frobenius p 0 A = MonoidHom.id ↥(points A)

The zeroth Frobenius iterate is the identity on the short-root type-F₄ carrier's point group.

theorem TauCeti.F4ShortRoot.frobenius_add (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (m : ℕ) : frobenius p (k + m) A = (frobenius p k A).comp (frobenius p m A)

Frobenius iterates add under composition on the short-root type-F₄ carrier's point group.

theorem TauCeti.F4ShortRoot.frobenius_pow (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (m : ℕ) : (have this := frobenius p k A; this) ^ m = frobenius p (k * m) A

Frobenius exponents multiply under taking powers: the m-th power of the p ^ k-power Frobenius of the short-root type-F₄ carrier, in the endomorphism monoid of its points, is its p ^ (k * m)-power Frobenius.

@[simp]

theorem TauCeti.F4ShortRoot.frobenius_eq_self_iff (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points A)) : (frobenius p k A) g = g ↔ ∀ (i j : Fin 26), ↑↑g i j ∈ frobeniusFixedSubring A p k

A short-root type-F₄ carrier point is fixed by Frobenius exactly when all of its matrix entries lie in the Frobenius-fixed subring.

theorem TauCeti.F4ShortRoot.map_subtype_fixedSubgroup_frobenius_eq (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] : Subgroup.map (points A).subtype (fixedSubgroup (frobenius p k A)) = Subgroup.map (Matrix.GeneralLinearGroup.map (frobeniusFixedSubring A p k).subtype) (points ↥(frobeniusFixedSubring A p k))

The Frobenius-fixed points of the short-root type-F₄ carrier are its points over the Frobenius-fixed subring. No finiteness of either side is asserted.