Simple root operators on the type-D spin basis

A positive simple root operator sends a spin basis vector of simple-coroot weight -1 to its reflected basis vector, up to an integral unit. A negative operator does the same at weight 1. At a chain node this exchanges an occupied and an unoccupied coordinate; at the fork node it creates or contracts the last two coordinates. Thus these moves preserve half-spin parity and connect the weight lines within each half-spin constituent.

The signs are units of ℤ, so these formulas remain effective after reduction in any characteristic. They supply the root moves needed to recognize invariant subspaces in the spin representation of the corresponding integral matrix carrier.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II.
• W. Fulton and J. Harris, Representation Theory: A First Course, §20.2.
• The proof follows the creation and contraction calculations in TauCeti.TypeBSpinCarrier.exists_rep_rootGenerator_inl_exteriorBasis and TauCeti.TypeBSpinCarrier.exists_rep_rootGenerator_inr_exteriorBasis.

theorem TauCeti.SpinPolarizationData.exists_typeDSpinRep_serreE_exteriorBasis {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) (i : Fin n) (s : Finset (Fin n)) (hs : DynkinType.typeDSpinWeight s i = -1) : ∃ (c : ℤˣ), ((P.typeDSpinRep b hn) ((UniversalEnvelopingAlgebra.ι ℚ) (serreE ℚ (CartanMatrix.D n) i))) (b.ExteriorAlgebra s) = c • b.ExteriorAlgebra (DynkinType.typeDSpinReflection i s)

A positive simple-root operator carries every spin basis vector of simple-coroot weight -1 to its simple reflection, with coefficient an integral unit.

theorem TauCeti.SpinPolarizationData.exists_typeDSpinRep_serreF_exteriorBasis {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) (i : Fin n) (s : Finset (Fin n)) (hs : DynkinType.typeDSpinWeight s i = 1) : ∃ (c : ℤˣ), ((P.typeDSpinRep b hn) ((UniversalEnvelopingAlgebra.ι ℚ) (serreF ℚ (CartanMatrix.D n) i))) (b.ExteriorAlgebra s) = c • b.ExteriorAlgebra (DynkinType.typeDSpinReflection i s)

A negative simple-root operator carries every spin basis vector of simple-coroot weight 1 to its simple reflection, with coefficient an integral unit.