The prime-field F4 generators preserve the represented flag

This file applies the represented-flag criteria to the actual root and weight-torus coordinate morphisms in the generated short-root carrier over ZMod 2.

theorem TauCeti.DynkinType.f4ShortRootPrimeField_weightTorus_blockTriangular : ((Comodule.coefficientMatrix f4ShortRootCotangentFlagBasis).map ⇑(CommHopfAlgCat.Hom.hom (F4ShortRoot.PrimeField.generator (Sum.inr ())))).BlockTriangular (⇑OrderDual.toDual ∘ f4ShortRootCotangentFlagWeight)

The weight-torus member of the prime-field generating family acts block triangularly on the adapted represented flag.

theorem TauCeti.DynkinType.f4ShortRootPrimeField_root_blockTriangular (k : Fin 4 ⊕ Fin 4) : ((Comodule.coefficientMatrix f4ShortRootCotangentFlagBasis).map ⇑(CommHopfAlgCat.Hom.hom (F4ShortRoot.PrimeField.generator (Sum.inl k)))).BlockTriangular (⇑OrderDual.toDual ∘ f4ShortRootCotangentFlagWeight)

Every root-subgroup member of the prime-field generating family acts block triangularly on the adapted represented flag.