The tripled type-D4 carrier preserves its three summands

The tripled carrier acts on V(ϖ₁) ⊕ V(ϖ₃) ⊕ V(ϖ₄), whose coordinates are labelled by TauCeti.DynkinType.d4TripledSummand. Every numbered simple-root operator moves a weight vector to a weight vector of the reflected weight, which lies in the same summand, and the weight torus is diagonal. So all of the generators lie in the block-diagonal subgroup GL₈ × GL₈ × GL₈ of GL₂₄, the weight Levi of the summand labelling. As the carrier is the closed subgroup scheme generated by those morphisms, it lies in that Levi scheme-theoretically: the Levi defining ideal is contained in the carrier's defining ideal. After base change to an arbitrary commutative ring, every matrix coordinate joining two different summands therefore vanishes on the carrier.

This is the input making each union of summands a subcomodule of the carrier's standard representation over every base.

Main results

• TauCeti.D4Tripled.weightLeviDefiningHopfIdeal_le_definingIdeal: the integral carrier is contained in the weight Levi of the summand labelling.
• TauCeti.D4Tripled.coordinateMap_X_eq_zero: over every commutative ring, a matrix coordinate between different summands vanishes in the carrier's coordinate algebra.

References

• J. E. Humphreys, Linear Algebraic Groups, §26.
• J. C. Jantzen, Representations of Algebraic Groups, II.1--2.
• The containment argument follows the upper-triangular containment of positive Kostant subsystems, generalLinearUpperTriangularDefiningHopfIdeal_le_kostantTorusSubsystemDefiningIdeal.

theorem TauCeti.D4Tripled.weightLeviDefiningHopfIdeal_le_definingIdeal : GeneralLinear.weightLeviDefiningHopfIdeal ℤ DynkinType.d4TripledSummand ≤ definingIdeal

The integral tripled carrier lies in the block-diagonal subgroup of its three summands. In Hopf coordinates, the weight-Levi defining ideal of the summand labelling is contained in the carrier's defining ideal.

theorem TauCeti.D4Tripled.coordinateMap_X_eq_zero (A : Type v) [CommRing A] {a b : Fin 24} (hab : DynkinType.d4TripledSummand a ≠ DynkinType.d4TripledSummand b) : (CommHopfAlgCat.Hom.hom (coordinateMap A)) ((GeneralLinear.coordinateHopfAlgebraAlgEquiv A 24) ((GeneralLinear.coordinateRingMap A 24) (MvPolynomial.X (a, b)))) = 0

Over every commutative ring, a matrix coordinate joining two different summands vanishes on the tripled carrier.