Concrete type-D Cartan weights on spinors

The split orthogonal model and the Clifford polarization use different coordinates for the same Cartan subalgebra. This file records their common weight calculation: a simple-coroot bivector, and hence the numbered matrix Cartan generator, acts on an exterior-basis spinor by the corresponding integral type-D spin weight. The arbitrary-field calculation factors the rational specialization in TypeD/KostantLattice.lean and supplies the concrete Cartan-action bridge needed when transporting highest-weight data between the orthogonal Lie algebra and the abstract type-D root datum.

Main declarations

• SpinPolarizationData.spinAction_typeDQuadraticEquiv_cartanGenerator_basis: the concrete numbered Cartan generator acts on each exterior-basis vector by its type-D spin weight.
• SpinPolarizationData.typeDSpinLieRep_apply_cartan_exteriorBasis: every element of the diagonal Cartan acts through the corresponding sign-vector weight functional.
• SpinPolarizationData.spinAction_typeDSimpleCorootBivector_basis: the corresponding reusable simple-coroot calculation over any commutative ring.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4–6, Plate IV.
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Section 20.2.

theorem TauCeti.SpinPolarizationData.spinAction_typeDSimpleCorootBivector_basis {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) K ↥P.W) (hn : 2 ≤ n) (i : Fin n) (s : Finset (Fin n)) : ((spinAction Q P) (P.typeDSimpleCorootBivector b hn i)) (b.ExteriorAlgebra s) = (algebraMap ℤ K) (DynkinType.typeDSpinWeight s i) • b.ExteriorAlgebra s

A type-D simple-coroot bivector acts on an exterior-basis spinor by the corresponding integral spin weight in the simply connected root datum.

theorem TauCeti.SpinPolarizationData.spinAction_typeDQuadraticEquiv_cartanGenerator_basis {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) K ↥P.W) [Invertible 2] (hn : 4 ≤ n) (hline : P.line = ⊥) (i : Fin n) (s : Finset (Fin n)) : ((spinAction Q P) ↑((P.typeDQuadraticEquiv b hline) (TypeDStd.cartanGenerator n hn i))) (b.ExteriorAlgebra s) = (algebraMap ℤ K) (DynkinType.typeDSpinWeight s i) • b.ExteriorAlgebra s

The numbered type-D Cartan generator acts on an exterior-basis spinor by the corresponding integral spin weight in the simply connected root datum.

theorem TauCeti.SpinPolarizationData.typeDSpinLieRep_apply_cartan_exteriorBasis {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [Fintype ι] [LinearOrder ι] (b : Module.Basis ι K ↥P.W) [Invertible 2] (hline : P.line = ⊥) (A : ↥(typeDDiagonalCartan K ι)) (s : Finset ι) : ((P.typeDSpinLieRep b hline) ↑A) (b.ExteriorAlgebra s) = (typeDWeightEquiv (spinWeight K s)) A • b.ExteriorAlgebra s

Every element of the diagonal Cartan acts on an exterior-basis spinor through the corresponding sign-vector weight functional.