Point actions of the represented F4 carrier quotient #
This file identifies the matrix obtained by evaluating the coordinate morphism of the represented carrier quotient with the corresponding point action on its scalar extension.
theorem
TauCeti.DynkinType.f4ShortRootQuotient_endOfPoint_of_represented
{A : Type u_1}
[CommRing A]
[Algebra (ZMod 2) A]
(g : ↑f4ShortRootCarrierCoordinateHopfAlgebra →ₐ[ZMod 2] A)
(x y : TensorProduct (ZMod 2) A f4ModularChevalleyLieAlgebra)
(h :
(Comodule.endOfPoint f4ShortRootCotangentDual g)
((LinearMap.baseChange A f4ShortRootCarrierCotangentRange.subtype.toLinearMap)
((LinearMap.baseChange A f4ShortRootCarrierRepresentedMap) x)) = (LinearMap.baseChange A f4ShortRootCarrierCotangentRange.subtype.toLinearMap)
((LinearMap.baseChange A f4ShortRootCarrierRepresentedMap) y))
:
An equality of represented vectors under the ambient carrier action descends to the modular quotient.
theorem
TauCeti.DynkinType.f4ShortRootCotangentBaseChangeMatrixEquiv_representedMap
{A : Type}
[CommRing A]
[Algebra (ZMod 2) A]
(x : TensorProduct (ZMod 2) A f4ModularChevalleyLieAlgebra)
:
Matrix coordinates of the scalar-extended represented map are the existing adjoint matrices.
theorem
TauCeti.DynkinType.f4ShortRootCotangentBaseChangeMatrixEquiv_endOfPoint
{A : Type}
[CommRing A]
[Algebra (ZMod 2) A]
(g : ↑f4ShortRootCarrierCoordinateHopfAlgebra →ₐ[ZMod 2] A)
(v : TensorProduct (ZMod 2) A f4ShortRootCotangentDual)
:
have G :=
(GeneralLinear.pointsMulEquiv 26)
(WithConv.toConv
(g.comp
↑(CommHopfAlgCat.Hom.hom
(CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26)
(CommHopfAlgCat.commonKernelHopfIdeal F4ShortRoot.PrimeField.generator)))));
f4ShortRootCotangentBaseChangeMatrixEquiv ((Comodule.endOfPoint f4ShortRootCotangentDual g) v) = ↑G * f4ShortRootCotangentBaseChangeMatrixEquiv v * ↑G⁻¹
The carrier cotangent action, in matrix coordinates, is conjugation by its ambient general-linear point.
theorem
TauCeti.DynkinType.f4ShortRootQuotient_endOfPoint_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))
(x : TensorProduct (ZMod 2) A f4ModularChevalleyLieAlgebra)
:
(Comodule.endOfPoint (f4ModularChevalleyLieAlgebra ⧸ f4ShortRootSubspace) g)
((LinearMap.baseChange A f4ShortRootSubspace.mkQ) x) = (LinearMap.baseChange A f4ShortRootSubspace.mkQ)
((cancelBaseChange ℤ (ZMod 2) A ↥f4ChevalleyLieLattice).symm
((f4RootExponential k (Multiplicative.toAdd u)) ((cancelBaseChange ℤ (ZMod 2) A ↥f4ChevalleyLieLattice) x)))
The action of a carrier root point on the actual quotient comodule is induced by the integral root exponential.
theorem
TauCeti.DynkinType.pointsMulEquiv_comp_f4ShortRootQuotientCoordinateBialgHom
{A : Type u_1}
[CommRing A]
[Algebra (ZMod 2) A]
(g : ↑f4ShortRootCarrierCoordinateHopfAlgebra →ₐ[ZMod 2] A)
:
↑((GeneralLinear.pointsMulEquiv 26) (WithConv.toConv (g.comp ↑f4ShortRootQuotientCoordinateBialgHom))) = (LinearMap.toMatrix (Module.Basis.baseChange A f4ShortRootQuotientBasis)
(Module.Basis.baseChange A f4ShortRootQuotientBasis))
(Comodule.endOfPoint (f4ModularChevalleyLieAlgebra ⧸ f4ShortRootSubspace) g)
Evaluating the represented quotient's coordinate morphism gives the matrix of the induced point action in the prescribed quotient basis.