The Spin-group representation on the exterior model

This file restricts the Fock action of a Clifford algebra to its Spin group and to its even subalgebra, and proves, when the first isotropic summand is finite free, that the underlying Clifford action generates every endomorphism of the exterior model.

The Spin group lies inside the even subalgebra (spinGroup.mem_even), so the Spin representation factors through the even Clifford action TauCeti.evenSpinAction along the inclusion TauCeti.spinGroupToEven. How much of the endomorphism algebra that restricted action reaches is exactly what distinguishes the two parities of the ambient dimension: in positive even dimension it splits off the two half-spin blocks, while in odd dimension it is still everything. Dimension zero is the degenerate exception to the even description, W being ⊥ there, so that S = K is one-dimensional, the odd block is zero and the even action is again onto.

Main definitions and results

• TauCeti.spinRep and TauCeti.pinRep are the representations of spinGroup Q and pinGroup Q on the exterior model.
• TauCeti.spinGroupToEven is the inclusion of the Spin group into the even Clifford subalgebra and TauCeti.evenSpinAction is the Fock action restricted to that subalgebra, through which the Spin representation factors by TauCeti.evenSpinAction_apply and TauCeti.coe_spinGroupToEven_apply.
• TauCeti.spinAction_surjective identifies the Fock action as onto the full endomorphism algebra when the first isotropic summand is finite free.

References

• Spin representations roadmap

noncomputable def TauCeti.spinRep {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (P : SpinPolarizationData Q) : Representation K (↥(spinGroup Q)) (ExteriorAlgebra K ↥P.W)

The representation of the Spin group obtained by restricting its Clifford-algebra action on the exterior algebra of the first isotropic summand.

Equations

• TauCeti.spinRep Q P = (↑(TauCeti.spinAction Q P).toRingHom).comp ((Units.coeHom (CliffordAlgebra Q)).comp spinGroup.toUnits)

@[simp]

theorem TauCeti.spinRep_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (P : SpinPolarizationData Q) (g : ↥(spinGroup Q)) : (spinRep Q P) g = (spinAction Q P) ↑g

A Spin-group element acts through its underlying Clifford-algebra element.

noncomputable def TauCeti.pinRep {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (P : SpinPolarizationData Q) : Representation K (↥(pinGroup Q)) (ExteriorAlgebra K ↥P.W)

The representation of the Pin group obtained by restricting its Clifford-algebra action on the exterior algebra of the first isotropic summand.

Equations

• TauCeti.pinRep Q P = (↑(TauCeti.spinAction Q P).toRingHom).comp ((Units.coeHom (CliffordAlgebra Q)).comp pinGroup.toUnits)

@[simp]

theorem TauCeti.pinRep_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (P : SpinPolarizationData Q) (g : ↥(pinGroup Q)) : (pinRep Q P) g = (spinAction Q P) ↑g

A Pin-group element acts through its underlying Clifford-algebra element.

def TauCeti.spinGroupToEven {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) : ↥(spinGroup Q) →* ↥(CliffordAlgebra.even Q)

The inclusion of the Spin group into the even Clifford subalgebra, the Spin group consisting of even elements by spinGroup.mem_even.

Equations

• TauCeti.spinGroupToEven Q = Submonoid.inclusion ⋯

@[simp]

theorem TauCeti.coe_spinGroupToEven_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (g : ↥(spinGroup Q)) : ↑((spinGroupToEven Q) g) = ↑g

A Spin-group element sits in the even subalgebra as itself.

noncomputable def TauCeti.evenSpinAction {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (P : SpinPolarizationData Q) : ↥(CliffordAlgebra.even Q) →ₐ[K] Module.End K (ExteriorAlgebra K ↥P.W)

The action of the even Clifford subalgebra on the spinor module S = ⋀·W, the Fock action restricted along the inclusion of CliffordAlgebra.even Q.

This is the algebra through which the Spin representation acts, spinGroup Q being contained in the even subalgebra; the half-spin actions of TauCeti.spinPlusAction and TauCeti.spinMinusAction are its two blocks in even dimension.

Equations

• TauCeti.evenSpinAction Q P = (TauCeti.spinAction Q P).comp (CliffordAlgebra.even Q).val

@[simp]

theorem TauCeti.evenSpinAction_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (P : SpinPolarizationData Q) (x : ↥(CliffordAlgebra.even Q)) : (evenSpinAction Q P) x = (spinAction Q P) ↑x

An even Clifford element acts on the spinor module by the Fock action.

theorem TauCeti.spinAction_surjective {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [Module.Free K ↥P.W] [Module.Finite K ↥P.W] : Function.Surjective ⇑(spinAction Q P)

When the first isotropic summand is finite free, the Fock action of a Clifford algebra on its exterior model is onto the full endomorphism algebra.