The type-D spin and half-spin Lie representations

An even polarization identifies the split type-D matrix Lie algebra with the quadratic elements of its Clifford algebra. Composing this equivalence with the Fock action gives the spin representation on the full exterior algebra.

Quadratic Clifford elements are even, so they preserve exterior parity. The same matrix Lie algebra therefore acts separately on the even and odd exterior summands, giving the two half-spin Lie representations. Their application formulas below compare both restricted actions directly with the full spin action after coercion to the exterior algebra.

Main definitions and results

• TauCeti.SpinPolarizationData.typeDSpinLieRep: the spin representation of the split type-D matrix Lie algebra.
• TauCeti.SpinPolarizationData.typeDSpinPlusLieRep and TauCeti.SpinPolarizationData.typeDSpinMinusLieRep: its restrictions to the two exterior parity summands.
• TauCeti.SpinPolarizationData.coe_typeDSpinPlusLieRep_apply and TauCeti.SpinPolarizationData.coe_typeDSpinMinusLieRep_apply: the restricted actions agree with the full action after coercion.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II.
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Section 20.2.

The full spin representation

noncomputable def TauCeti.SpinPolarizationData.typeDSpinLieRep {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) [Invertible 2] (hline : P.line = ⊥) : ↥(LieAlgebra.Orthogonal.typeD ι K) →ₗ⁅K⁆ Module.End K (ExteriorAlgebra K ↥P.W)

The split type-D matrix Lie algebra acting on the exterior spinor module through its quadratic Clifford realization.

Equations

• P.typeDSpinLieRep b hline = (TauCeti.spinAction Q P).toLieHom.comp ((CliffordAlgebra.quadraticLieSubalgebra Q).incl.comp (P.typeDQuadraticEquiv b hline).toLieHom)

@[simp]

theorem TauCeti.SpinPolarizationData.typeDSpinLieRep_apply {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) [Invertible 2] (hline : P.line = ⊥) (x : ↥(LieAlgebra.Orthogonal.typeD ι K)) : (P.typeDSpinLieRep b hline) x = (spinAction Q P) ↑((P.typeDQuadraticEquiv b hline) x)

A split type-D matrix acts through its corresponding quadratic Clifford element.

The half-spin representations

noncomputable def TauCeti.SpinPolarizationData.typeDSpinPlusLieRep {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) [Invertible 2] (hline : P.line = ⊥) : ↥(LieAlgebra.Orthogonal.typeD ι K) →ₗ⁅K⁆ Module.End K ↥(spinPlus Q P)

The split type-D matrix Lie algebra acting on the even half-spin summand.

Equations

• P.typeDSpinPlusLieRep b hline = (TauCeti.spinPlusAction Q P hline).toLieHom.comp (TauCeti.SpinPolarizationData.typeDToEvenLieHom✝ P b hline)

@[simp]

theorem TauCeti.SpinPolarizationData.coe_typeDSpinPlusLieRep_apply {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) [Invertible 2] (hline : P.line = ⊥) (x : ↥(LieAlgebra.Orthogonal.typeD ι K)) (s : ↥(spinPlus Q P)) : ↑(((P.typeDSpinPlusLieRep b hline) x) s) = ((P.typeDSpinLieRep b hline) x) ↑s

After coercion to the exterior algebra, the even half-spin action agrees with the full spin action.

noncomputable def TauCeti.SpinPolarizationData.typeDSpinMinusLieRep {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) [Invertible 2] (hline : P.line = ⊥) : ↥(LieAlgebra.Orthogonal.typeD ι K) →ₗ⁅K⁆ Module.End K ↥(spinMinus Q P)

The split type-D matrix Lie algebra acting on the odd half-spin summand.

Equations

• P.typeDSpinMinusLieRep b hline = (TauCeti.spinMinusAction Q P hline).toLieHom.comp (TauCeti.SpinPolarizationData.typeDToEvenLieHom✝ P b hline)

@[simp]

theorem TauCeti.SpinPolarizationData.coe_typeDSpinMinusLieRep_apply {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K ↥P.W) [Invertible 2] (hline : P.line = ⊥) (x : ↥(LieAlgebra.Orthogonal.typeD ι K)) (s : ↥(spinMinus Q P)) : ↑(((P.typeDSpinMinusLieRep b hline) x) s) = ((P.typeDSpinLieRep b hline) x) ↑s

After coercion to the exterior algebra, the odd half-spin action agrees with the full spin action.