The spinor module of a polarized quadratic space

A polarization of a quadratic space (V, Q) splits it as W ⊕ W' ⊕ L, with W and W' isotropic and in perfect QuadraticMap.polar-pairing and L an orthogonal remainder carried by a scalar coordinate. This file turns the exterior algebra ⋀·W into a module over the Clifford algebra of Q — the Fock model of the spinor representation. Classically, over ℂ, it is the carrier of the spin and half-spin representations, which no tensor power of V contains; that statement belongs to the complex theory and is not proved here.

The three summands act by three visibly different operators on S = ⋀·W:

• a vector of W acts by exterior multiplication (TauCeti.SpinPolarizationData.wedge), a creation operator;
• a vector of W' acts by contraction against the functional QuadraticMap.polar Q · y that the polarization pairing attaches to it (TauCeti.SpinPolarizationData.contract), an annihilation operator;
• a vector of the remainder acts by its scalar coordinate times the grade involution, or parity operator, of ⋀·W (TauCeti.SpinPolarizationData.lineOperator), which supplies the extra generator in odd dimension.

Assembled into one linear map TauCeti.SpinPolarizationData.cliffordOperator, these satisfy the Clifford relation, and the universal property then produces the algebra homomorphism TauCeti.spinAction. The coefficient in the relation is not a prose "twice": the computation of TauCeti.SpinPolarizationData.cliffordOperator_sq runs through QuadraticMap.polar, which enters through the creation–annihilation anticommutator TauCeti.SpinPolarizationData.contract_wedge and through nothing else.

The exterior algebra is Mathlib's ExteriorAlgebra K W, which is CliffordAlgebra (0 : QuadraticForm K W), so the interior product is the zero-form specialization of CliffordAlgebra.contractLeft and the parity operator is the zero-form specialization of CliffordAlgebra.involute; there is no bespoke exterior-algebra vocabulary here. Everything holds over an arbitrary commutative ring, since TauCeti.SpinPolarizationData already carries the isotropy and pairing that the relation needs; no invertibility of 2 is used.

Surjectivity of TauCeti.spinAction onto Module.End K S when P.W is finite free, and its restriction to pinGroup Q and spinGroup Q, are in TauCeti/RepresentationTheory/Spin/Representation.lean; the half-spin summands are in TauCeti/RepresentationTheory/Spin/HalfSpin/Basic.lean.

Main definitions

• TauCeti.SpinPolarizationData.wedge, TauCeti.SpinPolarizationData.contract, TauCeti.SpinPolarizationData.lineOperator: the three component operators on ⋀·W.
• TauCeti.SpinPolarizationData.cliffordOperator: the operator c v on ⋀·W attached to a vector v of V, assembled from them.
• TauCeti.spinAction: the resulting CliffordAlgebra Q-module structure on ⋀·W.

Main results

• TauCeti.SpinPolarizationData.cliffordOperator_coe_W, TauCeti.SpinPolarizationData.cliffordOperator_coe_W' and TauCeti.SpinPolarizationData.cliffordOperator_coe_line: the operator of a vector of a single summand, in terms of the component operator of that summand.
• TauCeti.SpinPolarizationData.contract_wedge: the only anticommutation relation between the component operators that is not zero, and the one carrying the polarization pairing.
• TauCeti.SpinPolarizationData.cliffordOperator_sq: the Clifford relation c v ∘ c v = Q v • 1.
• TauCeti.spinAction_ι_wedge, TauCeti.spinAction_ι_contract and TauCeti.spinAction_ι_lineOperator: the three summands act by exterior multiplication, contraction, and the parity operator.

References

• Spin representations roadmap, Layer 4, "The Clifford module S = ⋀·W".
• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §5.

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

The creation operator: a vector of the isotropic summand W acts on ⋀·W by exterior multiplication.

Equations

• P.wedge = LinearMap.mul K (ExteriorAlgebra K ↥P.W) ∘ₗ ExteriorAlgebra.ι K

@[simp]

theorem TauCeti.SpinPolarizationData.wedge_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (x : ↥P.W) (s : ExteriorAlgebra K ↥P.W) : (P.wedge x) s = (ExteriorAlgebra.ι K) x * s

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

The annihilation operator: a vector y of the second isotropic summand W' acts on ⋀·W by contraction against the functional x ↦ polar Q x y that the polarization pairing attaches to it.

Equations

• P.contract = CliffordAlgebra.contractLeft ∘ₗ ↑P.pairingEquiv

@[simp]

theorem TauCeti.SpinPolarizationData.contract_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (y : ↥P.W') (s : ExteriorAlgebra K ↥P.W) : (P.contract y) s = (CliffordAlgebra.contractLeft (P.pairingEquiv y)) s

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

The parity operator: a vector of the orthogonal remainder acts on ⋀·W by its scalar coordinate times the grade involution CliffordAlgebra.involute of the exterior algebra. The involution anticommutes with both the creation and the annihilation operators, and the scalar coordinate is the normalization that makes the square of this operator Q z.

Equations

• P.lineOperator = LinearMap.toSpanSingleton K (Module.End K (ExteriorAlgebra K ↥P.W)) CliffordAlgebra.involute.toLinearMap ∘ₗ P.lineCoordinate

@[simp]

theorem TauCeti.SpinPolarizationData.lineOperator_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (z : ↥P.line) (s : ExteriorAlgebra K ↥P.W) : (P.lineOperator z) s = P.lineCoordinate z • CliffordAlgebra.involute s

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

The Clifford operator of a vector: the assembly of the creation, annihilation and parity operators along the polarization coordinates.

Equations

• P.cliffordOperator = (P.wedge.coprod P.contract).coprod P.lineOperator ∘ₗ ↑P.decompositionEquiv.symm

@[simp]

theorem TauCeti.SpinPolarizationData.cliffordOperator_coe_W {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (x : ↥P.W) : P.cliffordOperator ↑x = P.wedge x

On the isotropic summand W the Clifford operator is the creation operator.

@[simp]

theorem TauCeti.SpinPolarizationData.cliffordOperator_coe_W' {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (y : ↥P.W') : P.cliffordOperator ↑y = P.contract y

On the second isotropic summand W' the Clifford operator is the annihilation operator.

@[simp]

theorem TauCeti.SpinPolarizationData.cliffordOperator_coe_line {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (z : ↥P.line) : P.cliffordOperator ↑z = P.lineOperator z

On the orthogonal remainder the Clifford operator is the scaled parity operator.

The squares and the anticommutators of the component operators

Expanding the Clifford relation in polarization coordinates produces six terms: the squares of the three component operators, and the three anticommutators between distinct ones. Five are statements about a single Clifford algebra and come from elsewhere. The two isotropic squares vanish — ExteriorAlgebra.ι_sq_zero for creation and CliffordAlgebra.contractLeft_contractLeft for annihilation — whereas the parity square does not: it is the identity, by CliffordAlgebra.involute_involute, which is what makes the remainder coordinate contribute Q z rather than 0. Parity anticommutes with each of the other two, by CliffordAlgebra.involute_ι through map_mul and by CliffordAlgebra.involute_contractLeft. The sixth term, the creation–annihilation anticommutator, is the only one that sees the polarization and the only nonzero one among the three; it is recorded here.

theorem TauCeti.SpinPolarizationData.contract_wedge {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (x : ↥P.W) (y : ↥P.W') (s : ExteriorAlgebra K ↥P.W) : (P.contract y) ((P.wedge x) s) = QuadraticMap.polar ⇑Q ↑x ↑y • s - (P.wedge x) ((P.contract y) s)

Creation and annihilation anticommute up to the pairing: this is the one anticommutator that is not zero, and the scalar it produces is the polar form of the two vectors. It is what pins the coefficient of the Clifford relation to QuadraticMap.polar.

@[simp]

theorem TauCeti.SpinPolarizationData.quadraticForm_coe_add_coe_add_coe {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (x : ↥P.W) (y : ↥P.W') (z : ↥P.line) : Q (↑x + ↑y + ↑z) = QuadraticMap.polar ⇑Q ↑x ↑y + Q ↑z

The quadratic form of a vector in polarization coordinates: both isotropic summands drop out and the remainder is orthogonal to them, so only the pairing term and the remainder survive.

theorem TauCeti.SpinPolarizationData.cliffordOperator_sq {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (v : V) : P.cliffordOperator v * P.cliffordOperator v = (algebraMap K (Module.End K (ExteriorAlgebra K ↥P.W))) (Q v)

The Clifford relation for the spinor operators: squaring the operator of a vector v returns the scalar Q v. The three cross terms are exactly the three anticommutators — creation against annihilation contributes the pairing, and parity against each of the other two cancels — so the coefficient is read off QuadraticMap.polar, not assumed.

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

The spinor representation of the Clifford algebra: CliffordAlgebra Q acts on the exterior algebra S = ⋀·W of the isotropic summand of a polarization, by exterior multiplication for W, by contraction against the polar pairing for W', and by a multiple of the parity operator for the orthogonal remainder.

This is the Fock model of the spin module. Classically — over an algebraically closed field of characteristic different from 2, with Q nondegenerate and finite-dimensional — it is an isomorphism onto Module.End K S in even dimension, and in odd dimension it factors through one of the two central-idempotent summands of the Clifford algebra; neither statement is proved here, and neither is claimed at the generality of this definition.

Equations

• TauCeti.spinAction Q P = (CliffordAlgebra.lift Q) ⟨P.cliffordOperator, ⋯⟩

@[simp]

theorem TauCeti.spinAction_ι {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (v : V) : (spinAction Q P) ((CliffordAlgebra.ι Q) v) = P.cliffordOperator v

theorem TauCeti.spinAction_ι_wedge {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (x : ↥P.W) (s : ExteriorAlgebra K ↥P.W) : ((spinAction Q P) ((CliffordAlgebra.ι Q) ↑x)) s = (ExteriorAlgebra.ι K) x * s

A vector of the isotropic summand W acts on the spin module by exterior multiplication.

theorem TauCeti.spinAction_ι_contract {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (y : ↥P.W') (s : ExteriorAlgebra K ↥P.W) : ((spinAction Q P) ((CliffordAlgebra.ι Q) ↑y)) s = (CliffordAlgebra.contractLeft (P.pairingEquiv y)) s

A vector of the second isotropic summand W' acts on the spin module by contraction against the functional the polarization pairing attaches to it.

theorem TauCeti.spinAction_ι_lineOperator {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (z : ↥P.line) (s : ExteriorAlgebra K ↥P.W) : ((spinAction Q P) ((CliffordAlgebra.ι Q) ↑z)) s = P.lineCoordinate z • CliffordAlgebra.involute s

A vector of the orthogonal remainder acts on the spin module by its scalar coordinate times the parity operator.