Lemma. Twisted Clifford conjugation is a reflection [lawson2016spin, I.2, Proposition 2.2 and (2.8), p. 13; (2.11)--(2.12), p. 14] [fcap-000A]
✍️source

    Let \(\alpha \) denote the grading involution of \(\mathcal {C}\kern -2pt\ell (Q)\). For \(Q(v)\ne 0\), the Clifford generator \(\iota (v)\) is invertible with \[\iota (v)^{-1}=Q(v)^{-1}\iota (v).\] Its twisted adjoint action on a generator is the reflection in Definition [fcap-0009]: \[\alpha (\iota (v))\,\iota (w)\,\iota (v)^{-1}=\iota (\rho _v(w)).\]

    Proof. 

      The generator-square rule CliffordAlgebra.ι_sq_scalar and the anticommutator rule CliffordAlgebra.ι_mul_ι_add_swap give \[\iota (v)\iota (w)+\iota (w)\iota (v)=B_Q(v,w).\] Since \(\alpha (\iota (v))=-\iota (v)\) and \(\iota (v)^2=Q(v)\), substitution yields \[-\iota (v)\iota (w)\frac {\iota (v)}{Q(v)} =\iota (w)-\frac {B_Q(v,w)}{Q(v)}\iota (v) =\iota (\rho _v(w)).\] The ordinary adjoint differs by the leading minus sign; the twisted adjoint is the action that gives the reflection itself.

      References

        Reference. Spin geometry (pms-38) [lawson2016spin]

        • 2016
        • H. Blaine Lawson, Marie-Louise Michelsohn
        @book{lawson2016spin,
 title = {Spin Geometry (Pms-38)},
 author = {Lawson, H. Blaine and Michelsohn, Marie-Louise},
 date = {2016},
 volume = {38},
 publisher = {{Princeton university press}}
}

        Context

          Reflections and square-normalized Clifford lifts [fcap-0007]

            A nonisotropic vector acts on the generating space by a reflection through twisted Clifford conjugation. Normalizing such vectors gives elements of Pin, while determinant parity detects the even products that belong to Spin. The cards pass from local lifts to reflection generation, Pin surjectivity, and finally Spin surjectivity onto the special orthogonal group.

            § [ca-0001]

            Convention. Quadratic-form sign [lawson2016spin, I.1, (1.3)--(1.4), p. 8] [fcap-0008]

              Lawson and Michelsohn write \[v^2=-q(v)1, \qquad vw+wv=-2q(v,w),\] where \(2q(v,w)=q(v+w)-q(v)-q(w)\). Mathlib and TauCeti instead use a quadratic form \(Q\) with \[\iota (v)^2=Q(v)1.\] The conventions agree after setting \(Q=-q\). The orthogonal group and its reflections are unchanged by this global sign reversal. A vector with \(q(v)=1\) therefore has \(Q(v)=-1\) in the convention used below. Mathlib's generator-square rule CliffordAlgebra.ι_sq_scalar uses this \(Q\)-convention.

              Definition. Reflection in a nonisotropic vector [lawson2016spin, I.2, (2.12), p. 14] [fcap-0009]
              reflection
              L∃∀N

                Let \(F\) be a field of characteristic different from \(2\), let \(Q\) be a quadratic form on an \(F\)-vector space \(V\), and write \[B_Q(x,y)=Q(x+y)-Q(x)-Q(y)\] for its polar form. If \(Q(v)\ne 0\), the reflection with normal vector \(v\) is \[\rho _v(w)=w-\frac {B_Q(v,w)}{Q(v)}v.\] It fixes \(v^\perp \) pointwise, sends \(v\) to \(-v\), and preserves \(Q\). Multiplying \(v\) by a nonzero scalar does not change \(\rho _v\).

                Lemma. Twisted Clifford conjugation is a reflection [lawson2016spin, I.2, Proposition 2.2 and (2.8), p. 13; (2.11)--(2.12), p. 14] [fcap-000A]
                ✍️source

                  Let \(\alpha \) denote the grading involution of \(\mathcal {C}\kern -2pt\ell (Q)\). For \(Q(v)\ne 0\), the Clifford generator \(\iota (v)\) is invertible with \[\iota (v)^{-1}=Q(v)^{-1}\iota (v).\] Its twisted adjoint action on a generator is the reflection in Definition [fcap-0009]: \[\alpha (\iota (v))\,\iota (w)\,\iota (v)^{-1}=\iota (\rho _v(w)).\]

                  Proof. 

                    The generator-square rule CliffordAlgebra.ι_sq_scalar and the anticommutator rule CliffordAlgebra.ι_mul_ι_add_swap give \[\iota (v)\iota (w)+\iota (w)\iota (v)=B_Q(v,w).\] Since \(\alpha (\iota (v))=-\iota (v)\) and \(\iota (v)^2=Q(v)\), substitution yields \[-\iota (v)\iota (w)\frac {\iota (v)}{Q(v)} =\iota (w)-\frac {B_Q(v,w)}{Q(v)}\iota (v) =\iota (\rho _v(w)).\] The ordinary adjoint differs by the leading minus sign; the twisted adjoint is the action that gives the reflection itself.

                    Lemma. Square-normalized Pin lift [lawson2016spin, I.2, Definition 2.3 and (2.26), pp. 14, 18] [fcap-000B]
                    reflection_mem_range_pinToOrthogonal_of_isSquare
                    L∃∀N

                      Lawson--Michelsohn make this product-and-scaling argument for a finite-dimensional quadratic vector space over a field. The statement below is TauCeti's extension to a quadratic module over a commutative ring. It assumes that \(2\) and \(Q(v)\) are invertible.

                      Let \(R\) be a commutative ring, let \(Q\) be a quadratic form on an \(R\)-module \(M\), and suppose \(2\) and \(Q(v)\) are invertible. If there is a scalar \(c\) such that \[c^2=-Q(v)^{-1},\] then \(Q(cv)=-1\). The normalized Clifford generator \(\iota (cv)\) belongs to the Pin group and its twisted adjoint action is \(\rho _v\), because \(\rho _{cv}=\rho _v\). Consequently \[\rho _v\in \operatorname {range}(\operatorname {pinToOrthogonal}).\] Equivalently, the required hypothesis is that \(-Q(v)^{-1}\) is a square. The conclusion is existential: it asserts that a Pin lift exists, not that a canonical square root has been chosen.

                      Theorem. Paired reflections have a product-square Spin lift [lawson2016spin, I.2, (2.24)--(2.26), p. 18] [fcap-000C]
                      reflection_mul_reflection_mem_range_spinToOrthogonal_of_isSquare
                      L∃∀N

                        The cited product formulas are stated for a finite-dimensional quadratic vector space over a field. TauCeti packages the same scaling and Clifford-product calculation over the commutative-ring and module hypotheses inherited from Lemma [fcap-000B].

                        Let \(R\), \(M\), and \(Q\) be as in Lemma [fcap-000B]. Suppose \(Q(v)\), \(Q(w)\), and \(2\) are invertible. If there is a scalar \(c\) such that \[c^2=Q(v)^{-1}Q(w)^{-1},\] then \[Q(cv)Q(w)=1.\] Set \(x=\iota (cv)\iota (w)\). The element \(x\) is a product of invertible Clifford generators, and \[x^{*}x =\iota (w)\iota (cv)^2\iota (w) =Q(cv)Q(w)=1.\] Thus \(x\) is a unitary element of the Lipschitz group. It has even degree, so it belongs to the Spin group. Its twisted adjoint action is the ordered product of reflections, and therefore \[\rho _v\rho _w\in \operatorname {range}(\operatorname {spinToOrthogonal}).\]

                        Proof. 

                          The displayed square identity gives \(Q(cv)Q(w)=c^2Q(v)Q(w)=1\). Each generator is a Clifford unit and lies in the Lipschitz group, while the star calculation above establishes the unitary condition. The twisted adjoint is multiplicative on Clifford units, and scalar rescaling does not change a reflection. Hence the action of \(x\) is \(\rho _{cv}\rho _w=\rho _v\rho _w\); its even degree supplies the remaining Spin condition.

                          Equations (2.24)--(2.26) give the product descriptions and scaling invariance used here. The product-square condition is sharper than asking for separate normalizations of \(v\) and \(w\): one scalar normalizes the product even when neither vector has been normalized separately.

                          Example. A Euclidean unit normal [lawson2016spin, I.2, (2.12), p. 14; (2.24)--(2.26), p. 18] [fcap-000D]

                            Let \(V=\mathbb {R}^n\) with Euclidean inner product and use the sign convention \[Q(x)=-\langle x,x\rangle .\] For a unit vector \(v\), one has \(Q(v)=-1\); thus \(c=1\) satisfies the square condition in Lemma [fcap-000B]. The Clifford generator \(\iota (v)\) is already Pin-normalized, and its action is the familiar hyperplane reflection \[\rho _v(w)=w-2\langle v,w\rangle v.\] For orthonormal \(v,w\), the even product \(\iota (v)\iota (w)\) lies in Spin and lifts the composition \(\rho _v\rho _w\). This is the Euclidean specialization of the general Pin and paired-Spin lifting statements in Lemma [fcap-000B] and Theorem [fcap-000C].

                            Remark. From individual lifts to generation [lawson2016spin, I.2, Proposition 2.2, Definition 2.3, and (2.24)--(2.26), pp. 13--18] [fcap-000E]

                              Lawson and Michelsohn supply the twisted-adjoint reflection formula, the definitions of Pin and Spin, the description by products of normalized vectors, and the square-root obstruction to normalization. The square-witness statements in Lemma [fcap-000B] and Theorem [fcap-000C] isolate the precise algebraic hypotheses under which one or two reflections lift.

                              An individual lift does not by itself show that all orthogonal transformations lift. That global conclusion requires finite dimension, nondegeneracy, and the Cartan--Dieudonne factorization developed next.

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

                                One reflection can enlarge the fixed subspace of an orthogonal transformation. Iterating this correction proves that reflections generate the orthogonal group. Once each reflection has a Pin lift, generation gives the Pin cover; determinant parity then restricts that cover to Spin over the special orthogonal group.

                                Lemma. Fixed-subspace correction by reflections [cartan1981theory, Section 10, pp. 10--12] [fcap-000V]
                                exists_mem_subgroup_mul_eqOn_sup_span_singleton_of_reflection_mem
                                L∃∀N

                                  Cartan proves reflection factorization by an induction that enlarges the fixed subspace. The subgroup-valued statement below is a formalized TauCeti lemma extracted from that method. Cartan's one- or two-reflection correction is repackaged as an element of \(H\) acting trivially on \(W+Kx\).

                                  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 TauCeti.CliffordAlgebra.spinToSpecialOrthogonal, and its action on vectors is the usual Spin action by TauCeti.CliffordAlgebra.coe_spinToSpecialOrthogonal_apply.

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

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

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

                                                    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)\), 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 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)\), 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, 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.

                                                            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. No topology on the groups is used.

                                                              For real quadratic spaces of arbitrary signature, Gallier proves that the two maps \[\operatorname {Pin}(p,q)\longrightarrow O(p,q),\qquad \operatorname {Spin}(p,q)\longrightarrow SO(p,q)\] are topological double covers [gallier2014clifford, Section 1.8, Proposition 1.21, pp. 39--40].

                                                              Gallier then treats the compact groups: \(\operatorname {Spin}(n)\) is path-connected for \(n\geq 2\), and for \(n\geq 3\) it is simply connected and hence the universal cover of \(SO(n)\) [gallier2014clifford, Section 1.8, pp. 40--42]. These claims are not being extended here to arbitrary signature. Kostant identifies the differential of the complex Spin cover with the quadratic Clifford Lie algebra [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287]. Those conclusions require topological or Lie-theoretic structure not supplied by an abstract group extension. They are not asserted by the four cards above.

                                                              Related

                                                                Definition. Reflection in a nonisotropic vector [lawson2016spin, I.2, (2.12), p. 14] [fcap-0009]
                                                                reflection
                                                                L∃∀N

                                                                  Let \(F\) be a field of characteristic different from \(2\), let \(Q\) be a quadratic form on an \(F\)-vector space \(V\), and write \[B_Q(x,y)=Q(x+y)-Q(x)-Q(y)\] for its polar form. If \(Q(v)\ne 0\), the reflection with normal vector \(v\) is \[\rho _v(w)=w-\frac {B_Q(v,w)}{Q(v)}v.\] It fixes \(v^\perp \) pointwise, sends \(v\) to \(-v\), and preserves \(Q\). Multiplying \(v\) by a nonzero scalar does not change \(\rho _v\).