The type-D spinor lattice is Kostant-stable

This file turns the type-Dₙ Clifford Serre system into a rational representation of the type-D Serre presentation and proves that its coordinate spinor lattice is stable under the Serre Kostant form.

The positive and negative simple-root representatives act by square-zero endomorphisms and preserve the exterior coordinate lattice. The simple-coroot representatives act diagonally on the exterior basis with the integral weights TauCeti.DynkinType.typeDSpinWeight; consequently all of their binomial coefficients preserve the same lattice. These two facts give stability under every generator of the Serre Kostant form.

The full exterior algebra, rather than either parity summand alone, is used because its weights span the full simply connected type-D character lattice. Thus this is the admissible-lattice input for the full-weight type-D Chevalley--Demazure carrier in Layer 9 of the ReductiveGroups roadmap. That carrier is consumed by the Dₙ(q) and ²Dₙ(q) branches of milestone L0 in the CFSGStatement roadmap.

Main declarations

• TauCeti.SpinPolarizationData.typeDSpinSerreRepresentation: the type-D Serre presentation acting on the spinor module.
• TauCeti.SpinPolarizationData.typeDSpinRep: its extension to the universal enveloping algebra.
• TauCeti.SpinPolarizationData.typeDSpinRep_rootGenerator_sq: the represented root operators are square-zero.
• TauCeti.SpinPolarizationData.typeDSpinRep_rootGenerator_mem_evenOdd: they preserve exterior parity, hence each half-spin summand.
• TauCeti.SpinPolarizationData.isCartanWeightVector_typeDSpinRep_integralLatticeBasis: the integral exterior basis is a weight basis with weights typeDSpinWeight.
• TauCeti.SpinPolarizationData.typeDSpinRep_serreKostantForm_apply_mem_integralLattice: the Serre 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, §§26--27.
• N. Bourbaki, Groupes et algèbres de Lie, Chapters 4--6, Plate IV.

The organization parallels the type-B spinor-lattice construction in Tau Ceti PR #5269; the fork coroot and the need for both half-spin parities are the type-D features.

The rational spin representation

noncomputable def TauCeti.SpinPolarizationData.typeDSpinSerreRepresentation {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) : Matrix.ToLieAlgebra ℚ (CartanMatrix.D n) →ₗ⁅ℚ⁆ Module.End ℚ (ExteriorAlgebra ℚ ↥P.W)

The rational type-D Serre presentation acting on the spinor module through its canonical Clifford Serre system.

Equations

• P.typeDSpinSerreRepresentation b hn = (TauCeti.spinAction Q P).toLieHom.comp (TauCeti.serreLift ⋯)

@[simp]

theorem TauCeti.SpinPolarizationData.typeDSpinSerreRepresentation_serreH {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) (i : Fin n) : (P.typeDSpinSerreRepresentation b hn) (serreH ℚ (CartanMatrix.D n) i) = (spinAction Q P) (P.typeDSimpleCorootBivector b ⋯ i)

A Cartan generator acts through the corresponding type-D simple-coroot Clifford element.

@[simp]

theorem TauCeti.SpinPolarizationData.typeDSpinSerreRepresentation_serreE {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) (i : Fin n) : (P.typeDSpinSerreRepresentation b hn) (serreE ℚ (CartanMatrix.D n) i) = (spinAction Q P) (P.typeDSimpleRootBivector b ⋯ i)

A positive Serre generator acts through the corresponding type-D root Clifford element.

@[simp]

theorem TauCeti.SpinPolarizationData.typeDSpinSerreRepresentation_serreF {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) (i : Fin n) : (P.typeDSpinSerreRepresentation b hn) (serreF ℚ (CartanMatrix.D n) i) = (spinAction Q P) (P.typeDSimpleNegativeRootBivector b ⋯ i)

A negative Serre generator acts through the corresponding negative-root Clifford element.

noncomputable def TauCeti.SpinPolarizationData.typeDSpinRep {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) : UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ (CartanMatrix.D n)) →ₐ[ℚ] Module.End ℚ (ExteriorAlgebra ℚ ↥P.W)

The type-D spin representation extended to the universal enveloping algebra.

Equations

• P.typeDSpinRep b hn = (UniversalEnvelopingAlgebra.lift ℚ) (P.typeDSpinSerreRepresentation b hn)

theorem TauCeti.SpinPolarizationData.typeDSpinRep_ι {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) (x : Matrix.ToLieAlgebra ℚ (CartanMatrix.D n)) : (P.typeDSpinRep b hn) ((UniversalEnvelopingAlgebra.ι ℚ) x) = (P.typeDSpinSerreRepresentation b hn) x

An included Lie element acts through the rational Serre representation.

Root operators

theorem TauCeti.SpinPolarizationData.typeDSpinRep_rootGenerator_sq {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) (k : Fin n ⊕ Fin n) : (P.typeDSpinRep b hn) ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator (CartanMatrix.D n) k)) ^ 2 = 0

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

theorem TauCeti.SpinPolarizationData.isNilpotent_typeDSpinRep_rootGenerator {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) (k : Fin n ⊕ Fin n) : IsNilpotent ((P.typeDSpinRep b hn) ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator (CartanMatrix.D n) k)))

Every represented positive or negative simple-root generator acts nilpotently.

theorem TauCeti.SpinPolarizationData.typeDSpinRep_serreE_eq_spinAction {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) (i : Fin n) : (P.typeDSpinRep b hn) ((UniversalEnvelopingAlgebra.ι ℚ) (serreE ℚ (CartanMatrix.D n) i)) = (spinAction Q P) (P.typeDSimpleRootBivector b ⋯ i)

The represented positive Serre generator acts through its simple-root Clifford bivector.

theorem TauCeti.SpinPolarizationData.typeDSpinRep_serreF_eq_spinAction {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) (i : Fin n) : (P.typeDSpinRep b hn) ((UniversalEnvelopingAlgebra.ι ℚ) (serreF ℚ (CartanMatrix.D n) i)) = (spinAction Q P) (P.typeDSimpleNegativeRootBivector b ⋯ i)

The represented negative Serre generator acts through its negative simple-root Clifford bivector.

theorem TauCeti.SpinPolarizationData.typeDSpinRep_rootGenerator_mem_evenOdd {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) (hline : P.line = ⊥) (k : Fin n ⊕ Fin n) {j : ZMod 2} {s : ExteriorAlgebra ℚ ↥P.W} (hs : s ∈ CliffordAlgebra.evenOdd 0 j) : ((P.typeDSpinRep b hn) ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator (CartanMatrix.D n) k))) s ∈ CliffordAlgebra.evenOdd 0 j

The represented root generators preserve exterior parity, for a polarization without a line summand. Each acts through a simple-root Clifford bivector, which is even, so it maps each half-spin summand into itself.

theorem TauCeti.SpinPolarizationData.typeDSpinRep_serreE_exteriorBasis_singleton {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) {i : Fin n} (hnext : ↑i + 1 < n) : ((P.typeDSpinRep b hn) ((UniversalEnvelopingAlgebra.ι ℚ) (serreE ℚ (CartanMatrix.D n) i))) (b.ExteriorAlgebra {⟨↑i + 1, hnext⟩}) = b.ExteriorAlgebra {i}

At a chain node, the positive type-D root generator moves the singleton exterior-basis vector at i + 1 to the singleton at i.

theorem TauCeti.SpinPolarizationData.typeDSpinRep_serreF_exteriorBasis_singleton {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) {i : Fin n} (hnext : ↑i + 1 < n) : ((P.typeDSpinRep b hn) ((UniversalEnvelopingAlgebra.ι ℚ) (serreF ℚ (CartanMatrix.D n) i))) (b.ExteriorAlgebra {i}) = b.ExteriorAlgebra {⟨↑i + 1, hnext⟩}

At a chain node, the negative type-D root generator moves the singleton exterior-basis vector at i to the singleton at i + 1.

theorem TauCeti.SpinPolarizationData.typeDSpinRep_serreE_exteriorBasis_empty {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) {i : Fin n} (hlast : ¬↑i + 1 < n) : ((P.typeDSpinRep b hn) ((UniversalEnvelopingAlgebra.ι ℚ) (serreE ℚ (CartanMatrix.D n) i))) (b.ExteriorAlgebra ∅) = ExteriorAlgebra.basisEraseSign ⟨n - 2, ⋯⟩ {⟨n - 2, ⋯⟩, ⟨n - 1, ⋯⟩} • b.ExteriorAlgebra {⟨n - 2, ⋯⟩, ⟨n - 1, ⋯⟩}

At the fork node, the positive type-D root generator creates the last two coordinates from the exterior vacuum.

theorem TauCeti.SpinPolarizationData.typeDSpinRep_serreF_exteriorBasis_pair {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) {i : Fin n} (hlast : ¬↑i + 1 < n) : ((P.typeDSpinRep b hn) ((UniversalEnvelopingAlgebra.ι ℚ) (serreF ℚ (CartanMatrix.D n) i))) (b.ExteriorAlgebra {⟨n - 2, ⋯⟩, ⟨n - 1, ⋯⟩}) = (ExteriorAlgebra.basisEraseSign ⟨n - 2, ⋯⟩ {⟨n - 2, ⋯⟩, ⟨n - 1, ⋯⟩} * ExteriorAlgebra.basisEraseSign ⟨n - 1, ⋯⟩ {⟨n - 1, ⋯⟩}) • b.ExteriorAlgebra ∅

At the fork node, the negative type-D root generator annihilates the last two coordinates to the exterior vacuum.

theorem TauCeti.SpinPolarizationData.typeDSpinRep_rootGenerator_apply_mem_integralLattice {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) (k : Fin n ⊕ Fin n) {v : ExteriorAlgebra ℚ ↥P.W} (hv : v ∈ ExteriorAlgebra.integralLattice b) : ((P.typeDSpinRep b hn) ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator (CartanMatrix.D n) k))) v ∈ ExteriorAlgebra.integralLattice b

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

Cartan weights and binomial operators

theorem TauCeti.SpinPolarizationData.isCartanWeightVector_typeDSpinRep_exteriorBasis {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) (s : Finset (Fin n)) : UniversalEnvelopingAlgebra.IsCartanWeightVector (serreH ℚ (CartanMatrix.D n)) (P.typeDSpinRep b hn) (DynkinType.typeDSpinWeight s) (b.ExteriorAlgebra s)

Every exterior-basis vector is a Cartan weight vector for the type-D spin representation, with its integral simply connected spin weight.

theorem TauCeti.SpinPolarizationData.isCartanWeightVector_typeDSpinRep_integralLatticeBasis {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) (s : Finset (Fin n)) : UniversalEnvelopingAlgebra.IsCartanWeightVector (serreH ℚ (CartanMatrix.D n)) (P.typeDSpinRep b hn) (DynkinType.typeDSpinWeight s) ↑((ExteriorAlgebra.integralLatticeBasis b) s)

The integral exterior basis is a Cartan weight basis for the type-D spin representation.

theorem TauCeti.SpinPolarizationData.typeDSpinRep_ringChoose_serreH_apply_mem_integralLattice {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) (i : Fin n) (m : ℕ) {v : ExteriorAlgebra ℚ ↥P.W} (hv : v ∈ ExteriorAlgebra.integralLattice b) : ((P.typeDSpinRep b hn) (Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (serreH ℚ (CartanMatrix.D n) i)) m)) v ∈ ExteriorAlgebra.integralLattice b

Every binomial coefficient in a represented simple-coroot generator preserves the coordinate spinor lattice.

Stability under the Serre Kostant form

theorem TauCeti.SpinPolarizationData.typeDSpinRep_serreKostantForm_apply_mem_integralLattice {V : Type u} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (P : SpinPolarizationData Q) {n : ℕ} (b : Module.Basis (Fin n) ℚ ↥P.W) (hn : 4 ≤ n) {u : UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ (CartanMatrix.D n))} (hu : u ∈ serreKostantForm (CartanMatrix.D n)) {v : ExteriorAlgebra ℚ ↥P.W} (hv : v ∈ ExteriorAlgebra.integralLattice b) : ((P.typeDSpinRep b hn) u) v ∈ ExteriorAlgebra.integralLattice b

The coordinate spinor lattice is admissible for the type-D Serre Kostant form.