Frobenius on the full-weight type-A carrier

TauCeti.SlStd.groupScheme r is the explicit full-weight Chevalley carrier of type A_r built from the standard representation of sl_{r+1} and its coordinate integral lattice. For a commutative value ring A of exponential characteristic p, this file equips its point group TauCeti.SlStd.points r A with the p ^ k-power Frobenius endomorphism.

The endomorphism raises every matrix entry to its p ^ k-th power. In particular it satisfies the pinned root-subgroup equation

F(x_i(u)) = x_i(u ^ (p ^ k))

for every Bourbaki-numbered raising or lowering generator, and it raises every coordinate of the split weight torus by the same exponent. Its fixed points are exactly the points of the same carrier over the Frobenius-fixed subring.

The construction is the carrier's functorial point map at the iterated Frobenius of the value ring. Nothing here asserts that the carrier is reductive, or that any fixed-point group is finite or simple.

Main definitions

• TauCeti.SlStd.frobenius: the p ^ k-power Frobenius endomorphism of the type-A_r point group.

Main results

• TauCeti.SlStd.coe_frobenius and TauCeti.SlStd.coe_frobenius_apply: the endomorphism acts by entrywise Frobenius.
• TauCeti.SlStd.frobenius_eq_map: it is the functorial point map induced by the iterated Frobenius endomorphism of the value ring.
• TauCeti.SlStd.frobenius_rootSubgroupPoints and TauCeti.SlStd.frobenius_weightTorusPoints: the equations on the pinned generating root subgroups and split torus.
• TauCeti.SlStd.frobenius_zero, TauCeti.SlStd.frobenius_add and TauCeti.SlStd.frobenius_pow: the iteration laws.
• TauCeti.SlStd.map_subtype_fixedSubgroup_frobenius_eq: the Frobenius-fixed points are the points over the Frobenius-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 organization follows the sibling carrier specialization TauCeti.Algebra.Lie.Orthogonal.TypeB.SpinCarrier.Frobenius.

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

The p ^ k-power Frobenius endomorphism of the full-weight type-A_r carrier.

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

Equations

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

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

The Frobenius endomorphism of the type-A_r carrier acts by entrywise Frobenius.

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

theorem TauCeti.SlStd.frobenius_eq_map (r p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] : frobenius r p k A = (pointsPresentation r A).map (pointsPresentation r A) (iterateFrobenius A p k)

The carrier Frobenius is the functorial map on points induced by the iterated Frobenius endomorphism of the value ring.

@[simp]

theorem TauCeti.SlStd.coe_frobenius_apply (r p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points r A)) (i j : Fin (r + 1)) : ↑↑((frobenius r 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.SlStd.frobenius_rootSubgroupPoints (r p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (i : Fin r ⊕ Fin r) (u : Multiplicative A) : (frobenius r p k A) ((rootSubgroupPoints r i A) u) = (rootSubgroupPoints r i A) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ p ^ k))

Frobenius raises the parameter of a numbered type-A_r root subgroup to its p ^ k-th power.

@[simp]

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

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

@[simp]

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

The zeroth Frobenius iterate is the identity on the type-A_r point group.

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

Frobenius iterates add under composition on the type-A_r point group.

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

Frobenius exponents multiply under taking powers: the m-th power of the p ^ k-power Frobenius of the type-A_r point group, in the endomorphism monoid of its points, is its p ^ (k * m)-power Frobenius.

@[simp]

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

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

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

The Frobenius-fixed points of the full-weight type-A_r carrier are its points over the Frobenius-fixed subring.