Complete reducibility of the type-D spin carrier representation

Over every field, the standard representation of the full-weight type-Dₙ spin carrier is completely reducible. The distinct torus characters extract its coordinate lines, and positive and negative simple-root points propagate each line through its entire half-spin parity class. The coordinate lines absent from a subcomodule therefore form a union of half-spin summands and give an invariant complement.

The torus coaction, rather than rational torus points, separates weights. Root moves have integral-unit coefficients. Thus the result includes finite fields and characteristic two. Together with faithfulness it allows elimination of normal smooth unipotent subgroups. The criterion TauCeti.TypeDSpinCarrier.isCompletelyReducible_of_spinWeights_of_rootSubgroupPoints uses only the torus weights, numbered root actions, and parity of matrix coefficients, so it also applies to the subgroup generated directly over the coefficient field.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II.
• J. C. Jantzen, Representations of Algebraic Groups, I.2 and II.2.

The coordinate-complement argument follows TauCeti.Algebra.Lie.E6.DoubledMinuscule.CompletelyReducible; signed root propagation follows TauCeti.Algebra.Lie.Orthogonal.TypeB.SpinCarrier.StandardComodule.

theorem TauCeti.TypeDSpinCarrier.single_mem_of_parity_eq_of_rootSubgroupPoints (n : ℕ) (hn : 4 ≤ n) (R : Type u) [CommRing R] (N : Submodule R (Fin (dimension n) → R)) (hroot : ∀ (j : Fin n ⊕ Fin n), ∀ v ∈ N, (↑↑((rootSubgroupPoints n hn j R) (Multiplicative.ofAdd 1))).mulVec v ∈ N) {a b : Fin (dimension n)} (hab : ↑(signSet n a).card = ↑(signSet n b).card) (hb : Pi.single b 1 ∈ N) : Pi.single a 1 ∈ N

A submodule stable under the numbered spin root matrices containing one coordinate line contains every coordinate line in its half-spin parity class.

theorem TauCeti.TypeDSpinCarrier.isCompletelyReducible_of_spinWeights_of_rootSubgroupPoints (n : ℕ) (hn : 4 ≤ n) (k : Type u) [Field k] {H : Type u_1} [AddCommGroup H] [Module k H] [Coalgebra k H] [Comodule k H (Fin (dimension n) → k)] (τ : H →ₗc[k] ↑(DiagonalizableGroup.coordinateRing k (SplitTorus.characterGroup (Fin n))).obj) (hτ : Comodule.Corestrict τ = Comodule.ofWeights (Pi.basisFun k (Fin (dimension n))) (basisCharacter n)) (hroot : ∀ (N : Subcomodule k H (Fin (dimension n) → k)) (j : Fin n ⊕ Fin n), ∀ v ∈ N, (↑↑((rootSubgroupPoints n hn j k) (Multiplicative.ofAdd 1))).mulVec v ∈ N) (hparity : ∀ (a b : Fin (dimension n)), basisParity n a ≠ basisParity n b → Comodule.coefficientMatrix (Pi.basisFun k (Fin (dimension n))) a b = 0) : Comodule.IsCompletelyReducible k H (Fin (dimension n) → k)

A comodule with the distinct spin torus weights, the numbered root actions, and no coefficients mixing half-spin parity is completely reducible.

theorem TauCeti.TypeDSpinCarrier.isCompletelyReducible_standardComodule (n : ℕ) (hn : 4 ≤ n) (k : Type u) [Field k] : Comodule.IsCompletelyReducible k (↑(coordinateHopfAlgebra n hn k)) (Fin (dimension n) → k)

The standard representation of the full-weight type-Dₙ spin carrier is completely reducible over every field, including characteristic two.