The Frobenius of the full-weight type-E6 minuscule carrier

The type-E₆ minuscule carrier is the explicit Kostant toral closure over ℤ built from the 27-dimensional minuscule representation 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.E6Minuscule.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 and exponents add under composition. The fixed points are the points of the same carrier over the Frobenius-fixed subring. No reductivity, finiteness, or simplicity statement is involved.

Main declarations

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

References

• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.
• The formal organization follows the carrier specializations TauCeti.Algebra.Lie.SpecialLinear.StandardCarrier.Frobenius and TauCeti.Algebra.Lie.Symplectic.StandardCarrier.Frobenius and uses the carrier's functorial points API.

This advances the Layer 9 target "points over an algebraically closed field as a group, functorially in the field" of TauCetiRoadmap/ReductiveGroups/README.md, which names the q-power Frobenius as its first consumer-facing case. Milestone L1 of TauCetiRoadmap/CFSGStatement/README.md will consume this carrier Frobenius and its root-subgroup equation in a future construction of the ordinary E₆(q) Steinberg map. The identification of this carrier with the required pinned simply connected reductive group remains pending.

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

The p ^ k-power Frobenius endomorphism of the full-weight type-E₆ minuscule carrier.

For p prime, 0 < k, and A an algebraic closure of ZMod p, this is the carrier Frobenius intended for a future construction of the ordinary E₆(p ^ k) Steinberg map.

Equations

• TauCeti.E6Minuscule.frobenius p k A = (TauCeti.E6Minuscule.pointsPresentation A).map (TauCeti.E6Minuscule.pointsPresentation A) (iterateFrobenius A p k)

theorem TauCeti.E6Minuscule.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 minuscule 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.E6Minuscule.coe_frobenius_apply (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points A)) (i j : Fin 27) : ↑↑((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.E6Minuscule.frobenius_rootSubgroupPoints (p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (i : Fin 6 ⊕ Fin 6) (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-E₆ simple-root subgroup to its p ^ k-th power.

@[simp]

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

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

@[simp]

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

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

theorem TauCeti.E6Minuscule.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 minuscule E₆ carrier's point group, in the endomorphism monoid of its points, is its p ^ (k * m)-power Frobenius.

@[simp]

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

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

theorem TauCeti.E6Minuscule.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 full-weight minuscule carrier are its points over the Frobenius-fixed subring.