The Spin action on the special orthogonal group

The determinant of the twisted-conjugation action records the parity of a Lipschitz element on a finite free module. Thus the conjugation action of an even element has determinant one. Outside the finite-free case, Mathlib defines the determinant to be one, so the codomain restriction remains canonical.

Main definitions and results

• CliffordAlgebra.spinToSpecialOrthogonal is the Spin action with codomain restricted to the special orthogonal group.
• CliffordAlgebra.ker_spinToSpecialOrthogonal identifies its kernel with that of the orthogonal Spin action.
• CliffordAlgebra.mem_even_of_det_lipschitzToOrthogonal_eq_one shows that a Lipschitz element inducing a determinant-one isometry is even.
• CliffordAlgebra.det_lipschitzToOrthogonal_eq_one_of_mem_even gives the converse: an even Lipschitz element acts with determinant one.
• CliffordAlgebra.coe_spinToSpecialOrthogonal_apply identifies its underlying action with the Spin action on the quadratic module.
• CliffordAlgebra.specialOrthogonalToOrthogonal_spinToSpecialOrthogonal: followed by the inclusion of SO(Q) into O(Q), it is the orthogonal Spin action.

References

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

theorem CliffordAlgebra.det_lipschitzToOrthogonal_eq_one_of_mem_even {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) (x : ↥(lipschitzGroup Q)) (hx : ↑↑x ∈ even Q) : (QuadraticMap.orthogonalDet Q) ((lipschitzToOrthogonal Q) x) = 1

An even Lipschitz element acts with determinant one. Outside the finite-free case, Mathlib's determinant convention makes this automatic.

theorem CliffordAlgebra.mem_even_of_det_lipschitzToOrthogonal_eq_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] [Module.Free R M] [Module.Finite R M] (Q : QuadraticForm R M) (x : ↥(lipschitzGroup Q)) (hdet : (QuadraticMap.orthogonalDet Q) ((lipschitzToOrthogonal Q) x) = 1) : ↑↑x ∈ even Q

A finite-free Lipschitz element whose orthogonal action has determinant one is even.

theorem CliffordAlgebra.mem_even_of_det_pinToOrthogonal_eq_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] [Module.Free R M] [Module.Finite R M] (Q : QuadraticForm R M) (p : ↥(pinGroup Q)) (hdet : LinearEquiv.det ↑((pinToOrthogonal Q) p) = 1) : ↑p ∈ even Q

A finite-free Pin element whose orthogonal action has determinant one is even.

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

The conjugation action of the Spin group, restricted to the determinant-one orthogonal automorphisms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CliffordAlgebra.ker_spinToSpecialOrthogonal {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) : (spinToSpecialOrthogonal Q).ker = (spinToOrthogonal Q).ker

Restricting the codomain of the Spin action to the special orthogonal group does not change its kernel.

@[simp]

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

A Spin element has the same underlying action whether regarded as orthogonal or special orthogonal.

@[simp]

theorem CliffordAlgebra.specialOrthogonalToOrthogonal_spinToSpecialOrthogonal {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) (x : ↥(spinGroup Q)) : (QuadraticMap.specialOrthogonalToOrthogonal Q) ((spinToSpecialOrthogonal Q) x) = (spinToOrthogonal Q) x

The Spin action into SO(Q), followed by the inclusion SO(Q) →* O(Q), is the Spin action into O(Q).