Torus pinning of the represented F4 quotient comodule

The weight-torus action on the represented F4 quotient is diagonal in its canonical basis, with weights given by the special character-lattice map. This torus pinning and the root formulas characterize the carrier special isogeny on its generators.

References

• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.
• R. W. Carter, Simple Groups of Lie Type, §12.3.

theorem TauCeti.DynkinType.f4ShortRootWeightTorusConj_quotientLift {A : Type} [CommRing A] [Algebra (ZMod 2) A] (s : Fin 4 → Aˣ) (a : Fin 26) : ((↑(f4ShortRootWeightTorusGL s)).lieConj (Units.invertible (f4ShortRootWeightTorusGL s))) (f4ShortRootAdjointMatrixBaseChange (f4ShortRootQuotientLift a)) = ↑(torusCharacter s (f4ShortRootQuotientWeight a)) • f4ShortRootAdjointMatrixBaseChange (f4ShortRootQuotientLift a)

Conjugation scales the represented canonical quotient lift by its long-root character, with character zero on the two Cartan coordinates.

theorem TauCeti.DynkinType.f4ShortRootQuotient_endOfPoint_torus {A : Type} [CommRing A] [Algebra (ZMod 2) A] (g : ↑f4ShortRootCarrierCoordinateHopfAlgebra →ₐ[ZMod 2] A) (s : Fin 4 → Aˣ) (hg : (GeneralLinear.pointsMulEquiv 26) (WithConv.toConv (g.comp ↑(CommHopfAlgCat.Hom.hom (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26) (CommHopfAlgCat.commonKernelHopfIdeal F4ShortRoot.PrimeField.generator))))) = f4ShortRootWeightTorusGL s) (a : Fin 26) : (Comodule.endOfPoint (f4ModularChevalleyLieAlgebra ⧸ f4ShortRootSubspace) g) ((Module.Basis.baseChange A f4ShortRootQuotientBasis) a) = ↑(torusCharacter (f4SpecialIsogenyTorusMap s) (f4ShortRootWeight a)) • (Module.Basis.baseChange A f4ShortRootQuotientBasis) a

The actual quotient carrier action is diagonal on the prescribed quotient basis, with weights pulled back along the special torus map.

theorem TauCeti.DynkinType.pointsMulEquiv_f4ShortRootQuotientCoordinateBialgHom_torus {A : Type} [CommRing A] [Algebra (ZMod 2) A] (g : ↑f4ShortRootCarrierCoordinateHopfAlgebra →ₐ[ZMod 2] A) (s : Fin 4 → Aˣ) (hg : (GeneralLinear.pointsMulEquiv 26) (WithConv.toConv (g.comp ↑(CommHopfAlgCat.Hom.hom (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26) (CommHopfAlgCat.commonKernelHopfIdeal F4ShortRoot.PrimeField.generator))))) = f4ShortRootWeightTorusGL s) : (GeneralLinear.pointsMulEquiv 26) (WithConv.toConv (g.comp ↑f4ShortRootQuotientCoordinateBialgHom)) = f4ShortRootWeightTorusGL (f4SpecialIsogenyTorusMap s)

Evaluating the quotient coordinate map at a weight-torus point applies the special torus map to that point.