Documentation

TauCeti.Algebra.Lie.F4.ShortRoot.TorusAction

Torus weights of the modular short-root adjoint representation #

This file records the integral weight support of the adjoint representation on the modular short-root ideal. The support statement is kept over ZMod 2, while the labels remain in the integral character lattice so that they can be used for torus conjugation after scalar extension.

source
theorem TauCeti.DynkinType.f4ShortRootAdjointMatrix_root_weight_support (α : Fin 48) (i j : Fin 26) (hne : f4ShortRootAdjointMatrix (f4ModularRootVector α) i j ≠ 0) :
f4ShortRootWeight i = f4ShortRootWeight j + f4Root α

Every nonzero coefficient of a root-vector adjoint matrix has the corresponding integral weight shift. This retains the characteristic-zero torus labels after reduction modulo two.

source
theorem TauCeti.DynkinType.f4ShortRootAdjointMatrix_simpleCoroot_weight_support (a : Fin F4.rank) (i j : Fin 26) (hne : f4ShortRootAdjointMatrix (f4ModularSimpleCoroot a) i j ≠ 0) :
f4ShortRootWeight i = f4ShortRootWeight j

Simple-coroot adjoint matrices preserve each integral weight coordinate.

source
@[reducible, inline]
noncomputable abbrev TauCeti.DynkinType.f4ShortRootWeightTorusGL {A : Type u_1} [CommRing A] (s : Fin 4 → Aˣ) :
GL (Fin 26) A

The short-root weight torus as an invertible matrix.

Equations
Instances For
    source
    theorem TauCeti.DynkinType.f4ShortRootWeightTorusGL_conj_root {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (s : Fin 4 → Aˣ) (α : Fin 48) :
    ↑(f4ShortRootWeightTorusGL s) * f4ShortRootAdjointMatrixBaseChange (f4ModularRootVector α) * ↑(f4ShortRootWeightTorusGL s)⁻¹ = ↑(torusCharacter s (f4Root α)) • f4ShortRootAdjointMatrixBaseChange (f4ModularRootVector α)

    Conjugation by the actual diagonal torus point scales a represented root vector by its integral root character.

    source
    theorem TauCeti.DynkinType.f4ShortRootWeightTorusGL_conj_simpleCoroot {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (s : Fin 4 → Aˣ) (a : Fin F4.rank) :
    ↑(f4ShortRootWeightTorusGL s) * f4ShortRootAdjointMatrixBaseChange (f4ModularSimpleCoroot a) * ↑(f4ShortRootWeightTorusGL s)⁻¹ = f4ShortRootAdjointMatrixBaseChange (f4ModularSimpleCoroot a)

    Conjugation by the actual diagonal torus point fixes a represented simple coroot.