Root subgroup moves on the type-D spin coordinate basis

The root subgroup at a simple root moves a coordinate vector of coroot weight -1 by a signed multiple of its reflected coordinate vector. The negative root subgroup does the same at weight 1. The coefficient is the parameter times an integral unit, over any commutative ring. In particular, parameter one gives a nonzero move over every field, including characteristic two.

These formulas transfer the polarized spin-basis calculations to the integral matrix carrier. Together with the two parity orbits of typeDSpinReflection, they provide the root moves needed to propagate an invariant coordinate line throughout its half-spin summand.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II.
• The matrix-to-coordinate calculation follows TauCeti.Algebra.Lie.Orthogonal.TypeB.SpinCarrier.StandardComodule.

theorem TauCeti.TypeDSpinCarrier.rootSubgroupPoints_mulVec_single_sub_of_eq (n : ℕ) (hn : 4 ≤ n) (j : Fin n ⊕ Fin n) {a a' : Fin (dimension n)} {c : ℤˣ} (h : ((rep n hn) ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator (CartanMatrix.D n) j))) ↑((latticeBasis n) a) = c • ↑((latticeBasis n) a')) (A : Type v) [CommRing A] (u : Multiplicative A) : (↑↑((rootSubgroupPoints n hn j A) u)).mulVec (Pi.single a 1) - Pi.single a 1 = (Multiplicative.toAdd u * ↑↑c) • Pi.single a' 1

A signed root-generator column gives the root subgroup's displacement of the corresponding coordinate vector, at every parameter over every commutative ring.

theorem TauCeti.TypeDSpinCarrier.exists_rootSubgroupPoints_inl_mulVec_single_sub (n : ℕ) (hn : 4 ≤ n) (i : Fin n) {a a' : Fin (dimension n)} (ha : basisWeight n a i = -1) (ha' : DynkinType.typeDSpinReflection i (signSet n a) = signSet n a') (A : Type v) [CommRing A] : ∃ (c : ℤˣ), ∀ (u : Multiplicative A), (↑↑((rootSubgroupPoints n hn (Sum.inl i) A) u)).mulVec (Pi.single a 1) - Pi.single a 1 = (Multiplicative.toAdd u * ↑↑c) • Pi.single a' 1

At simple-coroot weight -1, the positive root subgroup moves a spin coordinate vector by the reflected coordinate vector, with a fixed integral-unit sign at every parameter.

theorem TauCeti.TypeDSpinCarrier.exists_rootSubgroupPoints_inr_mulVec_single_sub (n : ℕ) (hn : 4 ≤ n) (i : Fin n) {a a' : Fin (dimension n)} (ha : basisWeight n a i = 1) (ha' : DynkinType.typeDSpinReflection i (signSet n a) = signSet n a') (A : Type v) [CommRing A] : ∃ (c : ℤˣ), ∀ (u : Multiplicative A), (↑↑((rootSubgroupPoints n hn (Sum.inr i) A) u)).mulVec (Pi.single a 1) - Pi.single a 1 = (Multiplicative.toAdd u * ↑↑c) • Pi.single a' 1

At simple-coroot weight 1, the negative root subgroup moves a spin coordinate vector by the reflected coordinate vector, with a fixed integral-unit sign at every parameter.