The coroot weights of the type-B spin module, and stability of its spinor lattice

This file proves that, over ℚ, the coordinate spinor lattice of the type-B spin representation TauCeti.SpinPolarizationData.typeBSpinRep of an odd polarization is stable under the simple-generator Kostant integral form: the subring TauCeti.UniversalEnvelopingAlgebra.kostantForm generated by the divided powers of the Bourbaki-numbered simple-root family TauCeti.typeBSimpleRootGeneratorFamily, in both signs, and the binomial coefficients in the simple coroots. As in TauCeti/LinearAlgebra/RootSystem/SimplyConnectedRootDatum/KostantForm.lean, identifying that subring with the canonical all-root Kostant ℤ-form is a separate theorem and is not claimed here.

The positive and negative simple-root vectors act through square-zero Clifford bivectors, so their divided powers preserve the lattice. The simple coroots act diagonally on the exterior basis with integral eigenvalues: adjacent differences of half-integral spin weights away from the terminal node, and twice the terminal half-weight at the short node. Their binomial coefficients therefore preserve the same lattice. These are precisely the two generator inputs consumed by kostantForm_apply_mem, so the whole subring they generate preserves the lattice.

Those same eigenvalues are what the file records about weights. Over ℚ the exterior basis is a Cartan weight basis for the numbered simple coroots, with the integral weight read off which coordinates occur; that weight agrees with the simply connected type-B spin weight TauCeti.DynkinType.typeBSpinWeight of the same index set. The all-coordinate vector carries the last fundamental weight ωₗ, and reading the coroot weights from the terminal node downwards shows that it is the only exterior-basis vector that does.

The nilpotence and eigenvalue computations are stated over an arbitrary field in which 2 is invertible, which is all the underlying Clifford comparison needs; only the lattice statements are specific to ℚ, where the coordinate lattice lives.

This is a step towards the admissible lattice for the full-weight simply connected type-B Chevalley carrier in Layer 9 of the ReductiveGroups roadmap. That carrier is consumed by the B_n(q) branch of milestone L0 in the CFSGStatement roadmap.

Main declarations

• TauCeti.SpinPolarizationData.typeBSpinRep_simpleRootGenerator_sq: the represented simple-root operators are square-zero.
• TauCeti.SpinPolarizationData.typeBSpinCorootWeight, with its values TauCeti.SpinPolarizationData.typeBSpinCorootWeight_last, TauCeti.SpinPolarizationData.typeBSpinCorootWeight_castSucc, TauCeti.SpinPolarizationData.typeBSpinCorootWeight_univ_eq_single and TauCeti.SpinPolarizationData.spinAction_typeBQuadraticEquiv_typeBSimpleCorootGenerator_basis: the integral eigenvalues of the numbered simple coroots on the exterior basis.
• TauCeti.SpinPolarizationData.typeBSpinCorootWeight_eq_typeBSpinWeight: those eigenvalues are the simply connected type-B spin weight of the same index set.
• TauCeti.SpinPolarizationData.typeBSpinCorootWeight_eq_single_iff: the last fundamental weight occurs at exactly one exterior-basis vector.
• TauCeti.SpinPolarizationData.isCartanWeightVector_typeBSpinRep_exteriorBasis: over ℚ, the exterior basis is a Cartan weight basis with those eigenvalues.
• TauCeti.SpinPolarizationData.typeBSpinRep_kostantForm_apply_mem_integralLattice: the simple-generator type-B Kostant form preserves the coordinate spinor lattice.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§25--27.
• N. Bourbaki, Groupes et algèbres de Lie, Chapters 4--6, Planche II.

Root operators

theorem TauCeti.SpinPolarizationData.typeBSpinRep_simpleRootGenerator_sq {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] (k : Fin (n + 1) ⊕ Fin (n + 1)) : (P.typeBSpinRep b z hz) ((UniversalEnvelopingAlgebra.ι K) (typeBSimpleRootGeneratorFamily k)) ^ 2 = 0

Every represented positive or negative simple-root vector is square-zero.

theorem TauCeti.SpinPolarizationData.typeBSpinRep_differenceRootGenerator_apply {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 j : Fin (n + 1)) (hij : i ≠ j) (x : ExteriorAlgebra K ↥P.W) : ((P.typeBSpinRep b z hz) ((UniversalEnvelopingAlgebra.ι K) (typeBDifferenceRootGenerator i j hij))) x = (ExteriorAlgebra.ι K) (b i) * (CliffordAlgebra.contractLeft (b.coord j)) x

The difference-root operator indexed by distinct coordinates i and j contracts the j-th exterior coordinate and then creates the i-th one.

theorem TauCeti.SpinPolarizationData.typeBSpinRep_simpleRootGenerator_castSucc_exteriorBasis_singleton {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] (j : Fin n) : ((P.typeBSpinRep b z hz) ((UniversalEnvelopingAlgebra.ι K) (typeBSimpleRootGeneratorFamily (Sum.inl j.castSucc)))) (b.ExteriorAlgebra {j.succ}) = b.ExteriorAlgebra {j.castSucc}

A nonterminal positive simple-root operator moves the next exterior singleton one coordinate to the left.

theorem TauCeti.SpinPolarizationData.typeBSpinRep_simpleNegativeRootGenerator_castSucc_exteriorBasis_singleton {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] (j : Fin n) : ((P.typeBSpinRep b z hz) ((UniversalEnvelopingAlgebra.ι K) (typeBSimpleRootGeneratorFamily (Sum.inr j.castSucc)))) (b.ExteriorAlgebra {j.castSucc}) = b.ExteriorAlgebra {j.succ}

A nonterminal negative simple-root operator moves an exterior singleton one coordinate to the right.

The weights of the simple coroots

def TauCeti.SpinPolarizationData.typeBSpinCorootWeight {n : ℕ} (s : Finset (Fin (n + 1))) (i : Fin (n + 1)) : ℤ

The integral eigenvalue of a numbered simple coroot on an exterior-basis vector.

Equations

• TauCeti.SpinPolarizationData.typeBSpinCorootWeight s i = Fin.lastCases (if Fin.last n ∈ s then 1 else -1) (fun (j : Fin n) => (if j.castSucc ∈ s then 1 else 0) - if j.succ ∈ s then 1 else 0) i

@[simp]

theorem TauCeti.SpinPolarizationData.typeBSpinCorootWeight_last {n : ℕ} (s : Finset (Fin (n + 1))) : typeBSpinCorootWeight s (Fin.last n) = if Fin.last n ∈ s then 1 else -1

At the terminal short node the coroot weight is 1 or -1 according to whether that node is occupied.

@[simp]

theorem TauCeti.SpinPolarizationData.typeBSpinCorootWeight_castSucc {n : ℕ} (s : Finset (Fin (n + 1))) (j : Fin n) : typeBSpinCorootWeight s j.castSucc = (if j.castSucc ∈ s then 1 else 0) - if j.succ ∈ s then 1 else 0

Away from the terminal node the coroot weight is the adjacent difference of occupation numbers.

theorem TauCeti.SpinPolarizationData.typeBSpinCorootWeight_eq_typeBSpinWeight {n : ℕ} (s : Finset (Fin (n + 1))) : typeBSpinCorootWeight s = DynkinType.typeBSpinWeight s

The representation-theoretic coroot weight is the simply connected type-B spin weight.

@[simp]

theorem TauCeti.SpinPolarizationData.typeBSpinCorootWeight_univ_eq_single {n : ℕ} : typeBSpinCorootWeight Finset.univ = Pi.single (Fin.last n) 1

The all-coordinate exterior-basis vector carries the last fundamental weight. Every coordinate is occupied, so the terminal short node reads 1 and every adjacent difference vanishes: the weight is the last fundamental weight ωₗ, the 1 sitting at the terminal short node. The generator-level highest-weight data for the corresponding spinor, namely annihilation by the positive simple generators together with this weight, are proved in TauCeti/RepresentationTheory/Spin/Polarization/TypeB/LastFundamentalWeight.lean.

@[simp]

theorem TauCeti.SpinPolarizationData.typeBSpinCorootWeight_eq_single_iff {n : ℕ} {s : Finset (Fin (n + 1))} : typeBSpinCorootWeight s = Pi.single (Fin.last n) 1 ↔ s = Finset.univ

The last fundamental weight occurs at exactly one exterior-basis vector. Reading the coroot weights from the terminal node downwards, the value 1 at the short node forces the last coordinate to be occupied and each vanishing adjacent difference propagates occupation one step to the left, so the only index set with this weight is the full one. In particular the weight ωₗ of the type-B spin module occurs with multiplicity one in its exterior basis.

@[simp]

theorem TauCeti.SpinPolarizationData.spinAction_typeBQuadraticEquiv_typeBSimpleCorootGenerator_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 + 1)) K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) [Invertible 2] (i : Fin (n + 1)) (s : Finset (Fin (n + 1))) : ((spinAction Q P) ↑((P.typeBQuadraticEquiv b z hz) (typeBSimpleCorootGenerator i))) (b.ExteriorAlgebra s) = ↑(typeBSpinCorootWeight s i) • b.ExteriorAlgebra s

A numbered simple coroot acts diagonally on the exterior basis, with integral eigenvalue typeBSpinCorootWeight.

Cartan weight vectors

theorem TauCeti.SpinPolarizationData.isCartanWeightVector_typeBSpinRep_exteriorBasis {V : Type v} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℚ ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) (s : Finset (Fin (n + 1))) : UniversalEnvelopingAlgebra.IsCartanWeightVector typeBSimpleCorootGenerator (P.typeBSpinRep b z hz) (typeBSpinCorootWeight s) (b.ExteriorAlgebra s)

The exterior basis is a Cartan weight basis of the type-B spin module: the numbered simple coroots act on the basis vector indexed by s through the integral weight TauCeti.SpinPolarizationData.typeBSpinCorootWeight s.

Stability of the coordinate spinor lattice

theorem TauCeti.SpinPolarizationData.typeBSpinRep_simpleRootGenerator_apply_mem_integralLattice {V : Type v} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℚ ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) (k : Fin (n + 1) ⊕ Fin (n + 1)) {v : ExteriorAlgebra ℚ ↥P.W} (hv : v ∈ ExteriorAlgebra.integralLattice b) : ((P.typeBSpinRep b z hz) ((UniversalEnvelopingAlgebra.ι ℚ) (typeBSimpleRootGeneratorFamily k))) v ∈ ExteriorAlgebra.integralLattice b

Every represented positive or negative simple-root vector preserves the coordinate spinor lattice.

theorem TauCeti.SpinPolarizationData.typeBSpinRep_ringChoose_coroot_apply_mem_integralLattice {V : Type v} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℚ ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) (i : Fin (n + 1)) (m : ℕ) {v : ExteriorAlgebra ℚ ↥P.W} (hv : v ∈ ExteriorAlgebra.integralLattice b) : ((P.typeBSpinRep b z hz) (Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (typeBSimpleCorootGenerator i)) m)) v ∈ ExteriorAlgebra.integralLattice b

Every binomial coefficient in a represented simple coroot preserves the coordinate spinor lattice: the exterior basis consists of eigenvectors with integral eigenvalues.

theorem TauCeti.SpinPolarizationData.typeBSpinRep_kostantForm_apply_mem_integralLattice {V : Type v} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin (n + 1)) ℚ ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) {u : UniversalEnvelopingAlgebra ℚ ↥(LieAlgebra.Orthogonal.typeB (Fin (n + 1)) ℚ)} (hu : u ∈ UniversalEnvelopingAlgebra.kostantForm typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator) {v : ExteriorAlgebra ℚ ↥P.W} (hv : v ∈ ExteriorAlgebra.integralLattice b) : ((P.typeBSpinRep b z hz) u) v ∈ ExteriorAlgebra.integralLattice b

The coordinate spinor lattice is stable under the simple-generator type-B Kostant form: under the subring generated by the divided powers of the simple-root family typeBSimpleRootGeneratorFamily and the binomial coefficients in typeBSimpleCorootGenerator. No comparison with the all-root Kostant ℤ-form of type B is claimed.