The Frobenius endomorphism of the points of the pinned Geck carrier

TauCeti.DynkinType.geckGroupScheme is the explicit affine group scheme over ℤ attached to a valid Dynkin type: the closed subgroup scheme of GLₙ generated by the divided-power exponential root subgroups of the Bourbaki-numbered Chevalley generators together with the weight torus of the Geck coordinate lattice. The shared GeneralLinear.IntegralPointsPresentation.map supplies the map its points inherit from a homomorphism of value rings. This file reads that functoriality at the p ^ k-power Frobenius of the value ring and derives the resulting endomorphism's interface from the general one.

For a value ring A of exponential characteristic p and q = p ^ k, the resulting endomorphism F of TauCeti.DynkinType.geckPoints raises every matrix entry to its q-th power, so on the pinned generating families it acts by

F (xᵢ(u)) = xᵢ(u ^ q),        F (t(s)) = t(s ^ q),

with i ranging over the numbered raising and lowering generators. Its fixed points, read inside GLₙ(A), are the points of the same carrier valued in the Frobenius-fixed subring of A; for p prime, 0 < k and A an algebraic closure of ZMod p, that subring is the field of q elements.

Two limitations are worth stating. This is the Frobenius of the carrier, not of the elementary subgroup its root subgroups generate: identifying the two needs a generation theorem that is not available, so no statement here restricts to the elementary group. And the Geck weights span the root lattice rather than, in general, the full character lattice, so this carrier is not yet the simply connected one a finite group of Lie type is built from. Nothing below asserts that any subgroup appearing in it is finite, is simple, or is a named finite group.

Main definitions

• TauCeti.DynkinType.geckFrobenius: the p ^ k-power Frobenius as a group endomorphism of the points of the pinned Geck carrier.

Main results

• TauCeti.DynkinType.coe_geckFrobenius: the endomorphism acts by the entrywise Frobenius.
• TauCeti.DynkinType.geckFrobenius_zero, TauCeti.DynkinType.geckFrobenius_add and TauCeti.DynkinType.geckFrobenius_pow: the iteration laws, the last of them saying that exponents multiply under taking powers in the endomorphism monoid.
• TauCeti.DynkinType.geckFrobenius_eq_self_iff: a carrier point is fixed exactly when all of its matrix entries are fixed.
• TauCeti.DynkinType.geckFrobenius_geckRootSubgroupPoints and TauCeti.DynkinType.geckFrobenius_geckWeightTorusPoints: the equations on the pinned root subgroups and on the pinned weight torus.
• TauCeti.DynkinType.map_subtype_fixedSubgroup_geckFrobenius_eq: the Frobenius-fixed points of the carrier are its points over the Frobenius-fixed subring.

References

• M. Geck, On the construction of semisimple Lie algebras and Chevalley groups, Proc. Amer. Math. Soc. 145 (2017), 3233--3247.
• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

This is the pinned instance of the target "points over an algebraically closed field as a group, functorially in the field, so that a field endomorphism induces a group endomorphism of the points" in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, which names the q-power Frobenius as the first case a consumer asks for. Its consumer is milestone L1 of TauCetiRoadmap/CFSGStatement/README.md, whose untwisted Steinberg map ValidLieTypeIndex.frobenius is Frob_q on the points of a pinned Chevalley--Demazure group and whose completion evidence is the simple-root-subgroup equations, together with milestone L3, which sets H_d = fixedSubgroup d.steinberg.

noncomputable def TauCeti.DynkinType.geckFrobenius (t : DynkinType) (ht : t.Valid) (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] : ↥(t.geckPoints ht A) →* ↥(t.geckPoints ht A)

The p ^ k-power Frobenius endomorphism of the points of the pinned Geck carrier.

For p prime, 0 < k and A an algebraic closure of ZMod p this is the untwisted Steinberg endomorphism of the carrier; for k = 0, or in characteristic zero, it is the identity.

Equations

• t.geckFrobenius ht p k A = (t.geckPointsPresentation ht A).map (t.geckPointsPresentation ht A) (iterateFrobenius A p k)

@[simp]

theorem TauCeti.DynkinType.coe_geckFrobenius (t : DynkinType) (ht : t.Valid) (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(t.geckPoints ht A)) : ↑((t.geckFrobenius ht p k A) g) = (Matrix.GeneralLinearGroup.map (iterateFrobenius A p k)) ↑g

The Frobenius endomorphism of the points of the pinned Geck carrier acts by the entrywise Frobenius.

theorem TauCeti.DynkinType.coe_geckFrobenius_apply (t : DynkinType) (ht : t.Valid) (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(t.geckPoints ht A)) (r c : Fin (t.geckDim ht)) : ↑↑((t.geckFrobenius ht p k A) g) r c = ↑↑g r c ^ p ^ k

Entrywise, the Frobenius endomorphism of the points of the pinned Geck carrier raises each entry to the p ^ k-th power.

@[simp]

theorem TauCeti.DynkinType.geckFrobenius_zero (t : DynkinType) (ht : t.Valid) (p : ℕ) (A : Type v) [CommRing A] [ExpChar A p] : t.geckFrobenius ht p 0 A = MonoidHom.id ↥(t.geckPoints ht A)

The zeroth Frobenius iterate is the identity on the points of the pinned Geck carrier.

theorem TauCeti.DynkinType.geckFrobenius_add (t : DynkinType) (ht : t.Valid) (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (m : ℕ) : t.geckFrobenius ht p (k + m) A = (t.geckFrobenius ht p k A).comp (t.geckFrobenius ht p m A)

Frobenius iterates add under composition on the points of the pinned Geck carrier.

theorem TauCeti.DynkinType.geckFrobenius_pow (t : DynkinType) (ht : t.Valid) (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (m : ℕ) : (have this := t.geckFrobenius ht p k A; this) ^ m = t.geckFrobenius ht p (k * m) A

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

@[simp]

theorem TauCeti.DynkinType.geckFrobenius_eq_self_iff (t : DynkinType) (ht : t.Valid) (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(t.geckPoints ht A)) : (t.geckFrobenius ht p k A) g = g ↔ ∀ (r c : Fin (t.geckDim ht)), ↑↑g r c ∈ frobeniusFixedSubring A p k

A point of the pinned Geck carrier is fixed by its Frobenius endomorphism exactly when every one of its matrix entries lies in the Frobenius-fixed subring.

@[simp]

theorem TauCeti.DynkinType.geckFrobenius_geckRootSubgroupPoints (t : DynkinType) (ht : t.Valid) (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (i : Fin t.rank ⊕ Fin t.rank) (u : Multiplicative A) : (t.geckFrobenius ht p k A) ((t.geckRootSubgroupPoints ht i A) u) = (t.geckRootSubgroupPoints ht i A) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ p ^ k))

The Frobenius raises the parameter of a numbered root subgroup inside the Geck carrier points to its p ^ k-th power.

@[simp]

theorem TauCeti.DynkinType.geckFrobenius_geckWeightTorusPoints (t : DynkinType) (ht : t.Valid) (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (s : Fin t.rank → Aˣ) : (t.geckFrobenius ht p k A) ((t.geckWeightTorusPoints ht A) s) = (t.geckWeightTorusPoints ht A) (s ^ p ^ k)

The Frobenius raises a point of the pinned Geck weight torus to its p ^ k-th power.

theorem TauCeti.DynkinType.map_subtype_fixedSubgroup_geckFrobenius_eq (t : DynkinType) (ht : t.Valid) (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] : Subgroup.map (t.geckPoints ht A).subtype (fixedSubgroup (t.geckFrobenius ht p k A)) = Subgroup.map (Matrix.GeneralLinearGroup.map (frobeniusFixedSubring A p k).subtype) (t.geckPoints ht ↥(frobeniusFixedSubring A p k))

The Frobenius-fixed points of the pinned Geck carrier are its points over the Frobenius-fixed subring. For p prime, 0 < k, A an algebraic closure of ZMod p and q = p ^ k this is G(𝔽_q) = G(A)^F for the pinned Chevalley carrier of a valid Dynkin type.