The type-B spin representation of an odd polarization

TauCeti.SpinPolarizationData.typeBQuadraticEquiv identifies the split type-B matrix Lie algebra LieAlgebra.Orthogonal.typeB ι K with the quadratic elements of the Clifford algebra of an odd polarization, and those act on the spinor module ExteriorAlgebra K P.W through TauCeti.SpinPolarizationData.spinAction. Composing the two gives the spin representation of the type-B matrix algebra, which this file assembles and extends to the universal enveloping algebra.

The numbered root and coroot generators are read through their Clifford realizations in TauCeti/RepresentationTheory/Spin/Polarization/TypeB/RootGenerators.lean; this file also records the field-generic terminal-root actions on the exterior basis. The integrality of that action is the subject of TauCeti/RepresentationTheory/Spin/Polarization/TypeB/KostantLattice.lean. Nothing here is specific to ℚ: any field in which 2 is invertible carries the same representation.

The enveloping-algebra extension is what the Chevalley--Demazure construction consumes, since divided powers of root vectors and binomial coefficients in coroots live in the enveloping algebra and not in the Lie algebra. This is a prerequisite of the full-weight simply connected type-B carrier in Layer 9, "The Chevalley--Demazure construction", of TauCetiRoadmap/ReductiveGroups/README.md, whose consumer is milestone L0 of TauCetiRoadmap/CFSGStatement/README.md.

Main declarations

• TauCeti.SpinPolarizationData.typeBSpinLieRep: the spin representation of the split type-B matrix Lie algebra.
• TauCeti.SpinPolarizationData.typeBSpinLieRep_apply: its value on a matrix.
• TauCeti.SpinPolarizationData.typeBSpinRep: its extension to the universal enveloping algebra.
• TauCeti.SpinPolarizationData.typeBSpinRep_ι: the extension evaluated on a Lie generator.
• typeBSpinRep_simpleRootGenerator_last_exteriorBasis_empty and typeBSpinRep_simpleNegativeRootGenerator_last_exteriorBasis_singleton: the terminal root actions on the exterior vacuum and final singleton.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §17.

noncomputable def TauCeti.SpinPolarizationData.typeBSpinLieRep {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) [Invertible 2] : ↥(LieAlgebra.Orthogonal.typeB ι K) →ₗ⁅K⁆ Module.End K (ExteriorAlgebra K ↥P.W)

The type-B matrix Lie algebra acting on the spinor module through the quadratic Clifford realization associated to an odd polarization.

Equations

• P.typeBSpinLieRep b z hz = (TauCeti.spinAction Q P).toLieHom.comp ((CliffordAlgebra.quadraticLieSubalgebra Q).incl.comp (P.typeBQuadraticEquiv b z hz).toLieHom)

@[simp]

theorem TauCeti.SpinPolarizationData.typeBSpinLieRep_apply {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) [Invertible 2] (x : ↥(LieAlgebra.Orthogonal.typeB ι K)) : (P.typeBSpinLieRep b z hz) x = (spinAction Q P) ↑((P.typeBQuadraticEquiv b z hz) x)

The spin representation sends a type-B matrix to the spin action of its quadratic Clifford realization.

noncomputable def TauCeti.SpinPolarizationData.typeBSpinRep {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) [Invertible 2] : UniversalEnvelopingAlgebra K ↥(LieAlgebra.Orthogonal.typeB ι K) →ₐ[K] Module.End K (ExteriorAlgebra K ↥P.W)

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

Equations

• P.typeBSpinRep b z hz = (UniversalEnvelopingAlgebra.lift K) (P.typeBSpinLieRep b z hz)

@[simp]

theorem TauCeti.SpinPolarizationData.typeBSpinRep_ι {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) [Invertible 2] (x : ↥(LieAlgebra.Orthogonal.typeB ι K)) : (P.typeBSpinRep b z hz) ((UniversalEnvelopingAlgebra.mkAlgHom K ↥(LieAlgebra.Orthogonal.typeB ι K)) ((TensorAlgebra.ι K) x)) = (spinAction Q P) ↑((P.typeBQuadraticEquiv b z hz) x)

A Lie generator acts in the enveloping-algebra representation through its quadratic Clifford element.

theorem TauCeti.SpinPolarizationData.typeBSpinRep_shortRootGenerator_apply {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [Invertible 2] {n : ℕ} (b : Module.Basis (Fin (n + 1)) K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) (i : Fin (n + 1)) (x : ExteriorAlgebra K ↥P.W) : ((P.typeBSpinRep b z hz) ((UniversalEnvelopingAlgebra.ι K) (typeBShortRootGenerator i))) x = (ExteriorAlgebra.ι K) (b i) * P.lineCoordinate z • CliffordAlgebra.involute x

A positive short-root operator creates its exterior coordinate after the grade involution, scaled by the line coordinate of the distinguished remainder vector.

theorem TauCeti.SpinPolarizationData.typeBSpinRep_shortNegativeRootGenerator_apply {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [Invertible 2] {n : ℕ} (b : Module.Basis (Fin (n + 1)) K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) (i : Fin (n + 1)) (x : ExteriorAlgebra K ↥P.W) : ((P.typeBSpinRep b z hz) ((UniversalEnvelopingAlgebra.ι K) (typeBShortNegativeRootGenerator i))) x = P.lineCoordinate z • CliffordAlgebra.involute ((CliffordAlgebra.contractLeft (b.coord i)) x)

A negative short-root operator contracts its exterior coordinate and applies the grade involution, scaled by the line coordinate of the distinguished remainder vector.

theorem TauCeti.SpinPolarizationData.typeBSpinRep_simpleRootGenerator_last_exteriorBasis_empty {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [Invertible 2] {n : ℕ} (b : Module.Basis (Fin (n + 1)) K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) (hcoord : P.lineCoordinate z = 1) : ((P.typeBSpinRep b z hz) ((UniversalEnvelopingAlgebra.ι K) (typeBSimpleRootGeneratorFamily (Sum.inl (Fin.last n))))) (b.ExteriorAlgebra ∅) = b.ExteriorAlgebra {Fin.last n}

The terminal positive short-root operator creates the final exterior coordinate from the vacuum when the distinguished remainder vector has coordinate one.

theorem TauCeti.SpinPolarizationData.typeBSpinRep_simpleNegativeRootGenerator_last_exteriorBasis_singleton {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [Invertible 2] {n : ℕ} (b : Module.Basis (Fin (n + 1)) K ↥P.W) (z : ↥P.line) (hz : Q ↑z = 1) (hcoord : P.lineCoordinate z = 1) : ((P.typeBSpinRep b z hz) ((UniversalEnvelopingAlgebra.ι K) (typeBSimpleRootGeneratorFamily (Sum.inr (Fin.last n))))) (b.ExteriorAlgebra {Fin.last n}) = b.ExteriorAlgebra ∅

The terminal negative short-root operator annihilates the final exterior coordinate to the vacuum when the distinguished remainder vector has coordinate one.