Theorem. The Spin image is the spinor-norm kernel [fcap-0023]
✍️source
range_spinToSpecialOrthogonal_eq_ker_spinorNorm
L∃∀N

    Let \(K\) be a field in which \(2\) is invertible, \(V\) a finite-dimensional \(K\)-space, and \(Q\) a nondegenerate quadratic form. The Clifford norm of a Lipschitz lift, taken modulo squares, descends to \(\nu _Q^O:O(V,Q)\to K^{\times }/(K^\times )^2\) CliffordAlgebra.orthogonalSpinorNorm_lipschitzToOrthogonal. Its restriction to \(SO(V,Q)\) is the spinor norm \(\nu _Q:SO(V,Q)\to K^\times / (K^\times )^2\) CliffordAlgebra.spinorNorm. Then \[\operatorname {im}\bigl (\operatorname {Spin}(V,Q)\to SO(V,Q)\bigr ) =\ker \nu _Q.\] Thus a special orthogonal transformation has a Spin lift exactly when its spinor-norm class is trivial.

    [chevalley1954algebraic, II.3.5--6, pp. 52--53] defines the reversal norm and describes the reduced orthogonal image by square classes of products \(Q(u)Q(v)\). His ordinary Clifford action and reversal norm compare with TauCeti's twisted action on even lifts: grading fixes such lifts, so the two actions agree, and reverse and star norms coincide Remark [fcap-0028]. For a single nonisotropic reflection, the descended orthogonal spinor norm is \[\nu _Q^O(r_v)=[Q(v)]\] CliffordAlgebra.orthogonalSpinorNorm_reflectionOrthogonal. This agrees with Chevalley's reverse norm. TauCeti's star norm on the odd vector lift has class \([-Q(v)]\); it is a different norm. The extra minus sign cancels on an even product, where the reverse and star norms agree.

    Proof. 

      Every Spin element has reverse norm one, so its image has trivial spinor norm CliffordAlgebra.spinorNorm_spinToSpecialOrthogonal. Conversely, suppose first that \(V\) has positive dimension. Take \(g\in SO(V,Q)\) with \(\nu _Q(g)=1\), and choose a Lipschitz lift \(x\) of \(g\). Since \(\det (g)=1\), determinant parity first shows that \(x\) is even CliffordAlgebra.mem_even_of_det_lipschitzToOrthogonal_eq_one Lemma [fcap-001A]. Trivial spinor class says that \(N_{\mathrm {rev}}(x)\) is a square. Scalar normalization therefore produces an even lift with reverse norm one source theorem; by the even-element comparison in Remark [fcap-0028], it lies in Spin and has the same orthogonal action. In dimension zero \(SO(V,Q)\) is trivial, so the image and the spinor-norm kernel are both its identity subgroup.

      References

        Reference. The algebraic theory of spinors [chevalley1954algebraic]

        • 1954
        • Claude Chevalley
        @book{chevalley1954algebraic,
 title = {The Algebraic Theory of Spinors},
 author = {Chevalley, Claude},
 year = {1954},
 publisher = {Columbia University Press}
}

        Context

          From reflection generation to Pin and Spin [fcap-000U]

            One reflection can enlarge the fixed subspace of an orthogonal transformation. Iterating this correction proves reflection generation and makes the unnormalized Lipschitz action onto the orthogonal group. Passing to the norm-one Pin and Spin carriers requires scalar normalization: determinant parity controls evenness, while the spinor norm measures the remaining obstruction over a general field.

            Extending the field preserves the spinor norm through the map on square classes. A quadratic extension can make a nontrivial obstruction vanish; the resulting pair of Spin lifts records this change through its Galois action.

            Isotropic transvections give a complementary explicit family in the Spin image: their nilpotent Clifford lifts add through the quotient \(u^{\perp }/Ku\). A null-frame calculation exhibits the quadratic action term, while a separate factorization retains a radical PGA shear inside the vector-generated carrier.

            Lemma. Fixed-subspace correction by reflections [cartan1981theory, Section 10, pp. 10--12] [fcap-000V]

              Cartan proves reflection factorization by an induction that enlarges the fixed subspace. TauCeti formalizes the correction as a list of at most two anisotropic reflections whose product with \(g\) fixes \(W+Kx\) pointwise TauCeti.QuadraticMap.exists_reflectionOrthogonal_list_prod_mul_eqOn_sup_span_singleton. The statement below repackages that list-valued result: when \(H\) contains every reflection, closure under products places the correcting element in \(H\).

              Let \(K\) be a field of characteristic different from \(2\), let \(Q\) be a quadratic form on a \(K\)-vector space \(V\), and let \(H\le O(V,Q)\) contain every reflection in a nonisotropic vector. Suppose \(g\in O(V,Q)\) fixes a subspace \(W\) pointwise and \(x\in W^{\perp }\) has \(Q(x)\ne 0\). Then there is an element \(r\in H\) such that \[rg\vert _{W+Kx}=\operatorname {id}.\] The correction leaves the previously fixed space untouched and fixes one additional nonisotropic direction. It is either one reflection or a product of two reflections.

              Proof. 

                Compare \(x\) with \(g(x)\). When \(g(x)-x\) is nonisotropic, reflection in that difference carries \(g(x)\) to \(x\); because the difference is orthogonal to \(W\), the reflection fixes \(W\). In the exceptional case \(g(x)+x\) is nonisotropic: reflection in this sum carries \(g(x)\) to \(-x\), and reflection in \(x\) supplies the second factor. Both factors fix \(W\), so their product gives the required correction.

                Lemma. Pin-range refinement of the correction [cartan1981theory, Section 10, pp. 10--12]; [lawson2016spin, I.2, (2.26) and Theorem 2.9, pp. 18--19] [fcap-0018]
                exists_mem_range_pinToOrthogonal_mul_eqOn_sup_span_singleton
                L∃∀N

                  Under the hypotheses of Lemma [fcap-000V], suppose moreover that \(K\) is separably closed and take \(H\) to be the range of the Pin action. Over a separably closed field, TauCeti's fixed-sign square condition from Theorem [fcap-000X] holds, so every reflection factor used by the correction has a square-normalized Pin lift by Lemma [fcap-000B]. The correcting element \(r\) can therefore be chosen in \[\operatorname {range}(\operatorname {pinToOrthogonal}),\] and still satisfies \(rg\vert _{W+Kx}=\operatorname {id}\). The statement concerns the correcting element in the Pin-action range; in the exceptional case it is the image of a product of two Pin lifts, not the image of a single reflecting vector.

                  Theorem. Cartan--Dieudonne generation [lawson2016spin, I.2, Theorem 2.7, p. 17] [fcap-000W]
                  subgroup_eq_top_of_reflection_mem
                  L∃∀N

                    Let \(K\) be a field of characteristic different from \(2\), let \(V\) be finite-dimensional, and let \(Q\) be nondegenerate. Every orthogonal transformation is a product of reflections in nonisotropic vectors. Equivalently, if a subgroup \(H\le O(V,Q)\) contains every such reflection, then \[H=O(V,Q).\] This formulation asserts generation only; it records neither a sharp bound on the number of reflection factors nor a parity formula for such a factorization.

                    Proof. 

                      Begin with the zero fixed subspace, whose restricted polar form is nondegenerate. If the current nondegenerate fixed subspace is not all of \(V\), its orthogonal complement is nonzero and nondegenerate, hence contains a nonisotropic vector. The correction step of Lemma [fcap-000V] enlarges the fixed subspace by that orthogonal line and preserves nondegeneracy. Finite-dimensional induction eventually makes the corrected product the identity, expressing the original transformation as a product of reflections. Cartan gives this fixed-vector induction, including the isotropic-difference case, in [cartan1981theory, Section 10, pp. 10--12].

                      Theorem. Surjectivity of the Pin action [lawson2016spin, I.2, Theorem 2.9, pp. 18--19] [fcap-000X]
                      pinToOrthogonal_surjective_of_isSquarepinToOrthogonal_surjective
                      L∃∀N

                        Let \(K\), \(V\), and \(Q\) be as in Theorem [fcap-000W]. Suppose every scalar \(-Q(v)^{-1}\) attached to a nonisotropic vector is a square in \(K\). Then the twisted-adjoint homomorphism is surjective: \[\operatorname {pinToOrthogonal}:\operatorname {Pin}(V,Q)\twoheadrightarrow O(V,Q).\] Indeed, Lemma [fcap-000B] puts every reflection in its range, and Theorem [fcap-000W] says that those reflections generate the target. In particular the conclusion holds over a separably closed field.

                        Lawson and Michelsohn ask whether a nonzero vector can be rescaled to quadratic length either \(+1\) or \(-1\); see (2.26) and the discussion preceding Theorem 2.9. Under the convention \(Q=-q\), TauCeti's hypothesis asks for the particular scalar \(-Q(v)^{-1}\) to be a square, so every reflecting vector is normalized to one fixed sign. This is a sufficient and generally stronger condition, not an equivalent reformulation of Lawson--Michelsohn's condition.

                        Example. A planar rotation as two reflections [lawson2016spin, I.2, (2.24)--(2.26), p. 18] [fcap-000Y]

                          In an oriented Euclidean plane, let \(u\) and \(v\) be unit normals whose directed angle is \(\frac {\theta }{2}\). Reflection in \(u^{\perp }\) followed by reflection in \(v^{\perp }\) is rotation through \(\theta \). With the convention \(Q=-\langle -,-\rangle \), both vectors have \(Q=-1\), and \[s=\iota (v)\iota (u)\in \operatorname {Spin}(V,Q)\] lifts that rotation. In an oriented orthonormal basis \(e_1,e_2\), the familiar rotor form is \[\pm s=\cos \left (\frac {\theta }{2}\right )+\sin \left (\frac {\theta }{2}\right )\,\iota (e_1)\iota (e_2),\] after choosing the central sign and the order convention for the two reflections. This is the two-dimensional specialization of the paired lift in Theorem [fcap-000C]; the half-angle appears because the Spin element acts by conjugation on vectors.

                          Lemma. Determinant parity detects the even lift [lawson2016spin, I.2, Theorems 2.7 and 2.9, pp. 17--19] [fcap-001A]
                          det_reflectionmem_even_of_det_pinToOrthogonal_eq_one
                          L∃∀N

                            Let \(R\) be a commutative ring in which \(2\) is invertible, let \(M\) be a finite free \(R\)-module, and let \(Q\) be a quadratic form on \(M\). A reflection in a vector of invertible quadratic value has determinant \(-1\). Therefore a product of \(r\) such reflections has determinant \[(-1)^r.\] In particular, every product of an even number of reflections belongs to \(SO(M,Q)\).

                            Lawson--Michelsohn state this parity argument for quadratic vector spaces over a field. The finite-free commutative-ring statement above is the formalized extension: its determinant calculation uses freeness and finiteness, while invertibility of \(2\) identifies the fixed part of the grading involution with the even subalgebra.

                            The Clifford lift remembers this parity. If \(p\in \operatorname {Pin}(M,Q)\) and its orthogonal action has determinant \(1\), then \(p\) lies in the even Clifford subalgebra. Hence \(p\) is a Spin element. Thus any Pin lift of a special orthogonal transformation is automatically even.

                            Proof. 

                              Multiplicativity of the determinant gives the first assertion from \(\det (\rho _v)=-1\). For the second, the grading involution of a Lipschitz element is its determinant sign times that element. If the determinant is \(1\), the involution fixes the Pin element. Because \(2\) is invertible, the fixed submodule of the grading involution is precisely the even Clifford subalgebra.

                              Theorem. Surjectivity of the Spin action [lawson2016spin, I.2, Theorem 2.9, pp. 18--19] [fcap-001B]
                              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 CliffordAlgebra.spinToSpecialOrthogonal, and its action on vectors is the usual Spin action by 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 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.

                                Proposition. The reverse norm descends through the Lipschitz action [fcap-002D]

                                  Let \(K\) be a field of characteristic different from two, let \(V\) be a positive-dimensional finite-dimensional \(K\)-space, and let \(Q\) be nondegenerate. Write \(\Gamma (Q)\) for the vector-generated Lipschitz group, and \(\tau _Q:\Gamma (Q)\to O(V,Q)\) for its twisted action. For \(x\in \Gamma (Q)\), let \(N_{\mathrm {rev}}(x)\in K^{\times }\) be the unique scalar unit satisfying \(\operatorname {rev}(x)x=N_{\mathrm {rev}}(x)\,1\). Set \(\mathcal {S}_K=K^{\times }/(K^{\times })^2\). The top row is exact, and the square commutes:

                                  The determinant arrow is a separate branch: \(SO(V,Q)=\ker (\det )\). It is not part of a longer exact row after \(O(V,Q)\). Positive dimension supplies an anisotropic vector, so scalar units form the displayed kernel; the Lipschitz action is onto CliffordAlgebra.scalarUnits_injective CliffordAlgebra.ker_lipschitzToOrthogonal CliffordAlgebra.lipschitzToOrthogonal_surjective. The right vertical map is the orthogonal spinor norm, while \(\nu _Q=\nu _Q^O|_{SO(V,Q)}\) is its restriction used in Theorem [fcap-0023]. The square expresses descent through the action, not surjectivity of \(\nu _Q^O\) CliffordAlgebra.orthogonalSpinorNorm_lipschitzToOrthogonal.

                                  If \(Q(v)\) is nonzero, then \[N_{\mathrm {rev}}(\widehat v)=Q(v),\qquad \nu _Q^O(r_v)=[Q(v)]\] CliffordAlgebra.cliffordNorm_unitι CliffordAlgebra.orthogonalSpinorNorm_reflectionOrthogonal. Consequently, for an even product \(x=\widehat v_1\cdots \widehat v_{2k}\) of nonisotropic vector lifts, \[\tau _Q(x)=r_{v_1}\cdots r_{v_{2k}}\in SO(V,Q),\qquad \nu _Q(r_{v_1}\cdots r_{v_{2k}}) =\left [\prod _{i=1}^{2k}Q(v_i)\right ].\] Multiplying a lift by \(c\in K^\times \) changes its reverse norm by \(c^2\), so the square class is independent of the chosen lift. [chevalley1954algebraic, II.3.5--6, pp. 52--53] gives these vector and paired-product values. The scalar exact sequence, reflection factorization, and the same square-scaling law appear in [meinrenken2013clifford, Theorem 3.1, pp. 50--51]. Chevalley's quotient statement assumes positive dimension; Meinrenken works with a finite-dimensional characteristic-zero nondegenerate bilinear space.

                                  If \(e:(V,Q)\simeq (V',Q')\) is an isometry equivalence, then conjugation transport preserves both norms: for \(g\in O(V,Q)\) and \(h\in SO(V,Q)\), \[\nu _{Q'}^O(ege^{-1})=\nu _Q^O(g),\qquad \nu _{Q'}(ehe^{-1})=\nu _Q(h).\] It therefore carries \(\ker \nu _Q\) onto \(\ker \nu _{Q'}\) QuadraticMap.IsometryEquiv.orthogonalSpinorNorm_orthogonalGroupCongr QuadraticMap.IsometryEquiv.spinorNorm_specialOrthogonalGroupCongr kernel-transport source. The induced kernel equivalence also commutes with Spin transport Spin-transport source. These are isometry-equivalence statements; they do not assert scalar-extension or orthogonal-product naturality. This is the norm-square companion to the vector-action square in Proposition [fcap-0029].

                                  Theorem. The Spin image is the spinor-norm kernel [fcap-0023]
                                  ✍️source
                                  range_spinToSpecialOrthogonal_eq_ker_spinorNorm
                                  L∃∀N

                                    Let \(K\) be a field in which \(2\) is invertible, \(V\) a finite-dimensional \(K\)-space, and \(Q\) a nondegenerate quadratic form. The Clifford norm of a Lipschitz lift, taken modulo squares, descends to \(\nu _Q^O:O(V,Q)\to K^{\times }/(K^\times )^2\) CliffordAlgebra.orthogonalSpinorNorm_lipschitzToOrthogonal. Its restriction to \(SO(V,Q)\) is the spinor norm \(\nu _Q:SO(V,Q)\to K^\times / (K^\times )^2\) CliffordAlgebra.spinorNorm. Then \[\operatorname {im}\bigl (\operatorname {Spin}(V,Q)\to SO(V,Q)\bigr ) =\ker \nu _Q.\] Thus a special orthogonal transformation has a Spin lift exactly when its spinor-norm class is trivial.

                                    [chevalley1954algebraic, II.3.5--6, pp. 52--53] defines the reversal norm and describes the reduced orthogonal image by square classes of products \(Q(u)Q(v)\). His ordinary Clifford action and reversal norm compare with TauCeti's twisted action on even lifts: grading fixes such lifts, so the two actions agree, and reverse and star norms coincide Remark [fcap-0028]. For a single nonisotropic reflection, the descended orthogonal spinor norm is \[\nu _Q^O(r_v)=[Q(v)]\] CliffordAlgebra.orthogonalSpinorNorm_reflectionOrthogonal. This agrees with Chevalley's reverse norm. TauCeti's star norm on the odd vector lift has class \([-Q(v)]\); it is a different norm. The extra minus sign cancels on an even product, where the reverse and star norms agree.

                                    Proof. 

                                      Every Spin element has reverse norm one, so its image has trivial spinor norm CliffordAlgebra.spinorNorm_spinToSpecialOrthogonal. Conversely, suppose first that \(V\) has positive dimension. Take \(g\in SO(V,Q)\) with \(\nu _Q(g)=1\), and choose a Lipschitz lift \(x\) of \(g\). Since \(\det (g)=1\), determinant parity first shows that \(x\) is even CliffordAlgebra.mem_even_of_det_lipschitzToOrthogonal_eq_one Lemma [fcap-001A]. Trivial spinor class says that \(N_{\mathrm {rev}}(x)\) is a square. Scalar normalization therefore produces an even lift with reverse norm one source theorem; by the even-element comparison in Remark [fcap-0028], it lies in Spin and has the same orthogonal action. In dimension zero \(SO(V,Q)\) is trivial, so the image and the spinor-norm kernel are both its identity subgroup.

                                      Theorem. Spinor norms commute with extension of scalars [fcap-003N]

                                        Let \(L/K\) be an extension of fields of characteristic different from two. Let \(V\) be a positive-dimensional finite-dimensional \(K\)-space, and let \(Q\) be nondegenerate. Set \(V_L=L\otimes _K V\), with extended form \(Q_L\), and write \[j:K^{\times }/(K^\times )^2\longrightarrow L^{\times }/(L^\times )^2, \qquad j([a]_K)=[a]_L.\] For \(g\in O(V,Q)\), scalar extension gives \(g_L(a\otimes v)=a\otimes g(v)\). Then \[\nu _{Q_L}^O(g_L)=j\bigl (\nu _Q^O(g)\bigr ).\] In particular, for \(g\in SO(V,Q)\), \[\nu _{Q_L}(g_L)=j\bigl (\nu _Q(g)\bigr ),\] and \(g_L\) has a Spin lift exactly when \(j(\nu _Q(g))=1\).

                                        Proof. 

                                          A Gram matrix for the unhalved polar form \(B_Q\) has nonzero determinant. Its determinant remains nonzero under the field embedding, so \(Q_L\) is nondegenerate. For \(Q(v)\ne 0\), the reflection formula is \[r_v(x)=x-\frac {B_Q(x,v)}{Q(v)}v.\] Since \(Q_L(1\otimes v)=Q(v)\) and the polar form extends by \(L\)-bilinearity, this formula on pure tensors gives \((r_v)_L=r_{1\otimes v}\). Cartan--Dieudonne writes any orthogonal \(g\) as \(r_{v_1}\cdots r_{v_k}\). The reflection values from Proposition [fcap-002D] therefore give \[\begin {aligned} \nu _{Q_L}^O(g_L) &=\left [\prod _{i=1}^k Q_L(1\otimes v_i)\right ]_L\\ &=j\left (\left [\prod _{i=1}^k Q(v_i)\right ]_K\right ) =j\bigl (\nu _Q^O(g)\bigr ). \end {aligned}\] Determinants also extend, so restricting to \(SO\) proves the second identity. Apply the image/kernel theorem Theorem [fcap-0023] over \(L\) to obtain the lifting criterion.

                                          The Clifford map \(c:\mathcal {C}\kern -2pt\ell (Q)\to \mathcal {C}\kern -2pt\ell (Q_L)\) sends \(\iota _Q(v)\) to \(\iota _{Q_L}(1\otimes v)\). It preserves parity, reversal and products, and carries each nonisotropic vector unit to a nonisotropic vector unit. Thus it restricts to a map of the actual Spin carriers, and their vector actions satisfy \[q_L(c(s))=(q_K(s))_L\qquad (s\in \operatorname {Spin}(Q)),\] where \(q_K\) and \(q_L\) denote the Spin projections. Indeed, apply \(c\) to the conjugation identity on every vector generator. A lift defined over \(K\) therefore remains a lift over \(L\); the next proposition explains how additional lifts can appear when \(j\) kills a nontrivial square class.

                                          [chevalley1954algebraic, Section 2.7, pp. 60--61] describes the Clifford extension, compatibility with the main antiautomorphism, and the group/vector-action inclusions in even dimension. His main antiautomorphism is reversal. The reflection proof above gives the stated naturality in every positive dimension, using the reverse-norm convention of Proposition [fcap-002D].

                                          TauCeti proves the orthogonal and special-orthogonal identities in CliffordAlgebra.orthogonalSpinorNorm_orthogonalGroupBaseChange and CliffordAlgebra.spinorNorm_specialOrthogonalGroupBaseChange under the field, finite-dimensionality, nondegeneracy and invertibility-of-two hypotheses. The commuting Spin-action square is CliffordAlgebra.spinToSpecialOrthogonal_baseChange; its more general input is a finite free module over a commutative ring with two invertible.

                                          Proposition. Spin lifts over a quadratic extension [fcap-003O]

                                            Keep the quadratic-space hypotheses of Theorem [fcap-003N]. Let \(d\in K^\times \) be nonsquare, put \(L=K(\sqrt d)\), and let \(\sigma \) be its nontrivial \(K\)-automorphism. The square-class map has kernel \[\ker j=\{1,[d]_K\}.\] Consequently, for \(g\in SO(V,Q)\), \[g_L\text { has a Spin lift} \quad \Longleftrightarrow \quad \nu _Q(g)\in \{1,[d]_K\}.\] The trivial class already gives a lift over \(K\). If \(\nu _Q(g)=[d]_K\), the two lifts over \(L\) are exchanged by \(\sigma \); neither is the scalar extension of a \(K\)-defined Spin element.

                                            Proof. 

                                              Suppose \(a\in K^\times \) becomes a square in \(L\). Write \[a=(u+v\sqrt d)^2=u^2+dv^2+2uv\sqrt d, \qquad u,v\in K.\] The basis \(1,\sqrt d\) and characteristic different from two give \(uv=0\). If \(v=0\), then \(a=u^2\); if \(u=0\), then \(a=dv^2\). The nonzero remaining coefficient shows that \([a]_K\) is respectively \(1\) or \([d]_K\). Both classes become squares in \(L\), and they are distinct because \(d\) is nonsquare. This proves the kernel formula; Theorem [fcap-003N] gives the criterion for \(g_L\).

                                              Now assume \(\nu _Q(g)=[d]_K\). By Proposition [fcap-002D], take a Lipschitz lift \(x\) of \(g\); determinant parity makes it even. Its reverse norm is \(db^2\) for some \(b\in K^\times \). Replacing \(x\) by \(x/b\) preserves its action and makes \(N_{\mathrm {rev}}(x)=d\). In the extended Clifford algebra set \[s=\frac {c(x)}{\sqrt d}.\] Scalar units are Lipschitz and even by Proposition [fcap-002D]. Thus \(s\) is even and Lipschitz, and \[N_{\mathrm {rev}}(s)=\frac {d}{(\sqrt d)^2}=1.\] The carrier criterion Remark [fcap-0028] places \(s\) in the actual \(\operatorname {Spin}(Q_L)\), and scalar normalization leaves its vector action equal to \(g_L\). Any other Spin lift differs from \(s\) by a scalar unit, by the Lipschitz action kernel over \(L\). Norm one forces that scalar's square to be one, so all lifts are precisely \(s\) and \(-s\).

                                              The coefficient automorphism \(\sigma \) acts semilinearly on \(\mathcal {C}\kern -2pt\ell (Q_L)\): it fixes each extended generator and sends \(\sqrt d\) to \(-\sqrt d\). In particular it fixes \(c(x)\) and gives \[\sigma (s)=-s,\qquad \sigma (-s)=s.\] These elements are distinct because \(s\) is a unit and the characteristic is not two. Every Clifford element obtained by extending coefficients from \(K\) is fixed by \(\sigma \). Neither lift can therefore come from \(\operatorname {Spin}(Q)\), in agreement with its nontrivial spinor-norm obstruction.

                                              For an explicit rational example, take \(K=\mathbb Q\) and \[Q(ae+bf)=a^2+2b^2,\qquad g=-\operatorname {Id}=r_e r_f.\] Here \(e^2=1\), \(f^2=2\), and \(ef=-fe\). Thus \(x=ef\) satisfies \[\operatorname {rev}(x)x=feef=2,\qquad x^2=efef=-2,\] and \(\nu _Q(g)=[2]_{\mathbb Q}\) is nontrivial. Over \(L=\mathbb Q(\sqrt 2)\), however, \[s=\frac {ef}{\sqrt 2},\qquad N_{\mathrm {rev}}(s)=1,\qquad s^2=-1.\] Its vector action is still \(-\operatorname {Id}\). The two Spin lifts \(s,-s\) are interchanged by conjugating \(\sqrt 2\); the rational orthogonal transformation acquires lifts without either lift becoming rational.

                                              Proposition. Eichler transvections have additive Spin lifts [fcap-002M]

                                                Let \(K\) be a field in which \(2\) is invertible, let \(V\) be a \(K\)-space, and let \(Q\) be nondegenerate. Write \(B_Q\) for the unhalved polar form and \(\widehat v=\iota _Q(v)\) for a Clifford generator. Suppose \[Q(u)=0,\qquad B_Q(u,w)=0.\] The Eichler transvection and its Clifford lift are \[\begin {aligned} E_{u,w}(x) &=x+B_Q(x,u)w-B_Q(x,w)u-Q(w)B_Q(x,u)u,\\ L_{u,w}&=1+\widehat w\widehat u. \end {aligned}\] Then \(L_{u,w}\in \operatorname {Spin}(Q)\), its Spin action is \(E_{u,w}\), and \[L_{u,w}^{-1}=\operatorname {rev}(L_{u,w})=1-\widehat w\widehat u.\] The formal transformation formula already makes sense over a commutative ring and module, without nondegeneracy or invertible \(2\) QuadraticMap.transvection_apply QuadraticMap.transvection_mem_specialOrthogonalGroup. The actual Spin lift uses the field, invertible-two, and nondegeneracy hypotheses stated above CliffordAlgebra.coe_spinTransvection CliffordAlgebra.coe_spinToSpecialOrthogonal_spinTransvection.

                                                Indeed, put \(N=\widehat w\widehat u\). The Clifford relations give \[\begin {gathered} N^2=0,\qquad \operatorname {rev}(N)=-N,\\ N\widehat x-\widehat xN =B_Q(x,u)\widehat w-B_Q(x,w)\widehat u,\\ N\widehat xN=Q(w)B_Q(x,u)\widehat u. \end {gathered}\] Thus expansion of \((1+N)\widehat x(1-N)\) gives exactly the displayed formula, including its negative quadratic term, and proves reverse norm one. Actual membership in the vector-generated carrier is a separate point. If \(Q(w)\ne 0\), the explicit factorization is \[1+\widehat w\widehat u =\widehat {\frac {w}{Q(w)}}\, \widehat {\bigl (w+Q(w)u\bigr )},\] and the two quadratic values multiply to \(1\). If \(Q(w)=0\) and \(w\notin Ku\), nondegeneracy supplies \(x\perp u\) with \(b=B_Q(w,x)\ne 0\). For \[a=x+\frac {b-Q(x)}{b}w\] one has \(Q(a)=b\), \(Q(w+a)=2b\), and \(L_{u,w}=L_{u,w+a}L_{u,-a}\), reducing to the nonisotropic case. If \(w\in Ku\), the lift is \(1\). This is the algebraic carrier argument behind the linked formal construction; it needs no finite-dimensionality.

                                                For \(w,w'\in u^\perp \), the cross term \((\widehat w\widehat u)(\widehat {w'}\widehat u)\) vanishes. Hence \[L_{u,w+w'}=L_{u,w}L_{u,w'},\qquad L_{u,-w}=L_{u,w}^{-1},\qquad L_{u,w+cu}=L_{u,w}.\] The same equations hold after projection to the Eichler transformations. Thus the lifts form a homomorphism \[u^{\perp }/Ku\longrightarrow \operatorname {Spin}(Q)\] which commutes with the projection to \(SO(Q)\); when \(u\ne 0\), it is injective CliffordAlgebra.spinTransvection_add CliffordAlgebra.spinTransvection_add_smul CliffordAlgebra.spinToSpecialOrthogonal_comp_spinTransvectionHom CliffordAlgebra.spinTransvectionHom_injective. The domain is \(u^{\perp }/Ku\), not all of \(V/Ku\); for \(u=0\) the family is trivial. If \(V\) is additionally finite-dimensional, these transformations have trivial spinor norm, as predicted by Theorem [fcap-0023] CliffordAlgebra.spinorNorm_transvection.

                                                Chevalley treats the common totally singular case \(Q(u)=Q(w)=B_Q(u,w)=0\): his finite exponential is \(1+\widehat w\widehat u\) and his conjugation formula is the displayed action with its quadratic term zero [chevalley1954algebraic, III.1.7, pp. 73--74]. This passage does not state the arbitrary-\(Q(w)\) formula. Meinrenken's quantization of the bivector \(w\wedge u\) is \(\widehat w\widehat u\); his commutator theorem and exponential Spin comparison recover the full formula over finite-dimensional nondegenerate real or complex spaces [meinrenken2013clifford, Section 2.2.10, Theorem 2.1 and Proposition 2.12, pp. 39--40] [meinrenken2013clifford, Proposition 3.2, pp. 53--54]. Here his symmetric form is the half-polar form \(B_M=b_Q=B_Q/2\). Since \(N^2=0\), both the Clifford and vector exponentials truncate, and the written polynomial calculation fixes the normalization and extends the formula to the stated general field. No claim that every Spin element is one exponential is made.

                                                Example. A null-frame Spin transvection and a radical shear [fcap-002N]

                                                  Let \(K\) be a field in which \(2\) is invertible and take the three-dimensional quadratic space \[Q(au+bv+cz)=ab+c^2.\] Thus \(u,v\) are null, \(B_Q(u,v)=1\), \(Q(z)=1\), and \(z\) is orthogonal to their hyperbolic plane. For \(w=tz\), the preceding lift and action become \[\begin {gathered} L_t=1+t\widehat z\widehat u =\widehat z\,\widehat {(z+tu)},\\ E_t(u)=u,\qquad E_t(z)=z-2tu,\qquad E_t(v)=v+tz-t^2u. \end {gathered}\] Both factors in the displayed product have quadratic value \(1\). Hence the pair criterion puts \(L_t\) directly in the actual Spin group, including at \(t=0\) CliffordAlgebra.ι_mul_ι_mem_spinGroup_of_norm_mul_norm_eq_one. In coordinates \((a,c,b)\) the transformation is \[E_t= \begin {pmatrix} 1&-2t&-t^2\\ 0&1&t\\ 0&0&1 \end {pmatrix}.\] Substitution gives \(Q(E_t x)=Q(x)\), while multiplication gives \(E_sE_t=E_{s+t}\) and \(L_sL_t=L_{s+t}\). At \(t=1/2\), \[z\longmapsto z-u,\qquad v\longmapsto v+\frac 12z-\frac 14u,\] and composing this map with itself gives \(z\mapsto z-2u\) and \(v\mapsto v+z-u\). For \(t\ne 0\), the vector action has \((E_t-1)^2v=-2t^2u\) and \((E_t-1)^3=0\), although the Clifford increment satisfies \((L_t-1)^2=0\). Over \(\mathbb R\), this is the null frame inside the split model of Example [fcap-002I]; over every stated field it is a concrete element of the spinor-norm kernel in Theorem [fcap-0023].

                                                  There is also a precise radical comparison. On the degenerate real form \[Q_{\mathrm {PGA}}(ar+xe+yf)=x^2+y^2\] the line \(\mathbb Rr\) is radical. With \(u=r\) and \(w=te\), the same ring-level transvection formula gives \[\begin {gathered} L_t=1+t\widehat e\widehat r =\widehat e\,\widehat {(e+tr)},\\ E_t(r)=r,\qquad E_t(e)=e-2tr,\qquad E_t(f)=f. \end {gathered}\] The nondegenerate packaged Spin-transvection theorem does not apply here. Nevertheless this particular lift still belongs to the vector-generated Spin carrier, because both displayed factors have quadratic value \(1\); the pair criterion itself needs no nondegeneracy. The quadratic action term vanishes because \(B_Q(r,-)=0\), and now \((E_t-1)^2=0\). This retains the original degenerate Clifford algebra rather than replacing it by the radical quotient of Remark [fcap-002C]. It does not identify the shear with a particular PGA point translation, motor parameter, dual encoding, or orientation convention.

                                                  Example. A mixed-sign isometry has no norm-one Spin lift [fcap-002E]

                                                    On \(\mathbb R^2\), let \(Q(a,b)=a^2-b^2\), \(e_+=(1,0)\), and \(e_-=(0,1)\). The corresponding reflections are \[r_{e_+}=\operatorname {diag}(-1,1),\qquad r_{e_-}=\operatorname {diag}(1,-1),\] so \(g=r_{e_+}r_{e_-}=-I\) lies in \(SO(Q)\). Its spinor norm is \[\nu _Q(g)=[Q(e_+)Q(e_-)]=[-1]\ne [1].\] With the two norm conventions of Remark [fcap-0028], the even Clifford lift \(x=\widehat e_+\widehat e_-\) has \[N_{\mathrm {rev}}(x)=N_*(x)=-1.\] For every \(c\in \mathbb R^\times \), the scalar multiple \(cx\) has norm \(-c^2\), which cannot equal \(1\). More generally, any two Lipschitz lifts of \(g\) differ by a scalar by Proposition [fcap-002D], so no lift can be normalized into the norm-one Spin carrier. Equivalently, the image theorem in Theorem [fcap-0023] excludes a Spin lift because \(\nu _Q(g)\) is nontrivial.

                                                    This is the mixed-sign counterpart to the successful square normalizations in Lemma [fcap-000B] and Theorem [fcap-000C]. Meinrenken notes that over \(\mathbb R\) one sometimes uses the weaker carrier condition \(N(x)=\pm 1\); under that different convention this \(x\) passes the norm test [meinrenken2013clifford, Remark 3.2, p. 52]. TauCeti's Spin group uses the norm-one carrier, so the two conventions must not be identified.

                                                    Remark. Real spinor-norm images and the low-rank boundary [fcap-002F]

                                                      Let \(Q\) be a positive-dimensional finite-dimensional nondegenerate real quadratic form. Distinguish the orthogonal norm \(\nu _Q^O\) on \(O(Q)\) from its restriction \(\nu _Q\) to \(SO(Q)\). Since \(\mathbb R^{\times }/(\mathbb R^\times )^2=\{[1],[-1]\}\), their images and the Spin image are: \[\begin {array}{c|c|c|c} \text {case}&\operatorname {im}\nu _Q^O& \operatorname {im}\nu _Q&\text {Spin image}\\ \hline \text {positive definite}&\{[1]\}&\{[1]\}&SO(Q)\\ \text {negative definite}&\{[1],[-1]\}&\{[1]\}&SO(Q)\\ \text {indefinite}&\{[1],[-1]\}&\{[1],[-1]\}&\ker \nu _Q \end {array}\] For a positive form, every reflected value is a square, so the orthogonal norm is trivial CliffordAlgebra.orthogonalSpinorNorm_eq_one_of_posDef. For a negative form, the orthogonal norm is the determinant square class and is therefore trivial on \(SO(Q)\) CliffordAlgebra.orthogonalSpinorNorm_eq_orthogonalDetSquareClass_of_negDef CliffordAlgebra.spinorNorm_eq_one_of_negDef. In the indefinite case, one positive and one negative reflection give a determinant-one element of norm \([-1]\), so \(\nu _Q\) is onto CliffordAlgebra.spinorNorm_surjective_of_indefinite. Thus the final kernel has index two. The Spin-image column follows from Theorem [fcap-0023]; the table does not identify this kernel with a topological component.

                                                      Rank zero is separate: \(SO(Q)\) is trivial, and the image/kernel theorem uses its subsingleton branch rather than the positive-dimensional scalar row. In rank one, \(SO(Q)\) and its spinor norm are trivial. For any nonzero \(v\), the image of \(\nu _Q^O\) is generated by \([Q(v)]\), and it is trivial exactly when \(Q(v)\) is a square CliffordAlgebra.spinorNorm_eq_one_of_finrank_le_one CliffordAlgebra.orthogonalSpinorNorm_range_eq_zpowers_of_finrank_eq_one CliffordAlgebra.orthogonalSpinorNorm_eq_one_iff_isSquare_apply_of_finrank_eq_one. An indefinite real form has rank at least two. Degenerate or semidefinite PGA forms lie outside every row of this nondegenerate table.

                                                      Theorem. Spin acts transitively on a positive quadratic sphere [fcap-0024]
                                                      exists_spinVectorAction_eq_of_posDef
                                                      L∃∀N

                                                        Let \(V\) be a finite-dimensional real vector space with \(\dim V\geq 2\), and let \(Q\) be positive definite. If \(Q(x)=Q(y)=c>0\), then some \(s\in \operatorname {Spin}(Q)\) satisfies \[\operatorname {spinVectorAction}_Q(s,x)=y.\] In particular, Spin acts transitively on the unit level \(Q(v)=1\). This is a statement about the algebraic vector action; no topology or compactness is needed.

                                                        Cartan's anisotropic-normal reflection has determinant \(-1\) [cartan1981theory, Section 9, pp. 9--10]. His even-reflection correction appears in [cartan1981theory, Section 10, p. 10]. The following two-case calculation gives the sphere orbit explicitly.

                                                        Proof. 

                                                          Write \(B_Q\) for the polar form. For \(a\ne 0\), reflection in the hyperplane perpendicular to \(a\) is \[r_a(v)=v-\frac {B_Q(a,v)}{Q(a)}a.\] If \(x+y\ne 0\), then positive definiteness makes \(x+y\) anisotropic, and \[Q(x+y)=2c+B_Q(x,y)=B_Q(x+y,x).\] Hence \(r_{x+y}(x)=-y\) and \(r_y r_{x+y}(x)=y\). If \(y=-x\), choose a nonzero \(z\) with \(B_Q(z,x)=0\), possible because \(\dim V\geq 2\). Then \(r_z(x)=x\) and \(r_x r_z(x)=y\). Both maps are products of two reflections, so they lie in \(SO(Q)\). The positive-definite surjectivity CliffordAlgebra.spinToSpecialOrthogonal_surjective_of_posDef lifts the chosen map to Spin, whose vector action is the same map.

                                                          The formal surjectivity theorem uses positive \(Q\) directly: every nonzero value \(Q(v)\) has a real square root, making the spinor norm trivial on \(SO(Q)\) CliffordAlgebra.orthogonalSpinorNorm_eq_one_of_posDef. This is a separate route from the fixed-sign sufficient hypothesis in Theorem [fcap-001B].

                                                          Lemma. The real Spin kernel is the scalar pair [gallier2014clifford, Section 1.8, Proposition 1.21, pp. 39--40] [fcap-001C]
                                                          zmodTwoMulEquivKerSpinToSpecialOrthogonal
                                                          L∃∀N

                                                            For a real quadratic space of signature \((p,q)\) with \(p+q>0\), the kernel of the Spin action is the scalar pair: \[(\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \simeq \ker \bigl (\operatorname {Spin}(p,q)\longrightarrow SO(p,q)\bigr ).\] The nontrivial residue class maps to the scalar Clifford element \(-1\). Thus the two kernel elements are precisely \(1\) and \(-1\). This is the kernel used in Gallier's real double-cover theorem.

                                                            TauCeti proves the analogous algebraic statement over a field \(K\): \(V\) is nontrivial and finite-dimensional, \(Q\) is nondegenerate, and \(2\) is invertible in \(K\). Under exactly those hypotheses it constructs the displayed canonical multiplicative equivalence. This is a generalization of the cited real result, not an attribution of arbitrary-field kernel classification to Gallier.

                                                            Theorem. The algebraic Spin extension [meinrenken2013clifford, Definition 3.2, pp. 51--52] [fcap-001D]
                                                            spinDoubleCoverOfSurjectivespinDoubleCover
                                                            L∃∀N

                                                              Let \(K\) be a characteristic-zero field, let \(V\) be nonzero and finite-dimensional, and let its bilinear form be nondegenerate. Meinrenken defines Spin as the even part of the norm-one Clifford group. Its kernel is the scalar pair. If the Spin action is surjective, these data form the group extension \[1\longrightarrow (\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \longrightarrow \operatorname {Spin}(Q)\longrightarrow SO(Q)\longrightarrow 1.\] The left map sends the nontrivial class to \(-1\); the right map is the Spin action. TauCeti packages this generic construction from an explicit surjectivity proof. The group-extension constructor used in that package is GroupExtension.ofMulEquivKer.

                                                              Meinrenken warns that the map to \(SO(V)\) need not be surjective over a general field; it is surjective when every element of \(K\) has a square root, because lifts can then be rescaled to have norm one. TauCeti separates this issue explicitly. Its generic construction assumes a field, a nontrivial finite-dimensional module, invertible \(2\), a nondegenerate quadratic form, and a supplied surjectivity proof. Over a separably closed field, Theorem [fcap-001B] supplies that proof and yields the specialized extension.

                                                              Lemma. The real Pin kernel is the scalar pair [gallier2014clifford, Section 1.8, Proposition 1.21, pp. 39--40] [fcap-001E]
                                                              zmodTwoMulEquivKerPinToOrthogonal
                                                              L∃∀N

                                                                For a real quadratic space of signature \((p,q)\) with \(p+q>0\), the Pin action has the same two-element kernel: \[(\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \simeq \ker \bigl (\operatorname {Pin}(p,q)\longrightarrow O(p,q)\bigr ).\] Its nontrivial generator is the image in Pin of the scalar Spin element \(-1\). The identification is obtained by comparing the Pin kernel with the Spin kernel, not by adding a second pair of central elements. Gallier's real double-cover proof uses exactly the quotient by \(\{\pm 1\}\).

                                                                TauCeti transports the Spin-kernel equivalence to Pin over a field \(K\) when the module is nontrivial and finite-dimensional, \(Q\) is nondegenerate, and \(2\) is invertible. These are the formal theorem's exact assumptions; the cited scholarly claim is the real case.

                                                                Theorem. The algebraic Pin extension [meinrenken2013clifford, Definition 3.2, pp. 51--52] [fcap-001F]
                                                                pinDoubleCoverOfSurjectivepinDoubleCover
                                                                L∃∀N

                                                                  In Meinrenken's characteristic-zero, nonzero, finite-dimensional, nondegenerate setting, Pin is the kernel of the norm on the Clifford group. Its scalar kernel and any proof that the Pin action is surjective determine the group extension \[1\longrightarrow (\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \longrightarrow \operatorname {Pin}(Q)\longrightarrow O(Q)\longrightarrow 1.\] The inclusion sends the nontrivial class to the scalar \(-1\), and the projection is the Pin action. Meinrenken notes that surjectivity can fail over a general field and that square roots for all field elements suffice to normalize lifts. TauCeti's generic theorem instead assumes a field, a nontrivial finite-dimensional module, invertible \(2\), a nondegenerate quadratic form, and an explicit surjectivity proof. Its separably closed specialization obtains that proof from the formal Cartan--Dieudonne route.

                                                                  Proposition. Isometries transport the Spin vector action [fcap-0029]
                                                                  spinGroupMap_spinVectorAction
                                                                  L∃∀N

                                                                    Let \(R\) be a commutative ring, let \(M_1,M_2\) be \(R\)-modules with quadratic forms \(Q_1,Q_2\), and let \(f:M_1\to M_2\) be an \(R\)-linear map satisfying \[Q_2(f(m))=Q_1(m).\] The Clifford universal property gives an algebra homomorphism \(\operatorname {Cl}(f):\mathcal {C}\kern -2pt\ell (Q_1)\to \mathcal {C}\kern -2pt\ell (Q_2)\) characterized on generators by \[\operatorname {Cl}(f)(\iota _{Q_1}(m))=\iota _{Q_2}(f(m))\] CliffordAlgebra.map_apply_ι. It preserves the Spin carrier and therefore restricts to a group homomorphism \(\operatorname {Spin}(f):\operatorname {Spin}(Q_1)\to \operatorname {Spin}(Q_2)\) QuadraticMap.Isometry.spinGroupMap. Concretely, the Clifford map preserves Lipschitz membership QuadraticMap.Isometry.map_mem_lipschitzGroup, evenness CliffordAlgebra.map_mem_even, and Clifford conjugation CliffordAlgebra.map_star; these are the carrier conditions separated in Remark [fcap-0028]. Neither construction requires \(f\) to have an inverse.

                                                                    Now suppose that \(2\) is invertible in \(R\). If \(a_i\) denotes the Spin vector action on \(M_i\), then \[a_2\bigl (\operatorname {Spin}(f)(s),f(m)\bigr ) =f\bigl (a_1(s,m)\bigr ).\] This identity says that the square with horizontal maps \(a_1,a_2\) and vertical maps \(\operatorname {Spin}(f)\times f,f\) commutes. It is the vector-action naturality equation, with no finite-dimensionality or nondegeneracy hypothesis. If \(f\) is instead an isometry equivalence, it induces a Spin equivalence QuadraticMap.IsometryEquiv.spinGroupEquiv, and the same square packages as naturality of the Spin-to-special-orthogonal homomorphism source theorem.

                                                                    A changed Gram matrix shows why the target form is part of the data. Over \(\mathbb Q\), set \(Q_1(x,y)=x^2+y^2\) and \(T(x,y)=(2x,y)\). Keeping the same form on the target does not give an isometry: at \(e_1\), \[Q_1(Te_1)=4\ne 1=Q_1(e_1).\] Correspondingly, the source generator \(\iota _{Q_1}(e_1)\) squares to \(1\), while its proposed image \(\iota _{Q_1}(2e_1)\) squares to \(4\); that assignment cannot define the claimed Clifford map.

                                                                    For the transported target form \(Q_2(x,y)=x^2/4+y^2\), one has \(Q_2(Tv)=Q_1(v)\). In column coordinates, \[G_1=I,\qquad G_2=(T^{-1})^\top G_1T^{-1} =\begin {pmatrix}1/4&0\\0&1\end {pmatrix},\qquad T^\top G_2T=G_1.\] Now \(\iota _{Q_2}(2e_1)^2=Q_2(2e_1)=1\), so the generator relation is preserved. Thus an arbitrary basis scaling is not a fixed-form isometry; it becomes an isometry only after the domain and target forms are related in the correct direction. This differs from the module equivalence \(T_Q:\mathcal {C}\kern -2pt\ell (Q)\simeq \bigwedge M\) in Lemma [fcap-0004], which is not an algebra map.

                                                                    Meinrenken derives \(\operatorname {Cl}(f)\) from the same universal property for a bilinear-form-preserving linear map [meinrenken2013clifford, Section 2.2.2, Proposition 2.2, p. 29]. Chevalley's tensor-quotient construction gives the corresponding extension from generator images whose squares are \(Q(x)\) [chevalley1954algebraic, II.1.1, pp. 38--39]. In Meinrenken's convention \(Q(v)=B(v,v)\), so his \(B\) is the half-polar form \(b_Q\) of Convention [fcap-0027]. These sources work over finite-dimensional vector spaces over fields; Meinrenken assumes characteristic different from two. The formal action square above has the commutative-ring hypotheses stated here. This card makes no claim about scalar extension, orthogonal sums, or composition of extension maps.

                                                                    Remark. Algebraic extension versus topological cover [fcap-000Z]

                                                                      The extensions in Theorem [fcap-001D] and Theorem [fcap-001F] are exact sequences of abstract groups. They record a surjective homomorphism and its two-element kernel, but no topology. For the positive real form, the actual finite-dimensional carrier topology, compact double cover, and connectedness are established in Proposition [fcap-0039]; the stabilizer argument and the universal-cover boundary are established in Proposition [fcap-003A]. Those results do not extend the compact connectedness conclusion to arbitrary real signature.

                                                                      Proposition. The compact real Spin projection is a two-sheeted cover [fcap-0039]

                                                                        For \(n\geq 0\), let \[Q_n^+(x)=\sum _{i=1}^n x_i^2\] on \(\mathbb R^n\), and give its actual vector-generated group \(\operatorname {Spin}(Q_n^+)\) the subspace topology from the finite-dimensional real Clifford algebra. This group is compact for every \(n\); it is path-connected for \(n\geq 2\). For \(n\geq 1\), the vector action is a two-sheeted covering \[\operatorname {Spin}(Q_n^+)\longrightarrow SO(n)\] with kernel \(\{1,-1\}\).

                                                                        Here is the compactness mechanism. Cartan--Dieudonne writes every special orthogonal transformation as a bounded even word of reflections. Positive definiteness normalizes every reflecting vector to the unit sphere. An additional unit-vector pair corrects the possible scalar \(-1\), and pairs \((e,e)\) pad the lift to a fixed length. Clifford multiplication therefore gives a continuous surjection \[\bigl (S^{n-1}\times S^{n-1}\bigr )^{n+1} \longrightarrow \operatorname {Spin}(Q_n^+)\qquad (n\geq 1).\] For \(n=0\), the actual vector-generated carrier is the singleton group, hence compact. For \(n\geq 1\), the displayed source is compact, proving compactness. For \(n\geq 2\) it is also path-connected, proving path-connectedness of the target. The plane curve in Example [fcap-0038] independently joins \(1\) to \(-1\).

                                                                        The vector action is a continuous surjection onto the Hausdorff group \(SO(n)\). Compactness makes it a quotient map. Its two-element kernel is discrete and acts freely, so the quotient-covering theorem makes the action a two-sheeted covering. The finite kernel alone would not prove either the quotient-map or covering assertion.

                                                                        [gallier2014clifford, Section 1.8, pp. 38--40] gives the compact double cover for \(n\geq 1\) and path-connectedness for \(n\geq 2\), using generators with negative square in \(\operatorname {Cl}_{0,n}\). [lawson2016spin, I.2 and I.4, pp. 14, 19, 25] use the same compact sign through \(v^2=-q(v)\).

                                                                        To compare their carrier with the positive-square model above, let \(e_i^2=1\) and \(f_i^2=-1\). The complex map \(e_i\mapsto i f_i\) restricts on real even PBW words to \[F(e_{i_1}\cdots e_{i_{2k}}) =(-1)^k f_{i_1}\cdots f_{i_{2k}}.\] The same formula is its inverse. It is a real linear homeomorphism, preserves multiplication and reversal, and carries an even product of real vectors to the corresponding even product up to a scalar \(-1\). That scalar belongs to both actual carriers, since \(e(-e)=-1\) and \(ff=-1\). Thus \(F\) and its inverse identify the actual Spin carriers. Complexifying the vector action and cancelling the common factor \(i\) shows that they also intertwine the actions on \(\mathbb R^n\). Gallier defines Spin through a normalizer condition; the carrier-completion argument in Proposition [fcap-0037], applied after this sign transfer, identifies that normalizer-defined group with the selected vector-generated carrier. This translates the source convention without identifying the two full real Clifford algebras.

                                                                        TauCeti proves compactness for every \(n\), path-connectedness in dimensions \(n+2\), and the quotient-covering and covering statements for nonzero dimension: CliffordAlgebra.instCompactSpaceRealCliffordSpinGroupZero, CliffordAlgebra.pathConnectedSpace_realCliffordSpinGroupZero_add_two, CliffordAlgebra.isQuotientCoveringMap_realCliffordSpinDoubleCoverZero_rightHom, and CliffordAlgebra.isCoveringMap_realCliffordSpinDoubleCoverZero_rightHom. These exact results concern the positive form and the finite-dimensional carrier topology; they do not assert simple connectedness.

                                                                        Proposition. The compact Spin cover is universal from dimension three [fcap-003A]

                                                                          For \(n\geq 3\), the covering in Proposition [fcap-0039] is the universal covering of \(SO(n)\). The proof uses the action on the unit sphere from Theorem [fcap-0024], together with the topology just supplied.

                                                                          Fix a unit vector \(e\). Its stabilizer in \(\operatorname {Spin}(Q_n^+)\) is the preimage of \(SO(e^\perp )\). The Clifford map for the orthogonal inclusion \(e^\perp \hookrightarrow \mathbb R^n\) embeds \(\operatorname {Spin}(Q_{n-1}^+)\) into that preimage, maps onto \(SO(e^\perp )\), and has the same kernel \(\{1,-1\}\). Hence the embedded subgroup is exactly the stabilizer. It is closed. Using the concrete Lie group structure of Proposition [fcap-0037], the closed-subgroup bundle theorem gives \[\operatorname {Spin}(n-1)\longrightarrow \operatorname {Spin}(n)\longrightarrow S^{n-1}.\] This supplies the stabilizer step rather than inferring a fibration from transitivity alone.

                                                                          One can see the local section directly in the positive-square convention. For a unit vector \(x\ne -e\), put \[u(x)=\frac {e+x}{\sqrt {Q_n^+(e+x)}},\qquad s(x)=\iota (u(x))\iota (e).\] Positive definiteness makes the denominator nonzero, and both vectors have square one. Thus \(s(x)\) is even with reverse norm one. If \(h=\iota (e+x)\), the Clifford relation gives \[h\iota (e)h=\bigl (2+B_Q(e,x)\bigr )\iota (x) =Q_n^+(e+x)\iota (x),\] so \(s(x)\iota (e)s(x)^{-1}=\iota (x)\). The formula is continuous on \(S^{n-1}\setminus \{-e\}\). In TauCeti \(e\) is the last coordinate vector: TauCeti.realCliffordSpinLastLocalSection_apply records the formula, TauCeti.continuousOn_realCliffordSpinLastLocalSection its continuity on that punctured sphere, and TauCeti.realCliffordSpinLastLocalSection_action its orbit identity. The definition assigns the identity at \(-e\); this totalization is not a continuous section on the whole sphere.

                                                                          With \(k=n-1\geq 1\), CliffordAlgebra.realCliffordSpinContinuousMulEquivLastStabilizer identifies \(\operatorname {Spin}(k)\) with the entire last-vector stabilizer in \(\operatorname {Spin}(k+1)\), continuously and multiplicatively. CliffordAlgebra.exists_realCliffordSpinOrbitTrivialization then provides a bundle chart around every sphere point \(y\), with base \(S^k\setminus \{-y\}\) and fiber \(\operatorname {Spin}(k)\); the resulting fiber-bundle statement is CliffordAlgebra.isFiberBundle_realCliffordSpinOrbitMap. These are charts for the actual orbit map, with the same rank shift as the displayed bundle.

                                                                          For \(n=3\), Example [fcap-002H] gives the coordinate isomorphism with unit quaternions. Its displayed linear map and inverse restrict continuously to the unit three-sphere, so \(\operatorname {Spin}(3)\) is simply connected. For \(n\geq 4\), the homotopy exact sequence of the bundle and simple connectedness of \(S^{n-1}\) give a surjection \[\pi _1\operatorname {Spin}(n-1)\longrightarrow \pi _1\operatorname {Spin}(n).\] Induction therefore gives \(\pi _1\operatorname {Spin}(n)=0\) for every \(n\geq 3\). Together with path-connectedness and the two-sheeted covering, this makes \(\operatorname {Spin}(n)\to SO(n)\) the universal cover.

                                                                          The formal base case uses TauCeti.realSpinThreeContinuousMulEquivQuaternionUnitary, the continuous multiplicative quaternion equivalence corresponding to Example [fcap-002H]. The full conclusion CliffordAlgebra.simplyConnectedSpace_realCliffordSpinGroupZero establishes simple connectedness for every \(n\geq 3\). Its induction uses the two antipodal bundle charts: their bases are contractible punctured spheres, their fibers are simply connected by induction, and their overlap is path-connected. Van Kampen then gives simple connectedness of the total space. This implements the same geometric induction through charts rather than the homotopy exact sequence used above. The quaternion case starts the induction; \(\operatorname {Spin}(2)\) is not a simply connected base case. Combining this conclusion with Proposition [fcap-0039] yields the universal-cover assertion.

                                                                          [gallier2014clifford, Section 1.8, pp. 40--42] gives this sphere--stabilizer induction. [meinrenken2013clifford, Section 1.6, Lemma 1.4, p. 13] independently checks the base topology using the parallel sphere fibration for \(SO(n)\). The explicit carrier/stabilizer comparison above is the convention bridge to the selected positive-square model.

                                                                          The lower ranks remain separate: \[\begin {array}{c|c|c} n&\operatorname {Spin}(n)&\text {cover behavior}\\ \hline 0&\{1\}&\text {separate trivial carrier}\\ 1&\{1,-1\}&\text {two sheets over }SO(1),\ \text {not universal}\\ 2&S^1&\text {twofold circle cover of }SO(2),\ \pi _1\ne 0. \end {array}\] The rank-two identification follows from \(a+b e_1e_2\) with \(a=\cos \phi \) and \(b=\sin \phi \). In the orientation of Example [fcap-0038], its vector action has angle \(-2\phi \); hence the map is a twofold circle cover. The formal simple-connectedness theorem therefore has exactly the lower bound needed here; the universal-cover claim combines it with the separately established covering.

                                                                          Backlinks

                                                                            Example. A mixed-sign isometry has no norm-one Spin lift [fcap-002E]

                                                                              On \(\mathbb R^2\), let \(Q(a,b)=a^2-b^2\), \(e_+=(1,0)\), and \(e_-=(0,1)\). The corresponding reflections are \[r_{e_+}=\operatorname {diag}(-1,1),\qquad r_{e_-}=\operatorname {diag}(1,-1),\] so \(g=r_{e_+}r_{e_-}=-I\) lies in \(SO(Q)\). Its spinor norm is \[\nu _Q(g)=[Q(e_+)Q(e_-)]=[-1]\ne [1].\] With the two norm conventions of Remark [fcap-0028], the even Clifford lift \(x=\widehat e_+\widehat e_-\) has \[N_{\mathrm {rev}}(x)=N_*(x)=-1.\] For every \(c\in \mathbb R^\times \), the scalar multiple \(cx\) has norm \(-c^2\), which cannot equal \(1\). More generally, any two Lipschitz lifts of \(g\) differ by a scalar by Proposition [fcap-002D], so no lift can be normalized into the norm-one Spin carrier. Equivalently, the image theorem in Theorem [fcap-0023] excludes a Spin lift because \(\nu _Q(g)\) is nontrivial.

                                                                              This is the mixed-sign counterpart to the successful square normalizations in Lemma [fcap-000B] and Theorem [fcap-000C]. Meinrenken notes that over \(\mathbb R\) one sometimes uses the weaker carrier condition \(N(x)=\pm 1\); under that different convention this \(x\) passes the norm test [meinrenken2013clifford, Remark 3.2, p. 52]. TauCeti's Spin group uses the norm-one carrier, so the two conventions must not be identified.

                                                                              Example. A null-frame Spin transvection and a radical shear [fcap-002N]

                                                                                Let \(K\) be a field in which \(2\) is invertible and take the three-dimensional quadratic space \[Q(au+bv+cz)=ab+c^2.\] Thus \(u,v\) are null, \(B_Q(u,v)=1\), \(Q(z)=1\), and \(z\) is orthogonal to their hyperbolic plane. For \(w=tz\), the preceding lift and action become \[\begin {gathered} L_t=1+t\widehat z\widehat u =\widehat z\,\widehat {(z+tu)},\\ E_t(u)=u,\qquad E_t(z)=z-2tu,\qquad E_t(v)=v+tz-t^2u. \end {gathered}\] Both factors in the displayed product have quadratic value \(1\). Hence the pair criterion puts \(L_t\) directly in the actual Spin group, including at \(t=0\) CliffordAlgebra.ι_mul_ι_mem_spinGroup_of_norm_mul_norm_eq_one. In coordinates \((a,c,b)\) the transformation is \[E_t= \begin {pmatrix} 1&-2t&-t^2\\ 0&1&t\\ 0&0&1 \end {pmatrix}.\] Substitution gives \(Q(E_t x)=Q(x)\), while multiplication gives \(E_sE_t=E_{s+t}\) and \(L_sL_t=L_{s+t}\). At \(t=1/2\), \[z\longmapsto z-u,\qquad v\longmapsto v+\frac 12z-\frac 14u,\] and composing this map with itself gives \(z\mapsto z-2u\) and \(v\mapsto v+z-u\). For \(t\ne 0\), the vector action has \((E_t-1)^2v=-2t^2u\) and \((E_t-1)^3=0\), although the Clifford increment satisfies \((L_t-1)^2=0\). Over \(\mathbb R\), this is the null frame inside the split model of Example [fcap-002I]; over every stated field it is a concrete element of the spinor-norm kernel in Theorem [fcap-0023].

                                                                                There is also a precise radical comparison. On the degenerate real form \[Q_{\mathrm {PGA}}(ar+xe+yf)=x^2+y^2\] the line \(\mathbb Rr\) is radical. With \(u=r\) and \(w=te\), the same ring-level transvection formula gives \[\begin {gathered} L_t=1+t\widehat e\widehat r =\widehat e\,\widehat {(e+tr)},\\ E_t(r)=r,\qquad E_t(e)=e-2tr,\qquad E_t(f)=f. \end {gathered}\] The nondegenerate packaged Spin-transvection theorem does not apply here. Nevertheless this particular lift still belongs to the vector-generated Spin carrier, because both displayed factors have quadratic value \(1\); the pair criterion itself needs no nondegeneracy. The quadratic action term vanishes because \(B_Q(r,-)=0\), and now \((E_t-1)^2=0\). This retains the original degenerate Clifford algebra rather than replacing it by the radical quotient of Remark [fcap-002C]. It does not identify the shear with a particular PGA point translation, motor parameter, dual encoding, or orientation convention.

                                                                                Proposition. Eichler transvections have additive Spin lifts [fcap-002M]

                                                                                  Let \(K\) be a field in which \(2\) is invertible, let \(V\) be a \(K\)-space, and let \(Q\) be nondegenerate. Write \(B_Q\) for the unhalved polar form and \(\widehat v=\iota _Q(v)\) for a Clifford generator. Suppose \[Q(u)=0,\qquad B_Q(u,w)=0.\] The Eichler transvection and its Clifford lift are \[\begin {aligned} E_{u,w}(x) &=x+B_Q(x,u)w-B_Q(x,w)u-Q(w)B_Q(x,u)u,\\ L_{u,w}&=1+\widehat w\widehat u. \end {aligned}\] Then \(L_{u,w}\in \operatorname {Spin}(Q)\), its Spin action is \(E_{u,w}\), and \[L_{u,w}^{-1}=\operatorname {rev}(L_{u,w})=1-\widehat w\widehat u.\] The formal transformation formula already makes sense over a commutative ring and module, without nondegeneracy or invertible \(2\) QuadraticMap.transvection_apply QuadraticMap.transvection_mem_specialOrthogonalGroup. The actual Spin lift uses the field, invertible-two, and nondegeneracy hypotheses stated above CliffordAlgebra.coe_spinTransvection CliffordAlgebra.coe_spinToSpecialOrthogonal_spinTransvection.

                                                                                  Indeed, put \(N=\widehat w\widehat u\). The Clifford relations give \[\begin {gathered} N^2=0,\qquad \operatorname {rev}(N)=-N,\\ N\widehat x-\widehat xN =B_Q(x,u)\widehat w-B_Q(x,w)\widehat u,\\ N\widehat xN=Q(w)B_Q(x,u)\widehat u. \end {gathered}\] Thus expansion of \((1+N)\widehat x(1-N)\) gives exactly the displayed formula, including its negative quadratic term, and proves reverse norm one. Actual membership in the vector-generated carrier is a separate point. If \(Q(w)\ne 0\), the explicit factorization is \[1+\widehat w\widehat u =\widehat {\frac {w}{Q(w)}}\, \widehat {\bigl (w+Q(w)u\bigr )},\] and the two quadratic values multiply to \(1\). If \(Q(w)=0\) and \(w\notin Ku\), nondegeneracy supplies \(x\perp u\) with \(b=B_Q(w,x)\ne 0\). For \[a=x+\frac {b-Q(x)}{b}w\] one has \(Q(a)=b\), \(Q(w+a)=2b\), and \(L_{u,w}=L_{u,w+a}L_{u,-a}\), reducing to the nonisotropic case. If \(w\in Ku\), the lift is \(1\). This is the algebraic carrier argument behind the linked formal construction; it needs no finite-dimensionality.

                                                                                  For \(w,w'\in u^\perp \), the cross term \((\widehat w\widehat u)(\widehat {w'}\widehat u)\) vanishes. Hence \[L_{u,w+w'}=L_{u,w}L_{u,w'},\qquad L_{u,-w}=L_{u,w}^{-1},\qquad L_{u,w+cu}=L_{u,w}.\] The same equations hold after projection to the Eichler transformations. Thus the lifts form a homomorphism \[u^{\perp }/Ku\longrightarrow \operatorname {Spin}(Q)\] which commutes with the projection to \(SO(Q)\); when \(u\ne 0\), it is injective CliffordAlgebra.spinTransvection_add CliffordAlgebra.spinTransvection_add_smul CliffordAlgebra.spinToSpecialOrthogonal_comp_spinTransvectionHom CliffordAlgebra.spinTransvectionHom_injective. The domain is \(u^{\perp }/Ku\), not all of \(V/Ku\); for \(u=0\) the family is trivial. If \(V\) is additionally finite-dimensional, these transformations have trivial spinor norm, as predicted by Theorem [fcap-0023] CliffordAlgebra.spinorNorm_transvection.

                                                                                  Chevalley treats the common totally singular case \(Q(u)=Q(w)=B_Q(u,w)=0\): his finite exponential is \(1+\widehat w\widehat u\) and his conjugation formula is the displayed action with its quadratic term zero [chevalley1954algebraic, III.1.7, pp. 73--74]. This passage does not state the arbitrary-\(Q(w)\) formula. Meinrenken's quantization of the bivector \(w\wedge u\) is \(\widehat w\widehat u\); his commutator theorem and exponential Spin comparison recover the full formula over finite-dimensional nondegenerate real or complex spaces [meinrenken2013clifford, Section 2.2.10, Theorem 2.1 and Proposition 2.12, pp. 39--40] [meinrenken2013clifford, Proposition 3.2, pp. 53--54]. Here his symmetric form is the half-polar form \(B_M=b_Q=B_Q/2\). Since \(N^2=0\), both the Clifford and vector exponentials truncate, and the written polynomial calculation fixes the normalization and extends the formula to the stated general field. No claim that every Spin element is one exponential is made.

                                                                                  Remark. Real spinor-norm images and the low-rank boundary [fcap-002F]

                                                                                    Let \(Q\) be a positive-dimensional finite-dimensional nondegenerate real quadratic form. Distinguish the orthogonal norm \(\nu _Q^O\) on \(O(Q)\) from its restriction \(\nu _Q\) to \(SO(Q)\). Since \(\mathbb R^{\times }/(\mathbb R^\times )^2=\{[1],[-1]\}\), their images and the Spin image are: \[\begin {array}{c|c|c|c} \text {case}&\operatorname {im}\nu _Q^O& \operatorname {im}\nu _Q&\text {Spin image}\\ \hline \text {positive definite}&\{[1]\}&\{[1]\}&SO(Q)\\ \text {negative definite}&\{[1],[-1]\}&\{[1]\}&SO(Q)\\ \text {indefinite}&\{[1],[-1]\}&\{[1],[-1]\}&\ker \nu _Q \end {array}\] For a positive form, every reflected value is a square, so the orthogonal norm is trivial CliffordAlgebra.orthogonalSpinorNorm_eq_one_of_posDef. For a negative form, the orthogonal norm is the determinant square class and is therefore trivial on \(SO(Q)\) CliffordAlgebra.orthogonalSpinorNorm_eq_orthogonalDetSquareClass_of_negDef CliffordAlgebra.spinorNorm_eq_one_of_negDef. In the indefinite case, one positive and one negative reflection give a determinant-one element of norm \([-1]\), so \(\nu _Q\) is onto CliffordAlgebra.spinorNorm_surjective_of_indefinite. Thus the final kernel has index two. The Spin-image column follows from Theorem [fcap-0023]; the table does not identify this kernel with a topological component.

                                                                                    Rank zero is separate: \(SO(Q)\) is trivial, and the image/kernel theorem uses its subsingleton branch rather than the positive-dimensional scalar row. In rank one, \(SO(Q)\) and its spinor norm are trivial. For any nonzero \(v\), the image of \(\nu _Q^O\) is generated by \([Q(v)]\), and it is trivial exactly when \(Q(v)\) is a square CliffordAlgebra.spinorNorm_eq_one_of_finrank_le_one CliffordAlgebra.orthogonalSpinorNorm_range_eq_zpowers_of_finrank_eq_one CliffordAlgebra.orthogonalSpinorNorm_eq_one_iff_isSquare_apply_of_finrank_eq_one. An indefinite real form has rank at least two. Degenerate or semidefinite PGA forms lie outside every row of this nondegenerate table.

                                                                                    Remark. Reverse norm signs and the Spin carrier [fcap-0028]

                                                                                      Let \(R\) be a commutative ring, let \(M\) be an \(R\)-module, and let \(Q\) be a quadratic form on \(M\). Write \(\widehat v=\iota _Q(v)\) for a Clifford generator. Before imposing any invertibility condition, consider the two algebra-valued norm expressions \(N_{\mathrm {rev}}(x)=\operatorname {rev}(x)x\) and \(N_*(x)=x^*x\), where \(x^*=\operatorname {rev}(\alpha (x))\). Identifying a scalar with its image in the Clifford algebra gives \[\begin {aligned} N_{\mathrm {rev}}(\widehat v)&=Q(v), &N_*(\widehat v)&=-Q(v),\\ N_{\mathrm {rev}}(\widehat u\widehat v) &=\widehat v\widehat u\widehat u\widehat v =Q(u)Q(v), &N_*(\widehat u\widehat v)&=Q(u)Q(v). \end {aligned}\] Thus the two signs differ on one generator and agree on a product of two. More generally, reversal gives the product of the quadratic values on every vector word CliffordAlgebra.reverse_prod_map_ι_mul_prod_map_ι, and the two norm expressions agree on every even Clifford element CliffordAlgebra.star_mul_self_eq_reverse_mul_self_of_mem_even.

                                                                                      For a Clifford unit \(x\), membership in the even-unitary carrier is equivalent to evenness together with \(N_{\mathrm {rev}}(x)=1\) CliffordAlgebra.evenUnitaryGroup.mem_iff_reverse_mul_self_eq_one. Those two conditions do not establish Lipschitz membership, which must be retained in the Spin criterion. Precisely, \[\operatorname {im}\bigl (\operatorname {Spin}(Q)\longrightarrow \operatorname {Cl}(Q)^\times \bigr ) =\operatorname {Lipschitz}(Q)\cap \operatorname {EvenUnitary}(Q)\] CliffordAlgebra.range_spinGroup_toUnits. Consequently, if \(Q(u)Q(v)=1\), then \(\widehat u\widehat v\) is an even product of Lipschitz vector units with reverse norm one, hence a Spin element CliffordAlgebra.ι_mul_ι_mem_spinGroup_of_norm_mul_norm_eq_one. This is an unquotiented scalar calculation. The passage to square classes, including the odd reflection sign and its cancellation on even products, is recorded separately in Theorem [fcap-0023].

                                                                                      Chevalley obtains the same norm from what he calls the main antiautomorphism and records \(\lambda (v)=Q(v)\) and the paired values \(Q(u)Q(v)\) [chevalley1954algebraic, II.3.5--6, pp. 52--53]. His symbol \(\alpha \) in that passage denotes reversal, whereas \(\alpha \) in Lemma [fcap-0021] denotes the grading involution. Meinrenken calls reversal transposition, writes \(N(x)=x^\top x\), and defines Spin as its norm-one subgroup inside the special Clifford group [meinrenken2013clifford, Sections 2.2.6 and 3.1.1--2, pp. 34, 49--51]. His convention has \(Q(v)=B(v,v)\), so his \(B\) is the half-polar form \(b_Q\) of Convention [fcap-0027]. Both sources work in narrower finite-dimensional field settings; Meinrenken here assumes characteristic zero and a nondegenerate form. The formal identities linked above hold under the commutative-ring and module hypotheses stated here.

                                                                                      Theorem. Spinor norms commute with extension of scalars [fcap-003N]

                                                                                        Let \(L/K\) be an extension of fields of characteristic different from two. Let \(V\) be a positive-dimensional finite-dimensional \(K\)-space, and let \(Q\) be nondegenerate. Set \(V_L=L\otimes _K V\), with extended form \(Q_L\), and write \[j:K^{\times }/(K^\times )^2\longrightarrow L^{\times }/(L^\times )^2, \qquad j([a]_K)=[a]_L.\] For \(g\in O(V,Q)\), scalar extension gives \(g_L(a\otimes v)=a\otimes g(v)\). Then \[\nu _{Q_L}^O(g_L)=j\bigl (\nu _Q^O(g)\bigr ).\] In particular, for \(g\in SO(V,Q)\), \[\nu _{Q_L}(g_L)=j\bigl (\nu _Q(g)\bigr ),\] and \(g_L\) has a Spin lift exactly when \(j(\nu _Q(g))=1\).

                                                                                        Proof. 

                                                                                          A Gram matrix for the unhalved polar form \(B_Q\) has nonzero determinant. Its determinant remains nonzero under the field embedding, so \(Q_L\) is nondegenerate. For \(Q(v)\ne 0\), the reflection formula is \[r_v(x)=x-\frac {B_Q(x,v)}{Q(v)}v.\] Since \(Q_L(1\otimes v)=Q(v)\) and the polar form extends by \(L\)-bilinearity, this formula on pure tensors gives \((r_v)_L=r_{1\otimes v}\). Cartan--Dieudonne writes any orthogonal \(g\) as \(r_{v_1}\cdots r_{v_k}\). The reflection values from Proposition [fcap-002D] therefore give \[\begin {aligned} \nu _{Q_L}^O(g_L) &=\left [\prod _{i=1}^k Q_L(1\otimes v_i)\right ]_L\\ &=j\left (\left [\prod _{i=1}^k Q(v_i)\right ]_K\right ) =j\bigl (\nu _Q^O(g)\bigr ). \end {aligned}\] Determinants also extend, so restricting to \(SO\) proves the second identity. Apply the image/kernel theorem Theorem [fcap-0023] over \(L\) to obtain the lifting criterion.

                                                                                          The Clifford map \(c:\mathcal {C}\kern -2pt\ell (Q)\to \mathcal {C}\kern -2pt\ell (Q_L)\) sends \(\iota _Q(v)\) to \(\iota _{Q_L}(1\otimes v)\). It preserves parity, reversal and products, and carries each nonisotropic vector unit to a nonisotropic vector unit. Thus it restricts to a map of the actual Spin carriers, and their vector actions satisfy \[q_L(c(s))=(q_K(s))_L\qquad (s\in \operatorname {Spin}(Q)),\] where \(q_K\) and \(q_L\) denote the Spin projections. Indeed, apply \(c\) to the conjugation identity on every vector generator. A lift defined over \(K\) therefore remains a lift over \(L\); the next proposition explains how additional lifts can appear when \(j\) kills a nontrivial square class.

                                                                                          [chevalley1954algebraic, Section 2.7, pp. 60--61] describes the Clifford extension, compatibility with the main antiautomorphism, and the group/vector-action inclusions in even dimension. His main antiautomorphism is reversal. The reflection proof above gives the stated naturality in every positive dimension, using the reverse-norm convention of Proposition [fcap-002D].

                                                                                          TauCeti proves the orthogonal and special-orthogonal identities in CliffordAlgebra.orthogonalSpinorNorm_orthogonalGroupBaseChange and CliffordAlgebra.spinorNorm_specialOrthogonalGroupBaseChange under the field, finite-dimensionality, nondegeneracy and invertibility-of-two hypotheses. The commuting Spin-action square is CliffordAlgebra.spinToSpecialOrthogonal_baseChange; its more general input is a finite free module over a commutative ring with two invertible.

                                                                                          Example. The Lorentz Spin action is Hermitian matrix congruence [fcap-0040]

                                                                                            In the Pauli model Example [fcap-002L], an odd vector becomes an even element after multiplication by \(e_0\). Encode \(v=te_0+x_1e_1+x_2e_2+x_3e_3\) by \[X(v)=\Psi (ve_0)=t1-\sum _{j=1}^3x_j\sigma _j =\begin {pmatrix}t-x_3&-x_1+i x_2\\-x_1-i x_2&t+x_3\end {pmatrix}.\] A matrix is Hermitian when \(Z^*=Z\), where \(*\) denotes conjugate transpose. Every Hermitian two-by-two matrix has the form \(Z=\begin {pmatrix}a&z\\\overline z&d\end {pmatrix}\) with \(a,d\in \mathbb R\). The inverse coordinates are \[X^{-1}(Z)=\left (\frac {a+d}{2},-\operatorname {Re}z, \operatorname {Im}z,\frac {d-a}{2}\right ).\] Thus \(X\) is a real linear equivalence, and direct expansion gives \[\det X(v)=t^2-x_1^2-x_2^2-x_3^2=Q_{1,3}(v).\]

                                                                                            For \(s\in \operatorname {Spin}(Q_{1,3})\), put \(M=\Psi (s)\in SL_2(\mathbb C)\). Then the vector action is \[X(svs^{-1})=M X(v)M^*.\] To prove it, conjugation by \(e_0\) defines an automorphism \(\gamma (x)=e_0xe_0\) of the even algebra. It negates each \(A_j=e_0e_j\) and the volume element \(I=e_0e_1e_2e_3\). On the matrix side, \(M\mapsto \operatorname {adj}(M)^*\) has the same effect on \(\sigma _j\) and \(-i1\). It is a real algebra automorphism: both adjugation and conjugate transpose reverse products, and in size two adjugation is linear. Checking the even generators therefore gives \[\Psi (\gamma (x))=\operatorname {adj}(\Psi (x))^*.\] Now multiply the Clifford action by \(e_0\): \[(svs^{-1})e_0=s(ve_0)\gamma (s^{-1}).\] Since \(\det M=1\), we have \(\operatorname {adj}(M^{-1})=M\). Applying \(\Psi \) proves the congruence formula. It preserves Hermitian matrices, and its determinant is unchanged because \(\det M=\det M^*=1\).

                                                                                            The square makes the coordinate meaning of the action explicit:

                                                                                            For example, let \(M=\operatorname {diag}(e^{r/2},e^{-r/2})\). Its congruence multiplies \(t-x_3\) by \(e^r\), multiplies \(t+x_3\) by \(e^{-r}\), and fixes the off-diagonal entries. Hence \[\begin {aligned} t'&=\cosh (r)t-\sinh (r)x_3,& x_1'&=x_1,\\ x_3'&=-\sinh (r)t+\cosh (r)x_3,& x_2'&=x_2. \end {aligned}\] This is the boost with the sign selected by \(X=t1-x\cdot \sigma \). The null cone is exactly the Hermitian matrices of rank at most one.

                                                                                            For comparison with the formal opposite-signature model, use \(T\) and \(E\) from Lemma [fcap-003Z]. TauCeti's vector equivalence has coordinates \[H(y)=\begin {pmatrix}y_3+y_2&-y_1-i y_0\\ -y_1+i y_0&y_3-y_2\end {pmatrix},\qquad \det H(y)=-Q_{3,1}(y)\] TauCeti.coe_realCliffordThreeOneVectorEquivHermitian_apply TauCeti.realCliffordThreeOneVectorEquivHermitian_det. Substitution gives \(H(Tv)=X(v)\). In the even algebra this is the same identity as \(E(ve_0)=-T(v)f_3\), since \(H(y)=\Phi (-yf_3)\). The group coercion formula TauCeti.coe_realSpinThreeOneEquivSpecialLinear_apply identifies the matrix of \(E(s)\) with \(\Phi (E(s))=\Psi (s)=M\). Consequently the action dictionary in Lemma [fcap-003Z] translates TauCeti's exact Hermitian congruence theorem TauCeti.realSpinThreeOneEquivSpecialLinear_action into the displayed Pauli action. This checks both the signature sign and the matrix axes, not just the abstract group type.

                                                                                            Multiplication by a fixed nonisotropic vector is the even-algebra action mechanism of [porteous1995clifford, Chapter 16, Proposition 16.9, pp. 143--144]. His Lorentz group calculation uses adjugation and the norm-one carrier [porteous1995clifford, Chapter 17, Proposition 17.5, pp. 151--152]. The coordinates and conjugate-transpose action above are derived in our chosen axes. The orthogonal image retains the spinor-norm condition of Theorem [fcap-0023]; a topological component identification is separate.

                                                                                            Definition [ca-000J]Definition [spin-000O]

                                                                                            Example. The Lorentzian four-dimensional Spin group is \(SL_2(\mathbb C)\) [fcap-002L]

                                                                                              For \(Q_{1,3}=x_0^2-x_1^2-x_2^2-x_3^2\), put \(A_j=e_0e_j\) for \(1\le j\le 3\) and \(I=e_0e_1e_2e_3\). Then the \(A_j\) square to \(1\) and anticommute, while \[I^2=-1,\qquad A_1A_2A_3=-I.\] For the Pauli matrices \[\sigma _1=\begin {pmatrix}0&1\\1&0\end {pmatrix},\quad \sigma _2=\begin {pmatrix}0&-i\\i&0\end {pmatrix},\quad \sigma _3=\begin {pmatrix}1&0\\0&-1\end {pmatrix},\] the assignments \(\Psi (A_j)=\sigma _j\) define a real-algebra map from the even Clifford algebra to \(M_2(\mathbb C)\). Since \(\sigma _1\sigma _2\sigma _3=i1\), necessarily \(\Psi (I)=-i1\). The images of \(1,A_1,A_2,A_3,I,IA_1,IA_2,IA_3\) form a real basis, so \(\Psi \) is an algebra equivalence.

                                                                                              Write a matrix uniquely as \[M=z_0 1+z_1\sigma _1+z_2\sigma _2+z_3\sigma _3, \qquad z_j=a_j+i b_j,\] where \[\begin {aligned} z_0&=(m_{11}+m_{22})/2,&z_3&=(m_{11}-m_{22})/2,\\ z_1&=(m_{12}+m_{21})/2,&z_2&=(m_{21}-m_{12})/(2i). \end {aligned}\] Then an explicit inverse is \[\Psi ^{-1}(M) =a_0+\sum _{j=1}^3a_jA_j -I\left (b_0+\sum _{j=1}^3b_jA_j\right ).\] Reversal fixes \(I\) and negates every \(A_j\); under \(\Psi \) it is the complex-linear matrix adjugate. Hence \[\Psi (\operatorname {rev}(x))=\operatorname {adj}(\Psi (x)),\qquad \Psi (\operatorname {rev}(x)x)=\det (\Psi (x))1.\] For an arbitrary even \(x\), this norm is algebra-valued: the determinant may be complex, corresponding to the even center. It is not yet the real scalar-valued Lipschitz norm, and adjugation is not conjugate transpose.

                                                                                              Restriction therefore gives a homomorphism \(\operatorname {Spin}(Q_{1,3})\to SL_2(\mathbb C)\). Conversely, a determinant-one matrix has adjugate as a two-sided inverse. Its displayed Clifford preimage is an even unit with \(\operatorname {rev}(x)x=1\), so the dimension-four carrier lemma places it in Spin. The written inverse proves both compositions and multiplicativity: \[\operatorname {Spin}(Q_{1,3})\simeq SL_2(\mathbb C).\]

                                                                                              The source indices require translation. [lawson2016spin, I.3, Theorem 3.7, pp. 23--24] use \(v^2=-q(v)\) and give the even-algebra reduction \[\operatorname {Cl}^{0}_{3,1}\simeq \operatorname {Cl}_{2,1}.\] Their base entries and recurrence then give \[\operatorname {Cl}_{2,1}\simeq M_2(\mathbb C)\] [lawson2016spin, I.4, (4.0) and Theorem 4.1, p. 25].

                                                                                              Gallier uses the opposite indexing. The positive-square \(A_j\) exhibit \(\operatorname {Cl}_{3,0}\). [gallier2014clifford, Example 1.3, p. 33] records the matrix base entries, while [gallier2014clifford, Lemma 1.15, p. 34] supplies the recurrence. Together they give \[\operatorname {Cl}_{3,0} \simeq \operatorname {Cl}_{0,1}\otimes \operatorname {Cl}_{2,0} \simeq M_2(\mathbb C).\]

                                                                                              [porteous1995clifford, Chapter 17, Proposition 17.5, pp. 151--152] identifies his norm-one subgroup \(\operatorname {Spin}^{+}(1,3)\) with \(SL_2(\mathbb C)\). He computes reversal as adjugation. His broader mixed-sign carrier permits norm \(\pm 1\), and his displayed axes are not the Pauli axes fixed above.

                                                                                              Here the even center is \(\mathbb R[I]\simeq \mathbb C\), with no nonzero complementary central idempotents. This contrasts with the split compact center \(\mathbb R\oplus \mathbb R\), although both even algebras have real dimension eight. The full algebra \(\mathcal {C}\kern -2pt\ell _{1,3}\simeq M_2(\mathbb H)\) in Example [fcap-0026] is a different algebra. The vector-action image remains the spinor-norm kernel from Theorem [fcap-0023]; no topological component or concrete gamma-map claim is made.

                                                                                              Proposition. The reverse norm descends through the Lipschitz action [fcap-002D]

                                                                                                Let \(K\) be a field of characteristic different from two, let \(V\) be a positive-dimensional finite-dimensional \(K\)-space, and let \(Q\) be nondegenerate. Write \(\Gamma (Q)\) for the vector-generated Lipschitz group, and \(\tau _Q:\Gamma (Q)\to O(V,Q)\) for its twisted action. For \(x\in \Gamma (Q)\), let \(N_{\mathrm {rev}}(x)\in K^{\times }\) be the unique scalar unit satisfying \(\operatorname {rev}(x)x=N_{\mathrm {rev}}(x)\,1\). Set \(\mathcal {S}_K=K^{\times }/(K^{\times })^2\). The top row is exact, and the square commutes:

                                                                                                The determinant arrow is a separate branch: \(SO(V,Q)=\ker (\det )\). It is not part of a longer exact row after \(O(V,Q)\). Positive dimension supplies an anisotropic vector, so scalar units form the displayed kernel; the Lipschitz action is onto CliffordAlgebra.scalarUnits_injective CliffordAlgebra.ker_lipschitzToOrthogonal CliffordAlgebra.lipschitzToOrthogonal_surjective. The right vertical map is the orthogonal spinor norm, while \(\nu _Q=\nu _Q^O|_{SO(V,Q)}\) is its restriction used in Theorem [fcap-0023]. The square expresses descent through the action, not surjectivity of \(\nu _Q^O\) CliffordAlgebra.orthogonalSpinorNorm_lipschitzToOrthogonal.

                                                                                                If \(Q(v)\) is nonzero, then \[N_{\mathrm {rev}}(\widehat v)=Q(v),\qquad \nu _Q^O(r_v)=[Q(v)]\] CliffordAlgebra.cliffordNorm_unitι CliffordAlgebra.orthogonalSpinorNorm_reflectionOrthogonal. Consequently, for an even product \(x=\widehat v_1\cdots \widehat v_{2k}\) of nonisotropic vector lifts, \[\tau _Q(x)=r_{v_1}\cdots r_{v_{2k}}\in SO(V,Q),\qquad \nu _Q(r_{v_1}\cdots r_{v_{2k}}) =\left [\prod _{i=1}^{2k}Q(v_i)\right ].\] Multiplying a lift by \(c\in K^\times \) changes its reverse norm by \(c^2\), so the square class is independent of the chosen lift. [chevalley1954algebraic, II.3.5--6, pp. 52--53] gives these vector and paired-product values. The scalar exact sequence, reflection factorization, and the same square-scaling law appear in [meinrenken2013clifford, Theorem 3.1, pp. 50--51]. Chevalley's quotient statement assumes positive dimension; Meinrenken works with a finite-dimensional characteristic-zero nondegenerate bilinear space.

                                                                                                If \(e:(V,Q)\simeq (V',Q')\) is an isometry equivalence, then conjugation transport preserves both norms: for \(g\in O(V,Q)\) and \(h\in SO(V,Q)\), \[\nu _{Q'}^O(ege^{-1})=\nu _Q^O(g),\qquad \nu _{Q'}(ehe^{-1})=\nu _Q(h).\] It therefore carries \(\ker \nu _Q\) onto \(\ker \nu _{Q'}\) QuadraticMap.IsometryEquiv.orthogonalSpinorNorm_orthogonalGroupCongr QuadraticMap.IsometryEquiv.spinorNorm_specialOrthogonalGroupCongr kernel-transport source. The induced kernel equivalence also commutes with Spin transport Spin-transport source. These are isometry-equivalence statements; they do not assert scalar-extension or orthogonal-product naturality. This is the norm-square companion to the vector-action square in Proposition [fcap-0029].

                                                                                                Example. The split four-dimensional Spin action is left and inverse-right multiplication [fcap-003Y]

                                                                                                  For \(Q_{2,2}(v)=v_0^2+v_1^2-v_2^2-v_3^2\), the even Clifford algebra is a pair of real matrix algebras. We construct its coordinates to specify which Spin factor acts on each side of a vector. Set \(A=e_0e_1\), \(B=e_0e_2\), \(C=e_1e_2\), and \(I=e_0e_1e_2e_3\). The subalgebra \(H_0=\langle 1,A,B,C\rangle _{\mathbb R}\) has \(A^2=-1\), \(B^2=C^2=1\), and \(AB=-C\). Define \[J=\begin {pmatrix}0&1\\-1&0\end {pmatrix},\quad S=\begin {pmatrix}0&1\\1&0\end {pmatrix},\quad D=\begin {pmatrix}-1&0\\0&1\end {pmatrix}.\] The assignments \(\rho (A)=-J\), \(\rho (B)=D\), \(\rho (C)=S\) satisfy these relations and give a basis of \(M_2(\mathbb R)\) together with the identity. They define an algebra equivalence \(\rho \). The volume element \(I\) is central in the even algebra and \(I^2=1\). The eight even basis monomials give \(\mathcal {C}\kern -2pt\ell ^+(Q_{2,2})=H_0\oplus I H_0\). Hence the map \[\Phi (u+Iw)=\bigl (\rho (u)-\rho (w),\ S(\rho (u)+\rho (w))S\bigr )\] is an algebra equivalence to \(M_2(\mathbb R)\times M_2(\mathbb R)\). For a pair \((P,R)\), its inverse is recovered from \[\rho (u)=\tfrac 12(P+SRS),\qquad \rho (w)=\tfrac 12(SRS-P).\]

                                                                                                  The reversion fixes \(I\) and negates \(A,B,C\). On \(H_0\), this is matrix adjugation, since \(\rho (A), \rho (B),\rho (C)\) are traceless. Conjugation by \(S\) commutes with adjugation, so \[\Phi (\operatorname {rev}(x))= \bigl (\operatorname {adj}(\Phi _1(x)), \operatorname {adj}(\Phi _2(x))\bigr ).\] Consequently \(\operatorname {rev}(x)x=1\) if and only if both component determinants are one. The carrier lemma Lemma [fcap-002J] therefore restricts \(\Phi \), with the displayed inverse, to the actual group \[\operatorname {Spin}(Q_{2,2})\simeq SL_2(\mathbb R)\times SL_2(\mathbb R).\] Porteous's norm-one subgroup is denoted \(\operatorname {Spin}^+\); his split-four entry is a pair of \(Sp_2(\mathbb R)\) factors [porteous1995clifford, Chapter 17, Theorem 17.9 and Table 14, p. 159]. In degree two, \(M^{\mathsf T}JM=(\det M)J\), so these are precisely \(SL_2(\mathbb R)\). The norm-one restriction is essential to that comparison.

                                                                                                  Our pair map has the following six bivector images: \[\begin {aligned} e_0e_1&\longmapsto (-J,J),& e_0e_2&\longmapsto (D,-D),\\ e_0e_3&\longmapsto (-S,S),& e_1e_2&\longmapsto (S,S),\\ e_1e_3&\longmapsto (D,D),& e_2e_3&\longmapsto (-J,-J). \end {aligned}\] In particular \(\Phi (I)=(-1,1)\). These are the specializations of TauCeti's bilinear-generator formula TauCeti.realCliffordTwoTwoEvenEquivMatrixProd_ι. Since the bivectors generate the even algebra, this identifies \(\Phi \) with its concrete even-algebra map and hence identifies the restricted group equivalence TauCeti.realSpinTwoTwoEquivSpecialLinearProd.

                                                                                                  Now encode vectors by \[X(v)=\Phi _1(ve_3)S= \begin {pmatrix}-v_0-v_2&-v_1-v_3\\v_1-v_3&-v_0+v_2\end {pmatrix}.\] The inverse sends \(\begin {pmatrix}a&b\\c&d\end {pmatrix}\) to \((-(a+d)/2,(c-b)/2,(d-a)/2,-(b+c)/2)\). A determinant expansion gives \(\det X(v)=Q_{2,2}(v)\). Thus \(X\) identifies the whole vector space with the determinant quadratic space of real two-by-two matrices TauCeti.realCliffordTwoTwoVectorEquivMatrix_apply TauCeti.realCliffordTwoTwoVectorEquivMatrix_det. Writing \(\Phi (s)=(P,R)\) for a Spin element, the action is \[X(svs^{-1})=P X(v)R^{-1}.\]

                                                                                                  For the proof, \(e_3^2=-1\), and conjugation \(\gamma (x)=-e_3xe_3\) fixes \(H_0\) and negates \(I\). Therefore \[\Phi (\gamma (x))= \bigl (S\Phi _2(x)S,\ S\Phi _1(x)S\bigr ).\] The identities \[e_0e_3=IC,\qquad e_1e_3=-IB,\qquad e_2e_3=-IA\] give the displayed formula for \(X\). Apply \(\Phi _1\) to \((svs^{-1})e_3=s(ve_3)\gamma (s^{-1})\), then multiply on the right by \(S\). Since \(S^2=1\), the result is \(P X(v)R^{-1}\). This proves TauCeti's exact coordinate action TauCeti.realSpinTwoTwoEquivSpecialLinearProd_action.

                                                                                                  The diagram records the two ways to calculate the same action:

                                                                                                  For example, take \(P=\operatorname {diag}(a,a^{-1})\), \(R=1\), where \(a\ne 0\). The two rows of \(X(v)\) are multiplied by \(a\) and \(a^{-1}\). Thus the null cone is exactly the matrices of rank at most one, and its rank-one part is preserved. For \(P=R\), the matrix \(X(e_0)=-1\) is fixed; this diagonal subgroup fixes \(e_0\).

                                                                                                  As in the compact action of Example [fcap-003K], multiplication by a fixed vector makes an odd vector accessible to the even algebra, and conjugation by that vector interchanges its two factors. Here the factors are real matrices, with the explicit \(S\)-conjugations above. This is the even-algebra action transport of [porteous1995clifford, Chapter 16, Proposition 16.9, pp. 143--144] in the stated axes. The construction gives the group and its vector action; its orthogonal image retains the spinor-norm qualification of Theorem [fcap-0023].

                                                                                                  Definition [ca-000J]Definition [ca-001J]Definition [spin-0012]Definition [spin-000O]

                                                                                                  Example. The split three-dimensional Spin action is symmetric matrix congruence [fcap-003X]

                                                                                                    For \(Q_{2,1}(v)=v_0^2+v_1^2-v_2^2\), keep the algebra map \(\Phi :\mathcal {C}\kern -2pt\ell ^+(Q_{2,1})\simeq M_2(\mathbb R)\) of Example [fcap-002I]. Multiplication by the last generator gives symmetric matrix coordinates \[X(v)=\Phi (ve_2)= \begin {pmatrix}-v_2-v_1&v_0\\v_0&-v_2+v_1\end {pmatrix}, \qquad \det X(v)=-Q_{2,1}(v).\] The inverse sends \(\begin {pmatrix}a&b\\b&d\end {pmatrix}\) to \((b,(d-a)/2,-(a+d)/2)\). Thus \(X\) is a real linear equivalence onto the symmetric matrices, with the stated negative determinant form TauCeti.coe_realCliffordTwoOneVectorEquivSymmetric_apply TauCeti.realCliffordTwoOneVectorEquivSymmetric_det. For \(s\in \operatorname {Spin}(Q_{2,1})\) and \(M=\Phi (s)\in SL_2(\mathbb R)\), the vector action becomes \[X(svs^{-1})=M X(v)M^{\mathsf T}.\]

                                                                                                    To prove the formula, write \(A=e_0e_1\), \(B=e_0e_2\), and \(C=e_1e_2\). Since \(e_2^2=-1\), conjugation by \(e_2\) is \(\gamma (x)=-e_2xe_2\). It fixes \(A\) and negates \(B,C\). On their three matrices in Example [fcap-002I], and on the identity, this gives \[\Phi (\gamma (x))=\operatorname {adj}(\Phi (x))^{\mathsf T}.\] Both sides are linear in \(x\), so the basis check proves the equality on the whole even algebra. Moreover, \[(svs^{-1})e_2=s(ve_2)\gamma (s^{-1}).\] The determinant-one equation gives \(\operatorname {adj}(M^{-1})=M\); applying \(\Phi \) proves the action. TauCeti's bilinear-generator formula sends \(A,B,C\) to exactly these three matrices, so its group map and action use this same \(\Phi \) TauCeti.realCliffordTwoOneEvenEquivMatrix_ι TauCeti.realSpinTwoOneEquivSpecialLinear_action.

                                                                                                    For example, let \(M=\operatorname {diag}(a,a^{-1})\) with \(a>0\), and choose its Spin preimage using Example [fcap-002I]. Put \(c=(a^2+a^{-2})/2\) and \(h=(a^2-a^{-2})/2\). The congruence action is \[v_0'=v_0,\qquad v_1'=cv_1+hv_2,\qquad v_2'=hv_1+cv_2.\] Here \(c^2-h^2=1\). The two null coordinates \(v_1+v_2\) and \(v_1-v_2\) are multiplied by \(a^2\) and \(a^{-2}\), respectively. This exhibits the action on both null directions in the chosen coordinates.

                                                                                                    For comparison, the compact quaternion action of Example [fcap-003J] has a complex matrix realization. Distinguish quaternion units \(\mathbf i,\mathbf j,\mathbf k\) from the complex scalar \(i\). The map \[\iota (a+b\mathbf i+c\mathbf j+d\mathbf k)= \begin {pmatrix}a+ib&c+id\\-c+id&a-ib\end {pmatrix}\] preserves multiplication and sends quaternion conjugation to conjugate transpose. Its determinant is \(a^2+b^2+c^2+d^2\), so it identifies the unit quaternions with \(SU(2)\). Indeed a special unitary matrix has the form \(\begin {pmatrix}z&w\\-\bar w&\bar z\end {pmatrix}\) with \(|z|^2+|w|^2=1\), which recovers the four real coordinates. These are Gallier's axes [gallier2014clifford, Section 1.1, pp. 8--9], and the exact embedding and group equivalence in TauCeti Quaternion.toComplexMatrix Quaternion.unitaryEquivSpecialUnitaryGroup.

                                                                                                    Keep \(\eta _3(v)=-v_1\mathbf i+v_0\mathbf j-v_2\mathbf k\) from Example [fcap-003J], and put \(K(v)=i\iota (\eta _3(v))\). It is a traceless Hermitian matrix. Applying \(i\iota \) to the already proved quaternion action gives \[K(svs^{-1})=U K(v)U^*,\qquad U=\iota (\theta (s))\in SU(2),\] where \(U^*\) is conjugate transpose. The composite Spin-to-\(SU(2)\) isomorphism is available in TauCeti TauCeti.realSpinThreeEquivSpecialUnitary. Its action theorem uses the unscaled matrix \(\iota (\eta _3(v))\) TauCeti.realSpinThreeEquivSpecialUnitary_action; multiplication by the central scalar \(i\) gives the displayed \(K\) formula. Thus neither quaternion nor vector axes change. The split formula uses real symmetric matrices and \(SL_2(\mathbb R)\) instead. The fixed-vector transport underlying these formulas is illustrated by [porteous1995clifford, Chapter 16, Proposition 16.9, pp. 143--144]. For the indefinite vector-action image, retain the spinor-norm kernel of Theorem [fcap-0023]; no component or covering-space assertion is needed.

                                                                                                    Definition [spin-000O]Definition [ca-001J]

                                                                                                    Example. The split three-dimensional Spin group is \(SL_2(\mathbb R)\) [fcap-002I]

                                                                                                      For \(Q_{2,1}(x_0,x_1,x_2)=x_0^2+x_1^2-x_2^2\), set \(A=e_0e_1\), \(B=e_0e_2\), and \(C=e_1e_2\). Then \[A^2=-1,\qquad B^2=C^2=1,\qquad AB=-C.\] The assignments \[A\longmapsto \begin {pmatrix}0&1\\-1&0\end {pmatrix},\qquad B\longmapsto \begin {pmatrix}0&1\\1&0\end {pmatrix},\qquad C\longmapsto \begin {pmatrix}-1&0\\0&1\end {pmatrix}\] satisfy these relations, and the images of \(1,A,B,C\) form a basis of \(M_2(\mathbb R)\). They therefore define an algebra equivalence \(\Phi \) with \[\Phi (s+aA+bB+cC)= \begin {pmatrix}s-c&a+b\\-a+b&s+c\end {pmatrix}.\] Reversal negates \(A,B,C\), so it becomes matrix adjugation, and \[N_{\mathrm {rev}}(s+aA+bB+cC) =s^2+a^2-b^2-c^2=\det \Phi (s+aA+bB+cC)\] CliffordAlgebra.map_reverseEven_eq_adjugate_of_finrank_eq_three CliffordAlgebra.reverseEven_mul_eq_one_iff_det_eq_one_of_finrank_eq_three.

                                                                                                      Restriction gives \(\operatorname {Spin}(Q_{2,1})\to SL_2(\mathbb R)\). Conversely, if \(M=(m_{ij})\in SL_2(\mathbb R)\), put \[\begin {aligned} s&=\frac {m_{00}+m_{11}}2,& a&=\frac {m_{01}-m_{10}}2,\\ b&=\frac {m_{01}+m_{10}}2,& c&=\frac {m_{11}-m_{00}}2. \end {aligned}\] Then \(\Phi (s+aA+bB+cC)=M\), and its reverse norm is \(\det M=1\). The carrier lemma puts this inverse value in the actual Spin group; the algebra maps give two-sided multiplicative inverses. Thus \[\operatorname {Spin}(Q_{2,1})\simeq SL_2(\mathbb R).\]

                                                                                                      The source translation matters. Lawson--Michelsohn's convention turns this even algebra into \(\operatorname {Cl}_{0,2}\simeq M_2(\mathbb R)\) via [lawson2016spin, I.3, Theorem 3.7, pp. 23--24; I.4, (4.0), p. 25]. With the reversed index convention, [gallier2014clifford, Example 1.3, p. 33] independently records \(\operatorname {Cl}_{2,0}\simeq M_2(\mathbb R)\), the same real matrix base algebra. Their indefinite Pin/Spin carrier conventions allow factors of quadratic value \(\pm 1\) [lawson2016spin, I.2, (2.24)--(2.25), p. 18] [gallier2014clifford, Section 1.5, Definition 1.6, p. 31]. We use their algebra identifications but impose the displayed reverse-norm-one equation. For example, \(e_0e_2\) has reverse norm \(-1\) and maps to a determinant \(-1\) matrix, so it is excluded here.

                                                                                                      This split form has polarization \(W=\mathbb R(e_0+e_2)\), \(W'=\mathbb R((e_0-e_2)/4)\), and line \(\mathbb R e_1\): the unhalved polar pairing of the displayed generators is \(1\), and the line coordinate squares to \(Q_{2,1}\). TauCeti's polarized dimension-three theorem therefore gives an independent abstract group equivalence with \(SL_2(\mathbb R)\) TauCeti.exists_spinGroup_mulEquiv_specialLinearGroup_and_spinRep_equiv_stdSLRep_of_finrank_eq_three. The concrete map \(\Phi \) above is not asserted to be definitionally that map, and the theorem's representation refinement belongs to the later module packet. Likewise, the vector-action image is the spinor-norm kernel from Theorem [fcap-0023], not all of \(SO(2,1)\). No component or covering-space claim is made.

                                                                                                      Related

                                                                                                        Lemma. Determinant parity detects the even lift [lawson2016spin, I.2, Theorems 2.7 and 2.9, pp. 17--19] [fcap-001A]
                                                                                                        det_reflectionmem_even_of_det_pinToOrthogonal_eq_one
                                                                                                        L∃∀N

                                                                                                          Let \(R\) be a commutative ring in which \(2\) is invertible, let \(M\) be a finite free \(R\)-module, and let \(Q\) be a quadratic form on \(M\). A reflection in a vector of invertible quadratic value has determinant \(-1\). Therefore a product of \(r\) such reflections has determinant \[(-1)^r.\] In particular, every product of an even number of reflections belongs to \(SO(M,Q)\).

                                                                                                          Lawson--Michelsohn state this parity argument for quadratic vector spaces over a field. The finite-free commutative-ring statement above is the formalized extension: its determinant calculation uses freeness and finiteness, while invertibility of \(2\) identifies the fixed part of the grading involution with the even subalgebra.

                                                                                                          The Clifford lift remembers this parity. If \(p\in \operatorname {Pin}(M,Q)\) and its orthogonal action has determinant \(1\), then \(p\) lies in the even Clifford subalgebra. Hence \(p\) is a Spin element. Thus any Pin lift of a special orthogonal transformation is automatically even.

                                                                                                          Proof. 

                                                                                                            Multiplicativity of the determinant gives the first assertion from \(\det (\rho _v)=-1\). For the second, the grading involution of a Lipschitz element is its determinant sign times that element. If the determinant is \(1\), the involution fixes the Pin element. Because \(2\) is invertible, the fixed submodule of the grading involution is precisely the even Clifford subalgebra.

                                                                                                            Remark. Reverse norm signs and the Spin carrier [fcap-0028]

                                                                                                              Let \(R\) be a commutative ring, let \(M\) be an \(R\)-module, and let \(Q\) be a quadratic form on \(M\). Write \(\widehat v=\iota _Q(v)\) for a Clifford generator. Before imposing any invertibility condition, consider the two algebra-valued norm expressions \(N_{\mathrm {rev}}(x)=\operatorname {rev}(x)x\) and \(N_*(x)=x^*x\), where \(x^*=\operatorname {rev}(\alpha (x))\). Identifying a scalar with its image in the Clifford algebra gives \[\begin {aligned} N_{\mathrm {rev}}(\widehat v)&=Q(v), &N_*(\widehat v)&=-Q(v),\\ N_{\mathrm {rev}}(\widehat u\widehat v) &=\widehat v\widehat u\widehat u\widehat v =Q(u)Q(v), &N_*(\widehat u\widehat v)&=Q(u)Q(v). \end {aligned}\] Thus the two signs differ on one generator and agree on a product of two. More generally, reversal gives the product of the quadratic values on every vector word CliffordAlgebra.reverse_prod_map_ι_mul_prod_map_ι, and the two norm expressions agree on every even Clifford element CliffordAlgebra.star_mul_self_eq_reverse_mul_self_of_mem_even.

                                                                                                              For a Clifford unit \(x\), membership in the even-unitary carrier is equivalent to evenness together with \(N_{\mathrm {rev}}(x)=1\) CliffordAlgebra.evenUnitaryGroup.mem_iff_reverse_mul_self_eq_one. Those two conditions do not establish Lipschitz membership, which must be retained in the Spin criterion. Precisely, \[\operatorname {im}\bigl (\operatorname {Spin}(Q)\longrightarrow \operatorname {Cl}(Q)^\times \bigr ) =\operatorname {Lipschitz}(Q)\cap \operatorname {EvenUnitary}(Q)\] CliffordAlgebra.range_spinGroup_toUnits. Consequently, if \(Q(u)Q(v)=1\), then \(\widehat u\widehat v\) is an even product of Lipschitz vector units with reverse norm one, hence a Spin element CliffordAlgebra.ι_mul_ι_mem_spinGroup_of_norm_mul_norm_eq_one. This is an unquotiented scalar calculation. The passage to square classes, including the odd reflection sign and its cancellation on even products, is recorded separately in Theorem [fcap-0023].

                                                                                                              Chevalley obtains the same norm from what he calls the main antiautomorphism and records \(\lambda (v)=Q(v)\) and the paired values \(Q(u)Q(v)\) [chevalley1954algebraic, II.3.5--6, pp. 52--53]. His symbol \(\alpha \) in that passage denotes reversal, whereas \(\alpha \) in Lemma [fcap-0021] denotes the grading involution. Meinrenken calls reversal transposition, writes \(N(x)=x^\top x\), and defines Spin as its norm-one subgroup inside the special Clifford group [meinrenken2013clifford, Sections 2.2.6 and 3.1.1--2, pp. 34, 49--51]. His convention has \(Q(v)=B(v,v)\), so his \(B\) is the half-polar form \(b_Q\) of Convention [fcap-0027]. Both sources work in narrower finite-dimensional field settings; Meinrenken here assumes characteristic zero and a nondegenerate form. The formal identities linked above hold under the commutative-ring and module hypotheses stated here.