Surjectivity of the Spin action #
The determinant-one Pin elements are even, so Pin surjectivity restricts to Spin surjectivity onto the special orthogonal group.
Main definitions and results #
CliffordAlgebra.spinToSpecialOrthogonal_surjective_of_pinToOrthogonal_surjectiverestricts any surjective Pin action to a surjective Spin action on the special orthogonal group.CliffordAlgebra.spinToSpecialOrthogonal_surjective_of_isSquareproves its surjectivity when every reflection normalization scalar is a square.CliffordAlgebra.spinToSpecialOrthogonal_surjectivespecializes this to a separably closed field.
References #
See H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §2.
theorem
CliffordAlgebra.spinToSpecialOrthogonal_surjective_of_pinToOrthogonal_surjective
{R : Type u}
{M : Type v}
[CommRing R]
[AddCommGroup M]
[Module R M]
[Module.Free R M]
[Module.Finite R M]
[Invertible 2]
(Q : QuadraticForm R M)
(hpin : Function.Surjective ⇑(pinToOrthogonal Q))
:
A surjective Pin action on a finite free module restricts to a surjective Spin action on the special orthogonal group.
theorem
CliffordAlgebra.spinToSpecialOrthogonal_surjective_of_isSquare
{K : Type u}
{V : Type v}
[Field K]
[AddCommGroup V]
[Module K V]
[FiniteDimensional K V]
[Invertible 2]
(Q : QuadraticForm K V)
(hQ : QuadraticMap.Nondegenerate)
(hsquare : ∀ (v : V) [inst : Invertible (Q v)], IsSquare (-⅟(Q v)))
:
The Spin action surjects onto the special orthogonal group when every reflection normalization scalar is a square.
theorem
CliffordAlgebra.spinToSpecialOrthogonal_surjective
{K : Type u}
{V : Type v}
[Field K]
[AddCommGroup V]
[Module K V]
[FiniteDimensional K V]
[Invertible 2]
[IsSepClosed K]
(Q : QuadraticForm K V)
(hQ : QuadraticMap.Nondegenerate)
:
The Spin action surjects onto the special orthogonal group for a finite-dimensional nondegenerate quadratic space over a separably closed field.