Root pinning of the represented F4 quotient comodule

The carrier action on its represented middle quotient reverses the numbered roots with the prescribed long- and short-root exponents. These formulas provide the root pinning of the characteristic-two F4 carrier special isogeny.

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.f4ShortRootLieIdealBasis_repr_quotientToIdeal {A : Type} [CommRing A] [Algebra (ZMod 2) A] (x : TensorProduct (ZMod 2) A (f4ModularChevalleyLieAlgebra ⧸ f4ShortRootSubspace)) : (Module.Basis.baseChange A f4ShortRootLieIdealBasis).repr (f4ShortRootQuotientToIdealBaseChange x) = (Module.Basis.baseChange A f4ShortRootQuotientBasis).repr x

The prescribed quotient and ideal bases have the same coordinates under the pinned identification after scalar extension.

theorem TauCeti.DynkinType.f4ShortRootQuotient_endOfPoint_root_pinning {A : Type} [CommRing A] [Algebra (ZMod 2) A] (g : ↑f4ShortRootCarrierCoordinateHopfAlgebra →ₐ[ZMod 2] A) (k : Fin 4 ⊕ Fin 4) (u : Multiplicative A) (hg : (GeneralLinear.pointsMulEquiv 26) (WithConv.toConv (g.comp ↑(CommHopfAlgCat.Hom.hom (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26) (CommHopfAlgCat.commonKernelHopfIdeal F4ShortRoot.PrimeField.generator))))) = ↑((F4ShortRoot.rootSubgroupPoints k A) u)) (a : Fin 26) : f4ShortRootQuotientToIdealBaseChange ((Comodule.endOfPoint (f4ModularChevalleyLieAlgebra ⧸ f4ShortRootSubspace) g) ((Module.Basis.baseChange A f4ShortRootQuotientBasis) a)) = (f4ShortRootExponential (F4ShortRoot.isogenyReverse k) (Multiplicative.toAdd u ^ F4ShortRoot.isogenyExponent k)) ((Module.Basis.baseChange A f4ShortRootLieIdealBasis) a)

Every signed simple-root point acts on the carrier quotient by the prescribed reversed root exponential with parameter exponent one or two.

theorem TauCeti.DynkinType.pointsMulEquiv_f4ShortRootQuotientCoordinateBialgHom_root {A : Type} [CommRing A] [Algebra (ZMod 2) A] (g : ↑f4ShortRootCarrierCoordinateHopfAlgebra →ₐ[ZMod 2] A) (k : Fin 4 ⊕ Fin 4) (u : Multiplicative A) (hg : (GeneralLinear.pointsMulEquiv 26) (WithConv.toConv (g.comp ↑(CommHopfAlgCat.Hom.hom (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26) (CommHopfAlgCat.commonKernelHopfIdeal F4ShortRoot.PrimeField.generator))))) = ↑((F4ShortRoot.rootSubgroupPoints k A) u)) : (GeneralLinear.pointsMulEquiv 26) (WithConv.toConv (g.comp ↑f4ShortRootQuotientCoordinateBialgHom)) = ↑((F4ShortRoot.rootSubgroupPoints (F4ShortRoot.isogenyReverse k) A) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ F4ShortRoot.isogenyExponent k)))

Evaluating the coordinate morphism of the actual quotient comodule at a root point produces the pinned target root matrix.