The type-D spin carrier preserves its two half-spin summands

The full-weight type-Dₙ spin carrier acts on the whole spin module S = S⁺ ⊕ S⁻, the even and odd parts of the exterior algebra whose coordinate basis is indexed by sign sets. The coordinate at a sign set lies in S⁺ or S⁻ according to the parity of its cardinality, TauCeti.TypeDSpinCarrier.basisParity.

Every numbered simple-root operator acts through an even Clifford element, so its integral matrix never joins the two parities, and the weight torus is diagonal. So all of the generators lie in the block-diagonal subgroup GL(S⁺) × GL(S⁻) of GL_(2^n), the weight Levi of the parity 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 the two half-spin summands therefore vanishes on the carrier.

This is the input making S⁺ and S⁻ subcomodules of the carrier's standard representation over every base.

Main declarations

• TauCeti.TypeDSpinCarrier.basisParity: the half-spin summand of a spin-basis index.

Main results

• TauCeti.TypeDSpinCarrier.weightLeviDefiningHopfIdeal_le_definingIdeal: the integral carrier is contained in the weight Levi of the parity labelling.
• TauCeti.TypeDSpinCarrier.coordinateMap_X_eq_zero: over every commutative ring, a matrix coordinate between the two half-spin summands vanishes in the carrier's coordinate algebra.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II.
• W. Fulton and J. Harris, Representation Theory: A First Course, §20.2.
• J. C. Jantzen, Representations of Algebraic Groups, II.1--2.

The containment argument follows the one for the summands of the tripled type-D₄ carrier in TauCeti.Algebra.Lie.D4.Tripled.Levi.

noncomputable def TauCeti.TypeDSpinCarrier.basisParity (n : ℕ) (a : Fin (dimension n)) : ℤ

The half-spin summand of a spin-basis index, recorded as the parity of the cardinality of its sign set: 0 for a coordinate of the even summand S⁺ and 1 for one of the odd summand S⁻.

Equations

• TauCeti.TypeDSpinCarrier.basisParity n a = ↑((TauCeti.TypeDSpinCarrier.signSet n a).card % 2)

theorem TauCeti.TypeDSpinCarrier.basisParity_eq_basisParity_iff (n : ℕ) {a b : Fin (dimension n)} : basisParity n a = basisParity n b ↔ ↑(signSet n a).card = ↑(signSet n b).card

Two spin-basis indices lie in the same half-spin summand exactly when the cardinalities of their sign sets have the same parity.

theorem TauCeti.TypeDSpinCarrier.weightLeviDefiningHopfIdeal_le_definingIdeal (n : ℕ) (hn : 4 ≤ n) : GeneralLinear.weightLeviDefiningHopfIdeal ℤ (basisParity n) ≤ definingIdeal n hn

The integral type-Dₙ spin carrier lies in the block-diagonal subgroup of its two half-spin summands. In Hopf coordinates, the weight-Levi defining ideal of the parity labelling is contained in the carrier's defining ideal.

theorem TauCeti.TypeDSpinCarrier.coordinateMap_X_eq_zero (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] {a b : Fin (dimension n)} (hab : basisParity n a ≠ basisParity n b) : (CommHopfAlgCat.Hom.hom (coordinateMap n hn A)) ((GeneralLinear.coordinateHopfAlgebraAlgEquiv A (dimension n)) ((GeneralLinear.coordinateRingMap A (dimension n)) (MvPolynomial.X (a, b)))) = 0

Over every commutative ring, a matrix coordinate joining the two half-spin summands vanishes on the type-Dₙ spin carrier.