The Frobenius of the tripled type-D4 carrier

The tripled type-D₄ carrier is the explicit Kostant toral closure over ℤ built from the 24-dimensional representation V(ϖ₁) ⊕ V(ϖ₃) ⊕ V(ϖ₄) and its admissible full-weight lattice. Over a commutative ring A of exponential characteristic p, entrywise p ^ k-th powers preserve its defining Hopf ideal and therefore give a group endomorphism of its A-valued points.

This file names that endomorphism TauCeti.D4Tripled.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 powers. The fixed points are the points of the same carrier over the Frobenius-fixed subring. No reductivity, finiteness, or simplicity statement is involved; no triality automorphism of the carrier is constructed here, so no Steinberg map is formed, and the carrier is not identified with the pinned simply connected group scheme of type D₄.

Main declarations

• TauCeti.D4Tripled.frobenius: the p ^ k-power Frobenius on the carrier's points.
• TauCeti.D4Tripled.frobenius_eq_pointsMap: it is the map on points induced by the iterated Frobenius of the value ring.
• TauCeti.D4Tripled.coe_frobenius and coe_frobenius_apply: its matrix and entrywise actions.
• TauCeti.D4Tripled.frobenius_rootSubgroupPoints: its action on every numbered simple-root subgroup.
• TauCeti.D4Tripled.frobenius_weightTorusPoints: its action on the split weight torus.
• TauCeti.D4Tripled.frobenius_zero, frobenius_add and frobenius_pow: its iteration laws.
• TauCeti.D4Tripled.frobenius_eq_self_iff and TauCeti.D4Tripled.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, §12.2, for the triality-twisted family.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.
• The entrywise Frobenius of the points cut out by a Hopf ideal in a general linear group is TauCeti.Algebra.AlgebraicGroup.Frobenius.GeneralLinear, and its action on a weight-torus matrix is TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Scheme.ToralClosure.Frobenius.

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

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

Equations

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

theorem TauCeti.D4Tripled.frobenius_eq_pointsMap (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] : frobenius p k A = pointsMap (iterateFrobenius A p k)

The Frobenius endomorphism of the tripled carrier is the map on points induced by the iterated Frobenius of the value ring. This is its unfolding lemma, through which the naturality of a symmetry of the carrier, such as triality, yields its commutation with the Frobenius.

theorem TauCeti.D4Tripled.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 tripled carrier acts by entrywise Frobenius.

@[simp]

theorem TauCeti.D4Tripled.coe_frobenius_apply (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points A)) (i j : Fin 24) : ↑↑((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.D4Tripled.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 tripled type-D₄ simple-root subgroup to its p ^ k-th power.

@[simp]

theorem TauCeti.D4Tripled.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.D4Tripled.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 tripled carrier's point group.

theorem TauCeti.D4Tripled.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 tripled carrier's point group.

theorem TauCeti.D4Tripled.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 tripled carrier, in the endomorphism monoid of its points, is its p ^ (k * m)-power Frobenius.

@[simp]

theorem TauCeti.D4Tripled.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 24), ↑↑g i j ∈ frobeniusFixedSubring A p k

A tripled carrier point is fixed by Frobenius exactly when all of its matrix entries lie in the Frobenius-fixed subring.

theorem TauCeti.D4Tripled.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 tripled carrier are its points over the Frobenius-fixed subring.