Theorem. Surjectivity of the Spin action [lawson2016spin, I.2, Theorem 2.9, pp. 18--19] [fcap-001B]
✍️source
spinToSpecialOrthogonal_surjective_of_isSquarespinToSpecialOrthogonal_surjective
L∃∀N

    Let \(K\) be a field of characteristic different from \(2\), let \(V\) be finite-dimensional, and let \(Q\) be nondegenerate. Suppose that for every nonisotropic \(v\in V\), the scalar \(-Q(v)^{-1}\) is a square in \(K\). Then the twisted-adjoint action restricts to a surjection \[\operatorname {Spin}(V,Q)\twoheadrightarrow SO(V,Q).\] The underlying homomorphism is TauCeti.CliffordAlgebra.spinToSpecialOrthogonal, and its action on vectors is the usual Spin action by TauCeti.CliffordAlgebra.coe_spinToSpecialOrthogonal_apply.

    Indeed, the square-normalization hypothesis and Cartan--Dieudonne generation give the Pin surjection of Theorem [fcap-000X]. It lifts an element of \(SO(V,Q)\) to Pin; the lift has determinant \(1\), so Lemma [fcap-001A] shows that it is even and therefore lies in Spin. The restriction square

    commutes because both vertical maps are induced by the same twisted Clifford conjugation. Over a separably closed field the square condition is automatic, so nondegeneracy and finite dimension suffice. The general restriction principle from a surjective Pin action is TauCeti.CliffordAlgebra.spinToSpecialOrthogonal_surjective_of_pinToOrthogonal_surjective.

    The square condition is TauCeti's fixed-sign sufficient hypothesis, stronger in general than Lawson--Michelsohn's option to normalize each vector to either sign; see Theorem [fcap-000X]. For a positive-definite real geometric form \(q\), the Clifford convention is \(Q=-q\); hence \(-Q(v)^{-1}>0\) for every nonzero \(v\), so the reflecting vectors can be normalized over \(\mathbb {R}\). This observation does not assert the square condition for arbitrary real signatures.