The last-fundamental-weight vector in the type-B spin representation #

The spin module of an odd polarization is the exterior algebra S = ⋀·W of the first isotropic summand, acted on by the split type-B matrix Lie algebra through TauCeti.SpinPolarizationData.typeBSpinLieRep. Its exterior basis diagonalizes the numbered simple coroots, with integral eigenvalues TauCeti.SpinPolarizationData.typeBSpinCorootWeight read off which coordinates occur; the underlying weights are the half-integral sign vectors ½(±1, …, ±1) of TauCeti.spinWeight. The last fundamental weight ωₗ of Bₙ₊₁, the one attached to the terminal short node of the Dynkin diagram, is carried by the basis vector with every coordinate occupied. This file combines two facts that identify that vector:

every positive simple-root generator annihilates it, hence so does the Lie subalgebra they generate;
its coroot weight is Pi.single (Fin.last n) 1, that last fundamental weight.

These are the generator-level inputs for a highest-weight identification, namely the identification S ≅ L(ωₗ) of the type-B spin module with the irreducible highest-weight module at the last fundamental weight. A promotion to TauCeti.IsHighestWeightVector additionally requires a compatible Borel and the proof that its positive nilradical is generated by the displayed positive root spaces; no such Borel is asserted here. The same gap is left by the type-D fork vectors in TauCeti/RepresentationTheory/Spin/Polarization/TypeD/ForkWeights.lean, whose statements these mirror.

The annihilation is read off the two ways a simple-root generator acts on the exterior basis. The terminal short generator creates the last coordinate (after the grade involution, and scaled by the line coordinate of the distinguished remainder vector), and that coordinate is already present, so the result vanishes. A nonterminal long generator e_{εⱼ - εⱼ₊₁} contracts the (j+1)-st coordinate and then creates the j-th one, which the contraction left untouched, so that vanishes too. Neither computation depends on the normalization of the remainder vector: the scalar is irrelevant once the wedge is zero. Both read off the same condition, that the coordinate the generator creates is already occupied, so the annihilation is stated for every index set containing that coordinate; the all-coordinate vector, where this holds for every generator at once, is the case used here.

The annihilation statements hold over any field in which 2 is invertible, which is all the underlying Clifford comparison needs. The weight-vector statement is over ℚ, where TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector lives.

Main results #

TauCeti.SpinPolarizationData.typeBSpinLieRep_simpleRootGenerator_exteriorBasis_eq_zero_of_mem: a positive simple-root generator annihilates every exterior-basis vector whose index set contains the generator's own coordinate, in particular the all-coordinate one.
typeBSpinLieRep_lieSpan_range_simpleRootGenerator_le_lieAnnihilator, in the same namespace: generatorwise vanishing extends to the Lie subalgebra the positive simple-root generators generate, with typeBSpinLieRep_lieSpan_range_simpleRootGenerator_le_lieAnnihilator_exteriorBasis_univ its instance at the all-coordinate vector.
TauCeti.SpinPolarizationData.isCartanWeightVector_typeBSpinRep_exteriorBasis_univ: the all-coordinate vector has the last fundamental weight.

References #

C. Chevalley, The Algebraic Theory of Spinors, Chapter II.
W. Fulton and J. Harris, Representation Theory: A First Course (1991), Section 20.2.
N. Bourbaki, Groupes et algèbres de Lie, Chapters 4--6, Planche II.

Annihilation by the positive simple-root generators #

source

theorem TauCeti.SpinPolarizationData.typeBSpinLieRep_simpleRootGenerator_exteriorBasis_eq_zero_of_mem {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 + 1)) K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) [Invertible 2] {i : Fin (n + 1)} {s : Finset (Fin (n + 1))} (hi : i ∈ s) :

((P.typeBSpinLieRep b z hz) (typeBSimpleRootGenerator i)) (b.ExteriorAlgebra s) = 0

A positive simple type-B generator annihilates every exterior-basis vector whose index set contains the generator's own coordinate. The terminal generator creates a coordinate that is already present, and a nonterminal one creates the coordinate it did not contract; the all-coordinate vector is the case s = Finset.univ.

source

theorem TauCeti.SpinPolarizationData.typeBSpinLieRep_lieSpan_range_simpleRootGenerator_le_lieAnnihilator {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 + 1)) K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) [Invertible 2] {v : ExteriorAlgebra K ↥P.W} (hv : ∀ (i : Fin (n + 1)), ((P.typeBSpinLieRep b z hz) (typeBSimpleRootGenerator i)) v = 0) :

LieSubalgebra.lieSpan K (↥(LieAlgebra.Orthogonal.typeB (Fin (n + 1)) K)) (Set.range typeBSimpleRootGenerator) ≤ lieAnnihilator K (↥(LieAlgebra.Orthogonal.typeB (Fin (n + 1)) K)) v

A vector annihilated by every positive simple-root generator is annihilated by the Lie subalgebra they generate. Annihilation is closed under brackets, so generatorwise vanishing already gives vanishing on the whole Lie span.

source

theorem TauCeti.SpinPolarizationData.typeBSpinLieRep_lieSpan_range_simpleRootGenerator_le_lieAnnihilator_exteriorBasis_univ {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 + 1)) K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) [Invertible 2] :

LieSubalgebra.lieSpan K (↥(LieAlgebra.Orthogonal.typeB (Fin (n + 1)) K)) (Set.range typeBSimpleRootGenerator) ≤ lieAnnihilator K (↥(LieAlgebra.Orthogonal.typeB (Fin (n + 1)) K)) (b.ExteriorAlgebra Finset.univ)

The Lie subalgebra generated by the positive simple-root generators annihilates the all-coordinate exterior-basis vector. Every coordinate is occupied, so every generator annihilates it.