The half-spin summands of the spin representation

TauCeti.spinAction makes the exterior algebra S = ⋀·W of the isotropic summand of a polarization a module over the Clifford algebra, and TauCeti.spinRep restricts that action along the inclusion of spinGroup Q — the spin representation proper — as TauCeti.pinRep does along the inclusion of pinGroup Q.

The exterior algebra is itself ℤ/2-graded, by exterior parity, and S splits as the sum S⁺ ⊕ S⁻ of the even and the odd part. Whether that splitting is a splitting of representations is the substance of this file, and it depends on the polarization.

• A vector of W acts by exterior multiplication and a vector of W' by contraction, and both reverse parity. So when the polarization has no line summand every vector acts by a parity-reversing operator, an even Clifford element acts by a parity-preserving one, and — since the spin group is even — S⁺ and S⁻ are subrepresentations of spinRep.
• A vector z of the line summand acts by P.lineCoordinate z times the grade involution, an operator that preserves parity, so with a line present an even Clifford element need not preserve parity at all. Concretely, take V a three-dimensional complex vector space carrying a nondegenerate quadratic form, polarized in the standard way: W and W' are dual isotropic lines and the line summand is their anisotropic orthogonal complement. Then S = ⋀·W is two-dimensional, spinGroup Q is a copy of SL₂ acting on S by its standard representation, and that representation has no one-dimensional subrepresentation, so the parity splitting is not invariant there. The hypothesis P.line = ⊥ below is therefore not a convenience; the statement is false without it.

The grading statement TauCeti.spinAction_mem_evenOdd is proved once, for an arbitrary parity of the acting Clifford element, and the half-spin invariance and the parity shift by odd elements are both read off it. Its two inputs are that exterior multiplication raises the exterior degree (Mathlib's CliffordAlgebra.evenOdd_mul_le) and that contraction lowers it (CliffordAlgebra.contractLeft_mem_evenOdd); the induction that propagates them from a single vector to a general Clifford element is Mathlib's CliffordAlgebra.evenOdd_induction.

Nothing here needs a field, a nondegeneracy hypothesis, or a finite dimension: like TauCeti.spinAction itself, everything holds over the commutative ring the polarization data lives over. Their dimensions, which need a field and a finite dimension, are counted in TauCeti/RepresentationTheory/Spin/Dimension.lean. Their invariant-subspace dichotomies over a field are proved in TauCeti/RepresentationTheory/Spin/Irreducible.lean; their highest weights belong to the complex theory and are not proved here.

Main definitions

• TauCeti.spinPlus and TauCeti.spinMinus: the even and odd half-spin summands of S.
• TauCeti.spinPlusSubrep and TauCeti.spinMinusSubrep: those summands bundled as subrepresentations of spinRep, for a polarization without a line summand.
• TauCeti.spinPlusAction and TauCeti.spinMinusAction: the actions of the even Clifford subalgebra on the two summands, and TauCeti.evenSpinActionProd their product.

Main results

• TauCeti.spinAction_mem_evenOdd: the Clifford action is graded for a polarization without a line summand, and TauCeti.spinAction_mem_evenOdd_of_mem_even: an even Clifford element preserves exterior parity.
• TauCeti.spinPlus_invariant and TauCeti.spinMinus_invariant: the half-spin summands are invariant under the spin representation.
• TauCeti.isCompl_spinPlus_spinMinus: the two summands are complementary, so S = S⁺ ⊕ S⁻, with TauCeti.spinPlus_sup_spinMinus and TauCeti.spinPlus_inf_spinMinus its two halves, and TauCeti.isCompl_spinPlusSubrep_spinMinusSubrep: the same in the lattice of subrepresentations of spinRep, so the splitting is one of representations.
• TauCeti.nontrivial_spinPlus and TauCeti.nontrivial_spinMinus: neither summand is zero, the odd one as soon as W is nonzero.
• TauCeti.coe_spinPlusAction_spinGroup_apply and TauCeti.coe_spinMinusAction_spinGroup_apply: the two bundlings agree, in that the even-subalgebra actions restrict along the spin group to the subrepresentations of spinRep.
• TauCeti.map_spinAction_spinPlus_le_spinMinus and TauCeti.map_spinAction_spinMinus_le_spinPlus: an odd Clifford element carries each of the two summands into the other, so the invariance argument does not extend from the spin group — which is even — to the pin group, which in general is not. That is why the splitting is stated for spinRep and not for pinRep.

References

• W. Fulton and J. Harris, Representation Theory: A First Course (1991), §20.1–20.2: the spin module S = ⋀·W of a maximal isotropic subspace and its splitting into the half-spin summands S⁺ and S⁻ (§20.1), and the pin and spin groups acting on it (§20.2) — the construction formalised here.
• Spin-representations roadmap, Layer 4, "The spin representation of the group" and "The half-spin summands".

The half-spin summands

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

The even half-spin summand S⁺ = ⋀ᵉᵛᵉⁿ W, the even half of the exterior parity grading of the spinor module.

Equations

• TauCeti.spinPlus Q P = CliffordAlgebra.evenOdd 0 0

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

The odd half-spin summand S⁻ = ⋀ᵒᵈᵈ W, the odd half of the exterior parity grading of the spinor module.

Equations

• TauCeti.spinMinus Q P = CliffordAlgebra.evenOdd 0 1

theorem TauCeti.spinPlus_def {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) : spinPlus Q P = CliffordAlgebra.evenOdd 0 0

theorem TauCeti.spinMinus_def {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) : spinMinus Q P = CliffordAlgebra.evenOdd 0 1

@[simp]

theorem TauCeti.mem_spinPlus {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {s : ExteriorAlgebra K ↥P.W} : s ∈ spinPlus Q P ↔ s ∈ CliffordAlgebra.evenOdd 0 0

A spinor lies in S⁺ exactly when it is of even exterior parity.

@[simp]

theorem TauCeti.mem_spinMinus {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) {s : ExteriorAlgebra K ↥P.W} : s ∈ spinMinus Q P ↔ s ∈ CliffordAlgebra.evenOdd 0 1

A spinor lies in S⁻ exactly when it is of odd exterior parity.

theorem TauCeti.isCompl_spinPlus_spinMinus {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) : IsCompl (spinPlus Q P) (spinMinus Q P)

The spinor module is the sum of its two half-spin summands, S = S⁺ ⊕ S⁻. This is the exterior parity grading, and it holds for every polarization. Invariance of the summands (TauCeti.spinPlus_invariant) does not: it needs a polarization without a line summand.

@[simp]

theorem TauCeti.spinPlus_sup_spinMinus {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) : spinPlus Q P ⊔ spinMinus Q P = ⊤

The two half-spin summands span the spinor module: every spinor is the sum of an even and an odd one.

@[simp]

theorem TauCeti.spinPlus_inf_spinMinus {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) : spinPlus Q P ⊓ spinMinus Q P = ⊥

The two half-spin summands meet only in zero: a spinor of both parities vanishes.

theorem TauCeti.nontrivial_spinPlus {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) [Nontrivial K] : Nontrivial ↥(spinPlus Q P)

The even half-spin summand is never zero: it contains the scalar 1, of exterior degree zero. Unlike TauCeti.nontrivial_spinMinus this needs no hypothesis on the isotropic summand.

theorem TauCeti.nontrivial_spinMinus {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hW : P.W ≠ ⊥) : Nontrivial ↥(spinMinus Q P)

The odd half-spin summand is nonzero as soon as the isotropic summand is. For W = ⊥ the spinor module is the ground ring, entirely even, and this fails.

The Clifford action is graded

The parity of the operator by which a Clifford element acts on S is the parity of the element, provided the polarization has no line summand.

theorem TauCeti.spinAction_mem_evenOdd {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) {i j : ZMod 2} {x : CliffordAlgebra Q} (hx : x ∈ CliffordAlgebra.evenOdd Q i) {s : ExteriorAlgebra K ↥P.W} (hs : s ∈ CliffordAlgebra.evenOdd 0 j) : ((spinAction Q P) x) s ∈ CliffordAlgebra.evenOdd 0 (i + j)

The Clifford action on the spinor module is graded when the polarization has no line summand: a Clifford element of parity i shifts the exterior parity of a spinor by i.

theorem TauCeti.spinAction_mem_evenOdd_of_mem_even {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) {x : CliffordAlgebra Q} (hx : x ∈ CliffordAlgebra.even Q) {j : ZMod 2} {s : ExteriorAlgebra K ↥P.W} (hs : s ∈ CliffordAlgebra.evenOdd 0 j) : ((spinAction Q P) x) s ∈ CliffordAlgebra.evenOdd 0 j

An even Clifford element preserves exterior parity, when the polarization has no line summand. This is the i = 0 case of TauCeti.spinAction_mem_evenOdd, and the form the spin group consumes.

The even Clifford subalgebra acting on the two half-spin summands

noncomputable def TauCeti.spinPlusAction {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (P : SpinPolarizationData Q) (hline : P.line = ⊥) : ↥(CliffordAlgebra.even Q) →ₐ[K] Module.End K ↥(spinPlus Q P)

The action of the even Clifford subalgebra on the even half-spin summand S⁺, for a polarization without a line summand.

Equations

• TauCeti.spinPlusAction Q P hline = TauCeti.restrictSpinAction✝ P (TauCeti.spinPlus Q P) ⋯

noncomputable def TauCeti.spinMinusAction {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (P : SpinPolarizationData Q) (hline : P.line = ⊥) : ↥(CliffordAlgebra.even Q) →ₐ[K] Module.End K ↥(spinMinus Q P)

The action of the even Clifford subalgebra on the odd half-spin summand S⁻.

Equations

• TauCeti.spinMinusAction Q P hline = TauCeti.restrictSpinAction✝ P (TauCeti.spinMinus Q P) ⋯

@[simp]

theorem TauCeti.coe_spinPlusAction_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) (x : ↥(CliffordAlgebra.even Q)) (s : ↥(spinPlus Q P)) : ↑(((spinPlusAction Q P hline) x) s) = ((spinAction Q P) ↑x) ↑s

The action of an even Clifford element on S⁺ is the Fock action.

@[simp]

theorem TauCeti.coe_spinMinusAction_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) (x : ↥(CliffordAlgebra.even Q)) (s : ↥(spinMinus Q P)) : ↑(((spinMinusAction Q P hline) x) s) = ((spinAction Q P) ↑x) ↑s

The action of an even Clifford element on S⁻ is the Fock action.

noncomputable def TauCeti.evenSpinActionProd {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (P : SpinPolarizationData Q) (hline : P.line = ⊥) : ↥(CliffordAlgebra.even Q) →ₐ[K] Module.End K ↥(spinPlus Q P) × Module.End K ↥(spinMinus Q P)

The paired actions of the even Clifford subalgebra on the half-spin summands.

Equations

• TauCeti.evenSpinActionProd Q P hline = (TauCeti.spinPlusAction Q P hline).prod (TauCeti.spinMinusAction Q P hline)

@[simp]

theorem TauCeti.evenSpinActionProd_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) (x : ↥(CliffordAlgebra.even Q)) : (evenSpinActionProd Q P hline) x = ((spinPlusAction Q P hline) x, (spinMinusAction Q P hline) x)

Invariance of the half-spin summands

theorem TauCeti.spinPlus_invariant {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) (g : ↥(spinGroup Q)) : Submodule.map ((spinRep Q P) g) (spinPlus Q P) ≤ spinPlus Q P

The even half-spin summand is invariant under the spin representation, when the polarization has no line summand: the spin group lies in the even Clifford subalgebra, and an even element preserves exterior parity.

theorem TauCeti.spinMinus_invariant {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) (g : ↥(spinGroup Q)) : Submodule.map ((spinRep Q P) g) (spinMinus Q P) ≤ spinMinus Q P

The odd half-spin summand is invariant under the spin representation, when the polarization has no line summand.

def TauCeti.spinPlusSubrep {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) : Subrepresentation (spinRep Q P)

The even half-spin summand as a subrepresentation of the spin representation.

Equations

• TauCeti.spinPlusSubrep P hline = { toSubmodule := TauCeti.spinPlus Q P, apply_mem_toSubmodule := ⋯ }

def TauCeti.spinMinusSubrep {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) : Subrepresentation (spinRep Q P)

The odd half-spin summand as a subrepresentation of the spin representation.

Equations

• TauCeti.spinMinusSubrep P hline = { toSubmodule := TauCeti.spinMinus Q P, apply_mem_toSubmodule := ⋯ }

@[simp]

theorem TauCeti.toSubmodule_spinPlusSubrep {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) : (spinPlusSubrep P hline).toSubmodule = spinPlus Q P

@[simp]

theorem TauCeti.toSubmodule_spinMinusSubrep {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) : (spinMinusSubrep P hline).toSubmodule = spinMinus Q P

@[simp]

theorem TauCeti.mem_spinPlusSubrep {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) {s : ExteriorAlgebra K ↥P.W} : s ∈ spinPlusSubrep P hline ↔ s ∈ spinPlus Q P

Membership in the even half-spin subrepresentation is membership in S⁺. A goal about a Subrepresentation is stated through its SetLike membership, on which TauCeti.toSubmodule_spinPlusSubrep cannot fire.

@[simp]

theorem TauCeti.mem_spinMinusSubrep {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) {s : ExteriorAlgebra K ↥P.W} : s ∈ spinMinusSubrep P hline ↔ s ∈ spinMinus Q P

Membership in the odd half-spin subrepresentation is membership in S⁻.

theorem TauCeti.coe_spinPlusAction_spinGroup_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) (g : ↥(spinGroup Q)) (s : ↥(spinPlus Q P)) : ↑(((spinPlusAction Q P hline) ⟨↑g, ⋯⟩) s) = ↑(((spinPlusSubrep P hline).toRepresentation g) ⟨↑s, ⋯⟩)

The even-subalgebra action on S⁺, restricted to the spin group, is the representation carried by the even half-spin subrepresentation.

theorem TauCeti.coe_spinMinusAction_spinGroup_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) (g : ↥(spinGroup Q)) (s : ↥(spinMinus Q P)) : ↑(((spinMinusAction Q P hline) ⟨↑g, ⋯⟩) s) = ↑(((spinMinusSubrep P hline).toRepresentation g) ⟨↑s, ⋯⟩)

The even-subalgebra action on S⁻, restricted to the spin group, is the representation carried by the odd half-spin subrepresentation.

theorem TauCeti.isCompl_spinPlusSubrep_spinMinusSubrep {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) : IsCompl (spinPlusSubrep P hline) (spinMinusSubrep P hline)

The spin representation is the sum of its two half-spin subrepresentations. This is TauCeti.isCompl_spinPlus_spinMinus read in the lattice of subrepresentations of spinRep, where it says that the parity splitting of S is a splitting of the spin representation itself.

Odd elements carry each summand into the other

An odd Clifford element maps S⁺ into S⁻ and S⁻ into S⁺. Unlike the spin group, the pin group need not lie in the even subalgebra, so the invariance argument does not extend to it, and that is why the half-spin splitting is stated for spinRep and not for pinRep. Nothing here says that pinRep really does fail to preserve the splitting: that would need an odd element of the pin group whose action does not kill the summand — which for some Q there is none of, the pin group then being even — and it is not proved here.

theorem TauCeti.map_spinAction_spinPlus_le_spinMinus {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) {x : CliffordAlgebra Q} (hx : x ∈ CliffordAlgebra.evenOdd Q 1) : Submodule.map ((spinAction Q P) x) (spinPlus Q P) ≤ spinMinus Q P

An odd Clifford element carries S⁺ into S⁻.

theorem TauCeti.map_spinAction_spinMinus_le_spinPlus {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (hline : P.line = ⊥) {x : CliffordAlgebra Q} (hx : x ∈ CliffordAlgebra.evenOdd Q 1) : Submodule.map ((spinAction Q P) x) (spinMinus Q P) ≤ spinPlus Q P

An odd Clifford element carries S⁻ into S⁺.