The spin group acting on its quadratic space

The spin group is a subgroup of the Lipschitz group, and its action is the restriction of the common twisted-conjugation action on the quadratic space. This file packages that restriction as spinToOrthogonal Q : spinGroup Q →* QuadraticMap.orthogonalGroup Q and records its Clifford application formula.

This is the representation underlying the double cover from the spin group to the special orthogonal group. The determinant-one property and surjectivity require the later Cartan--Dieudonné argument and are deliberately not asserted here.

Main definitions

• CliffordAlgebra.spinVectorAction Q x is the restriction of CliffordAlgebra.lipschitzVectorAction along the canonical Spin inclusion.
• CliffordAlgebra.spinToOrthogonal Q is the resulting homomorphism into O(Q).

References

See H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §2.

noncomputable def CliffordAlgebra.spinVectorAction {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(spinGroup Q)) : M ≃ₗ[R] M

The action of a spin element on the generating vectors of its Clifford algebra, transported back to the underlying module. It is characterized by ι_spinVectorAction_apply, which identifies it with conjugation inside the Clifford algebra.

Equations

• CliffordAlgebra.spinVectorAction Q x = CliffordAlgebra.lipschitzVectorAction Q ((CliffordAlgebra.spinToLipschitz✝ Q) x)

@[simp]

theorem CliffordAlgebra.spinVectorAction_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : spinVectorAction Q 1 = LinearEquiv.refl R M

The identity Spin element acts by the identity linear equivalence.

@[simp]

theorem CliffordAlgebra.spinVectorAction_mul {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x y : ↥(spinGroup Q)) : spinVectorAction Q (x * y) = spinVectorAction Q x * spinVectorAction Q y

The Spin vector action sends products to composition of linear equivalences.

@[simp]

theorem CliffordAlgebra.ι_spinVectorAction_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(spinGroup Q)) (m : M) : (ι Q) ((spinVectorAction Q x) m) = ↑x * (ι Q) m * star ↑x

A spin element acts on a vector by conjugation inside the Clifford algebra.

@[simp]

theorem CliffordAlgebra.spinVectorAction_map_app {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(spinGroup Q)) (m : M) : Q ((spinVectorAction Q x) m) = Q m

Conjugation by a spin element preserves the quadratic form.

noncomputable def CliffordAlgebra.spinToOrthogonal {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : ↥(spinGroup Q) →* ↥(TauCeti.QuadraticMap.orthogonalGroup Q)

The representation of the spin group on the quadratic space by Clifford conjugation.

Equations

• CliffordAlgebra.spinToOrthogonal Q = (CliffordAlgebra.lipschitzToOrthogonal Q).comp (CliffordAlgebra.spinToLipschitz✝ Q)

@[simp]

theorem CliffordAlgebra.coe_spinToOrthogonal_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(spinGroup Q)) (m : M) : ↑((spinToOrthogonal Q) x) m = (spinVectorAction Q x) m

@[instance_reducible]

noncomputable instance CliffordAlgebra.instMulActionSpinGroup {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : MulAction (↥(spinGroup Q)) M

The Spin action on its quadratic space, for every quadratic form with 2 invertible.

Equations

• CliffordAlgebra.instMulActionSpinGroup Q = MulAction.compHom M (CliffordAlgebra.spinToOrthogonal Q)

@[simp]

theorem CliffordAlgebra.spinGroup_smul_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (s : ↥(spinGroup Q)) (x : M) : s • x = (spinVectorAction Q s) x

The induced MulAction agrees pointwise with the transported Clifford-conjugation action.