Weight-torus stability of the represented modular F4 flag

The short-root weight torus preserves the represented ideal and range in matrix coordinates. Transporting those two facts through the cotangent-dual matrix equivalence makes its adjoint coefficient matrix block triangular for the adapted weights 2, 1, 0.

theorem TauCeti.DynkinType.f4ShortRootWeightTorusConj_mem_representedRange {A : Type} [CommRing A] [Algebra (ZMod 2) A] (s : Fin 4 → Aˣ) {X : Matrix (Fin 26) (Fin 26) A} (hX : X ∈ f4ShortRootRepresentedRangeMatrixBaseChange) : ((↑(f4ShortRootWeightTorusGL s)).lieConj (Units.invertible (f4ShortRootWeightTorusGL s))) X ∈ f4ShortRootRepresentedRangeMatrixBaseChange

The base-changed represented range is preserved by every short-root weight-torus point.

theorem TauCeti.DynkinType.f4ShortRootWeightTorusConj_mem_representedIdeal {A : Type} [CommRing A] [Algebra (ZMod 2) A] (s : Fin 4 → Aˣ) {X : Matrix (Fin 26) (Fin 26) A} (hX : X ∈ f4ShortRootRepresentedIdealMatrixBaseChange) : ((↑(f4ShortRootWeightTorusGL s)).lieConj (Units.invertible (f4ShortRootWeightTorusGL s))) X ∈ f4ShortRootRepresentedIdealMatrixBaseChange

The base-changed represented ideal is preserved by every short-root weight-torus point.

theorem TauCeti.DynkinType.f4ShortRootWeightTorus_adjoint_blockTriangular {A : Type} [CommRing A] [Algebra (ZMod 2) A] (g : ↑(HopfAlgebra.points ↧A)) (s : Fin 4 → Aˣ) (hg : (GeneralLinear.pointsMulEquiv 26) g = f4ShortRootWeightTorusGL s) : ((Comodule.coefficientMatrix f4ShortRootCotangentFlagBasis).map ⇑g.ofConv).BlockTriangular (⇑OrderDual.toDual ∘ f4ShortRootCotangentFlagWeight)

Every short-root weight-torus point acts block triangularly on the adapted represented flag.