Proposition. The central sign determines descent to the special orthogonal group [fcap-003M]
✍️source

    Keep the hypotheses and notation of Theorem [fcap-003L], and let \(q:G\to SO(n)\) be the vector action. The integrated representation \(R\) factors through a smooth representation \(\overline R\) of \(SO(n)\) precisely when \[R(-1)=\operatorname {Id}_S.\] Equivalently, let \(J\in \mathfrak {so}(n)\) send \(e_1\mapsto -e_2\), \(e_2\mapsto e_1\), and vanish on the remaining coordinate vectors. Then the descent condition is \[\exp \bigl (2\pi r(J)\bigr )=\operatorname {Id}_S.\]

    Proof. 

      The covering Proposition [fcap-0039] has kernel \(\{1,-1\}\). A factorization forces \(R(-1)=\overline R(1)=\operatorname {Id}_S\). Conversely, under that condition set \(\overline R(q(g))=R(g)\). Any two lifts differ by \(1\) or \(-1\), so the value is independent of the lift. Surjectivity of \(q\) proves both the homomorphism law and uniqueness of \(\overline R\). The differential of \(q\) is an isomorphism by Proposition [fcap-0037]; its local smooth inverse sections express \(\overline R\) locally as \(R\) composed with a smooth section. Hence the descended representation is smooth. Finally, Example [fcap-0038] gives \[\exp \bigl (2\pi b(J)\bigr )=-1,\] so exponential naturality identifies \(R(-1)\) with the displayed matrix exponential.

      This criterion compares the integrated action with Clifford modules. Suppose \[f:\mathcal {C}\kern -2pt\ell ^0(Q_n^+)\longrightarrow \operatorname {End}_F(S)\] is a unital real-algebra homomorphism from the even Clifford algebra. Its restriction \(R_f(g)=f(g)\) takes Spin to invertible operators, with inverse \(f(g^{-1})\). Finite-dimensional linearity makes this restriction smooth. Since \(b(A)\) is even, the exponential power series stays inside \(\mathcal {C}\kern -2pt\ell ^0(Q_n^+)\) and gives \[R_f\bigl (\exp (t b(A))\bigr ) =\exp \bigl (t f(b(A))\bigr ).\] Since \(f\) preserves commutators, \(r(A)=f(b(A))\) is a Lie-algebra action. Consequently \(d(R_f)_1(b(A))=f(b(A))\). The uniqueness in Theorem [fcap-003L] identifies \(R_f\) with the integrated action for \(r(A)=f(b(A))\); it is an equality on the chosen module, not merely an unspecified representation equivalence.

      Unitality gives \(R_f(-1)=-\operatorname {Id}_S\). Thus a nonzero such module does not descend to \(SO(n)\). This includes the complex spin and half-spin modules: they are restrictions of modules for the complexified even Clifford algebra, as described in [meinrenken2013clifford, Section 3.7.5, pp. 80--81]. No extension of a half-spin module to the full Clifford algebra is needed. The central scalar \(-1\) is fixed by the even-algebra sign comparison in Proposition [fcap-0039], so this obstruction is unchanged by the two Clifford sign conventions.

      The same calculation shows why tensor constructions can descend. On \(S\otimes _F S\) the central element acts by \((-\operatorname {Id})\otimes (-\operatorname {Id})=\operatorname {Id}\); on \(\operatorname {End}_F(S)\) its conjugation action is also the identity. Both actions therefore factor through \(SO(n)\). Differentiating their defining group actions gives, respectively, \[\begin {aligned} A\cdot (s\otimes t)&=r(A)s\otimes t+s\otimes r(A)t,\\ A\cdot T&=r(A)T-Tr(A). \end {aligned}\] The tensor formula agrees with [fulton2004representation, Section 8.1, equation (8.12), p. 110]. Descent concerns the central action of the whole group, even though these differentiated formulas use only its Lie algebra.

      For an action of the full real Clifford algebra, TauCeti's AlgHom.lieMap_realCliffordSpinSmoothHom_eq identifies its differentiated smooth restriction with the quadratic Clifford action. The declaration uses the closed Spin range in Clifford units and its Lie-algebra coordinates; the natural carrier equivalence transports the action back to \(G\). Its input is a full-Clifford algebra homomorphism into a finite-dimensional normed real algebra. It does not state the even-module extension or the descent criterion proved here.

      The actual orthogonal differential fixes its coordinates as well. Let \(X\in T_1\operatorname {Spin}(n)\) and put \(A=d_1q(X)\), expressed as a skew-symmetric matrix. With the normalized \(b\) from Proposition [fcap-0037], the refined identity is \[d(R_f)_1(X)=f\bigl (b(A)\bigr ) =f\bigl (\eta (\kappa ^{-1}(A))\bigr ).\] AlgHom.unitsLieAlgebraLieEquiv_lieMap_realCliffordSpinSmoothHom_eq_bivectorExterior proves this after the canonical identification of the target units Lie algebra with its ambient algebra. Its \(A\) comes from the differential of the actual Spin projection, so the formula has the normalization already checked in Proposition [fcap-0037]. The input remains a homomorphism from the full \(\mathcal {C}\kern -2pt\ell (Q_n^+)\) into a finite-dimensional normed real algebra. It supplies the differential comparison for that restriction; the integration, even-only and half-spin cases, and central-sign descent argument retain their separate proofs above and in Theorem [fcap-003L].

      References

        Reference. Clifford algebras and lie theory [meinrenken2013clifford]

        • 2013
        • Eckhard Meinrenken
        @book{meinrenken2013clifford,
 title = {Clifford algebras and Lie theory},
 author = {Meinrenken, Eckhard},
 year = {2013},
 volume = {58},
 publisher = {Springer}
}

        Reference. Representation theory: A first course [fulton2004representation]

        • 2004
        • William Fulton, Joe Harris
        @book{fulton2004representation,
 title = {Representation theory: a first course},
 author = {Fulton, William and Harris, Joe},
 year = {2004},
 publisher = {Springer}
}

        Context

          Differentiating and integrating Spin representations [fcap-001Q]

            The quadratic Clifford construction in the preceding section is algebraic. A different bridge starts from a smooth homomorphism of Lie groups and differentiates it at the identity. The concrete Spin calculation identifies this differential with the normalized quadratic lift. For compact \(\operatorname {Spin}(n)\), \(n\geq 3\), simple connectedness then gives the reverse construction: integration of a Lie-algebra representation. Its action on the covering kernel decides whether it also represents \(SO(n)\).

            Definition. The differential of a smooth homomorphism [liu2016lie, Section 2.1, p. 9] [fcap-001R]

              Let \(G\) and \(H\) be finite-dimensional real Lie groups, with identities \(e_G\) and \(e_H\), and let \(\phi :G\to H\) be a smooth group homomorphism. Their Lie algebras are the tangent spaces \[\mathfrak g=T_{e_G}G, \qquad \mathfrak h=T_{e_H}H.\] The differential of \(\phi \) at the identity is the linear map \[\operatorname {Lie}(\phi )=d\phi _{e_G}: \mathfrak g\longrightarrow \mathfrak h.\] No connectedness or simply-connectedness hypothesis is needed to define this map. Those hypotheses enter the converse problem of integrating a Lie-algebra homomorphism, not the differentiation of a given smooth homomorphism.

              For \(X\in \mathfrak g\), let \(\widetilde X\) be its left-invariant vector field, \[\widetilde X_g=d(L_g)_{e_G}X.\] The homomorphism identity \(\phi \circ L_g=L_{\phi (g)}\circ \phi \) gives \[d\phi _g(\widetilde X_g) =\widetilde {\operatorname {Lie}(\phi )(X)}_{\phi (g)}.\] Thus differentiation at the identity and transport by left translation are two descriptions of the same infinitesimal map.

              Lemma. The differential preserves the Lie bracket [liu2016lie, Section 2.1, p. 9] [fcap-001S]

                In the setting of Definition [fcap-001R], the differential is a Lie-algebra homomorphism: \[\operatorname {Lie}(\phi )([X,Y]) =[\operatorname {Lie}(\phi )(X), \operatorname {Lie}(\phi )(Y)].\] Indeed, the left-invariant fields \(\widetilde X\) and \(\widetilde Y\) are \(\phi \)-related to the left-invariant fields determined by their images. Brackets of related vector fields are again related. Evaluating that relation at \(e_G\) gives the displayed identity.

                This argument is local at the identity. In particular, bracket preservation does not require \(G\) to be connected or simply connected.

                Theorem. The Lie functor [liu2016lie, Section 2.2, p. 10] [fcap-001T]

                  Differentiation at the identity is functorial. For smooth homomorphisms \(G\xrightarrow {\phi }H\xrightarrow {\psi }K\), the chain rule gives \[\operatorname {Lie}(\operatorname {id}_G) =\operatorname {id}_{\mathfrak g}, \qquad \operatorname {Lie}(\psi \circ \phi ) =\operatorname {Lie}(\psi )\circ \operatorname {Lie}(\phi ).\] Together with Lemma [fcap-001S], this defines a functor from Lie groups and smooth homomorphisms to Lie algebras and Lie-algebra homomorphisms.

                  The stronger correspondence between simply connected Lie groups and Lie algebras concerns existence and uniqueness in the reverse direction. It is not a hypothesis of these functor laws.

                  Theorem. Naturality of the exponential [liu2016lie, Section 2.4, pp. 12--13] [fcap-001U]

                    Let \(\phi :G\to H\) be a smooth Lie-group homomorphism. For every \(X\in \mathfrak g\), \[\phi (\exp _G X) =\exp _H\bigl (\operatorname {Lie}(\phi )(X)\bigr ).\] Equivalently, the square

                    commutes.

                    Proof. 

                      The curve \(t\mapsto \phi (\exp _G(tX))\) is a one-parameter subgroup of \(H\). Its tangent vector at \(t=0\) is \(\operatorname {Lie}(\phi )(X)\). The curve \(t\mapsto \exp _H(t\operatorname {Lie}(\phi )(X))\) has the same property and the same tangent vector. Uniqueness of the one-parameter subgroup with a given tangent vector identifies the curves; setting \(t=1\) proves the formula.

                      Example. Differentiating a matrix representation [liu2016lie, Sections 2.1 and 2.4, pp. 9, 12] [fcap-001V]

                        Let \(V\) be a finite-dimensional real vector space and let \[\rho :G\longrightarrow \operatorname {GL}(V)\] be a smooth representation. Its differential is a Lie-algebra representation \[d\rho _{e_G}:\mathfrak g\longrightarrow \mathfrak {gl}(V).\] Naturality of the exponential becomes \[\rho (\exp _G X)=\exp \bigl (d\rho _{e_G}(X)\bigr ),\] where the exponential on the right is the ordinary matrix exponential. For example, for the determinant homomorphism \(\det :\operatorname {GL}_n(\mathbb R)\to \mathbb R^\times \), \[d(\det )_I(A)=\operatorname {tr}(A).\]

                        Remark. Why explicit smoothness changes the roadmap [liu2016lie, Sections 2.1--2.4 and 2.8, pp. 9--13, 19--20]; [isaev2018theory, Section 3.1.2, pp. 106--107] [fcap-001W]

                          The constructions in Definition [fcap-001R]--Example [fcap-001V] start with a smooth homomorphism. Their tangent map, bracket law, functor laws, and exponential naturality therefore do not require a theorem that upgrades a continuous homomorphism to a smooth one. The generic theorem does not invoke the closed-subgroup theorem; that theorem belongs to the later specialization to concrete matrix subgroups. This is the dependency split recorded in TauCetiRoadmap PR 224.

                          The exponential input is separate from the tangent and bracket input. Likewise, the Baker--Campbell--Hausdorff calculation can first be made in a matrix or general-linear group; using it inside a particular closed matrix subgroup additionally requires the subgroup's Lie structure. Liu describes the local exponential and BCH coordinates, while Isaev--Rubakov give the matrix Campbell--Hausdorff calculation.

                          Tau Ceti's generic interface now defines the Lie map of a bundled smooth monoid morphism between finite-dimensional real Lie groups lieMap. It proves the identity and composition laws lieMap_id, lieMap_comp, and exponential naturality map_lieExp. These declarations act on left-invariant derivations and require the corresponding smooth Lie-group structures.

                          The generic interface does not by itself identify the differential of \(\operatorname {Spin}(Q)\to SO(Q)\) inside the vector-generated Clifford carrier. The closed-subgroup realization, tangent calculation, and quadratic-lift comparison are supplied in Proposition [fcap-0037]. Thus the generic Lie functor and the Clifford calculation retain distinct hypotheses and meet only after the actual group structure has been established.

                          Proposition. The differential of the actual Spin action is the quadratic lift [fcap-0037]

                            Let \(V\) be a positive-dimensional finite-dimensional real vector space, and let \(Q\) be nondegenerate. Give \(\mathcal {C}\kern -2pt\ell (Q)\) its ordinary finite-dimensional topology. Inside \(\mathcal {C}\kern -2pt\ell (Q)^\times \), evenness, reverse norm one, and normalization of the embedded vector subspace are closed conditions and define a subgroup. This subgroup is the actual vector-generated \(\operatorname {Spin}(Q)\). Indeed, for any element \(x\) satisfying them, its twisted action lies in \(O(Q)\). Cartan--Dieudonne supplies a vector product \(u\) with the same twisted action. For \(z=u^{-1}x\), \[\alpha (z)\iota (v)=\iota (v)z\qquad (v\in V).\] Graded centrality makes \(z\) a nonzero scalar; no parity of \(u\) has been assumed in this step. If \(Q(w)\ne 0\), every nonzero scalar \(c\) is the two-vector product \[\iota (w)\,\iota \left (\frac {c}{Q(w)}w\right )=c1.\] Thus \(x\) is vector-generated, and its stated evenness and norm place it in Spin. The reverse inclusion is immediate from the carrier definition. The closed-subgroup theorem now gives this concrete Spin group its finite-dimensional real Lie-group structure.

                            For \(A\in \mathfrak {so}(V,B_Q)\), let \(b(A)\) be the normalized quadratic Clifford lift of Theorem [fcap-000R]. For every \(t\in \mathbb R\), \[g_A(t)=\exp \bigl (t b(A)\bigr )\in \operatorname {Spin}(Q), \qquad g_A(t)\,\iota (v)\,g_A(t)^{-1} =\iota \bigl (\exp (tA)v\bigr ).\] Indeed, reversal sends \(b(A)\) to \(-b(A)\), so the exponential is even and has reverse norm one. The commutator identity \([b(A),\iota (v)]=\iota (Av)\) gives the displayed conjugation formula by the exponential series. Hence \(g_A(t)\) satisfies the three closed conditions above and belongs to the actual Spin group.

                            The tangent Lie algebra at \(1\) is exactly the image of \(b\). One inclusion is supplied by the curves \(g_A\). Conversely, let \(X\) be tangent at \(1\). Differentiating evenness, reverse norm one, and vector normalization gives \[X\text { even},\qquad \operatorname {rev}(X)=-X, \qquad [X,\iota (V)]\subseteq \iota (V).\] Write \([X,\iota (v)]=\iota (Av)\). Differentiating preservation of \(Q\) makes \(A\) skew-adjoint. Then \(X-b(A)\) is even and commutes with every vector, so it is scalar; reverse antisymmetry forces that real scalar to vanish. Therefore \[T_1\operatorname {Spin}(Q)=b\bigl (\mathfrak {so}(V,B_Q)\bigr ), \qquad d_1(\operatorname {spinVectorAction})\bigl (b(A)\bigr )=A.\] This is the genuine differential statement whose algebraic commutator precursor appears in Theorem [fcap-000R] and whose polar-dual coordinate formula is Theorem [fcap-001Z].

                            If \(\pi :\mathcal {C}\kern -2pt\ell (Q)\to \operatorname {End}_{\mathbb R}(S)\) is a finite-dimensional real Clifford module, continuity of the power series gives \[\pi (g_A(t))=\exp \bigl (t\pi (b(A))\bigr ), \qquad d\pi _1\bigl (b(A)\bigr )=\pi (b(A)).\] A complex Clifford module may be regarded here as a real module; this does not assert a separately constructed complex Lie-group structure.

                            [meinrenken2013clifford, Proposition 2.12, p. 40; Proposition 3.2, pp. 53--54] proves the normalized bivector realization and the Spin exponential/action identity. [lawson2016spin, I.2, Remark 2.1 and (2.6)--(2.7), pp. 13--14] independently give the ambient Clifford exponential and its conjugation derivative. The carrier completion and tangent converse above identify the exact vector-generated group used here; Lawson's ambient exponential formula alone does not supply that membership.

                            For the convention match, Meinrenken's bilinear form \(B_M\) satisfies \(B_Q=2B_M\). If \((e_M^i)\) is \(B_M\)-dual to \((e_i)\), then the \(B_Q\)-dual vectors are \(e_M^i/2\), and \[b(A)=\frac 12\sum _i\beta _Q\left (Ae_i,\frac 12e_M^i\right ) =\frac 14\sum _i\beta _Q(Ae_i,e_M^i) =\frac 14\sum _i(Ae_i)e_M^i.\] The last equality uses \(\operatorname {tr}(A)=0\); it does not rescale the half-commutator \(\beta _Q\). TauCeti proves the algebraic lift and generator action at the pinned revision through CliffordAlgebra.quadraticLift_lie_ι and the coordinate formula CliffordAlgebra.soEquivQuadratic_eq_sum_bivector. The same normalization governs the actual compact differential below.

                            For the standard positive form \(Q_n^+\), TauCeti equips the closed range of Spin in Clifford units with a Lie-group structure. The continuous multiplicative equivalence TauCeti.CliffordAlgebra.realCliffordSpinContinuousMulEquivUnitsRange identifies this range with the original vector-generated carrier. Write \(\eta :\Lambda ^2\mathbb R^n\to \mathfrak {cl}^2(Q_n^+)\) for the exterior-bivector realization and \(\kappa :\Lambda ^2\mathbb R^n\to \mathfrak {so}(n)\) for the standard bivector Lie equivalence. In these coordinates the differential of the actual projection \(q:\operatorname {Spin}(n)\to SO(n)\) satisfies \[(d_1q)_{\mathrm {coord}}\bigl (\eta (z)\bigr )=\kappa (z), \qquad b(A)=\eta \bigl (\kappa ^{-1}(A)\bigr ).\] The first equality is TauCeti.CliffordAlgebra.realCliffordSpinToSpecialOrthogonalCoordinateLieHom_eq_bivectorEquivSo. Its proof differentiates conjugation by the Clifford exponential and identifies the resulting action with the commutator above. Thus neither an extra sign nor a factor of two is inserted in passing from the algebraic lift to the group differential.

                            There is also an all-signature exponential criterion. For the standard real form \(Q_{p,q}\), CliffordAlgebra.forall_expUnit_smul_mem_realCliffordSpinGroup_iff_mem_quadraticLieSubalgebra states, for an ambient Clifford element \(x\), \[\bigl (\forall t\in \mathbb R,\ \exp (tx)\in \operatorname {Spin}(Q_{p,q})\bigr ) \quad \Longleftrightarrow \quad x\in \mathfrak {cl}^2(Q_{p,q}).\] Here the exponential is first formed as a Clifford unit and membership is in the actual Spin carrier. This quantifies over every real \(t\); it does not identify quadratic elements from a single exponential value. The differential declaration uses the compact form \(Q_n^+\); the criterion ranges over all standard real signatures. The argument above continues to supply the assertion for an arbitrary nondegenerate \(Q\).

                            Example. A planar Spin curve records the half-angle [fcap-0038]

                              Let \(Q(e_1)=Q(e_2)=1\) with \(B_Q(e_1,e_2)=0\), and let \(J(e_1)=-e_2\), \(J(e_2)=e_1\). The normalization in Proposition [fcap-0037] gives \[b(J)=\frac 12e_1e_2, \qquad g(\theta )=\exp \left (\frac \theta 2e_1e_2\right ) =\cos \frac \theta 2+\sin \frac \theta 2e_1e_2.\] Since \((e_1e_2)^2=-1\), direct multiplication gives \[g(\theta )e_1g(\theta )^{-1} =\cos \theta \,e_1-\sin \theta \,e_2.\] Thus differentiating at zero gives \(J\) with the displayed sign, while \[g(2\pi )=-1,\qquad g(4\pi )=1.\] The Spin parameter therefore has twice the period of its vector action. This is the rank-two curve used in the compact-cover calculation below.

                              [meinrenken2013clifford, Example 3.3, p. 54] computes the same Clifford exponential and planar action. His convention has \(B_M(e_i,e_i)=1\), hence the same generator squares; the preceding polar-form translation fixes the coefficient \(1/2\).

                              Theorem. Lie-algebra representations integrate uniquely on compact Spin [fcap-003L]

                                Let \(n\geq 3\), let \(F=\mathbb R\) or \(\mathbb C\), and let \(S\) be a finite-dimensional \(F\)-vector space. Put \(G=\operatorname {Spin}(Q_n^+)\) for the compact positive-square group of Proposition [fcap-0039], and write \(b:\mathfrak {so}(n)\to T_1G\) for the quadratic lift of Proposition [fcap-0037]. Every real-linear Lie-algebra homomorphism \[r:\mathfrak {so}(n)\longrightarrow \mathfrak {gl}_F(S)\] has a unique smooth group representation \(R:G\to GL_F(S)\) satisfying \[dR_1(b(A))=r(A),\qquad R\bigl (\exp (t b(A))\bigr )=\exp (t r(A)).\] Here \(A\in \mathfrak {so}(n)\) and \(t\in \mathbb R\). When \(F=\mathbb C\), the target \(\mathfrak {gl}_{\mathbb C}(S)\) is regarded as a real Lie algebra: the group being represented is compact real Spin, and its operators on \(S\) are complex-linear.

                                [fulton2004representation, Section 8.3, Proposition 8.41 and Second Principle, pp. 118--119] proves integration by the graph-subgroup construction. The concrete Lie structure in Proposition [fcap-0037] and simple connectedness in Proposition [fcap-003A] supply its hypotheses for the selected Spin carrier.

                                Proof. 

                                  Compose \(r\) with \(b^{-1}\) to obtain a Lie homomorphism \(\widetilde r:T_1G\to \mathfrak {gl}_F(S)\). Its graph \[\mathfrak j=\{(X,\widetilde r(X)):X\in T_1G\}\] is a real Lie subalgebra of \(T_1G\oplus \mathfrak {gl}_F(S)\). The Lie-subgroup theorem integrates it to a connected immersed subgroup \(J\subseteq G\times GL_F(S)\). Projection onto the first factor gives a homomorphism \(p:J\to G\) whose differential is an isomorphism.

                                  Thus \(p\) is a local diffeomorphism. Its image is an open subgroup of connected \(G\), hence all of \(G\). Moreover, \(p\) is a covering: choose an identity neighborhood \(U\subseteq J\) on which \(p\) is a diffeomorphism onto \(V\subseteq G\). The inverse image of \(V\) is the disjoint union of the translates \(kU\), \(k\in \ker p\); every translate maps diffeomorphically to \(V\). Since \(J\) is connected and \(G\) is simply connected, this covering is an isomorphism. Projection onto the second factor after \(p^{-1}\) is the required \(R\).

                                  A smooth homomorphism carries a one-parameter subgroup to the one-parameter subgroup with the differentiated generator. This gives the exponential identity above. If two homomorphisms have the stated differential, they therefore agree on the image of an exponential neighborhood of zero. An identity neighborhood generates every connected Lie group, so they agree on all of \(G\).

                                  TauCeti's lieMap_injective proves this uniqueness principle for smooth homomorphisms out of a preconnected finite-dimensional real Lie group. It does not supply the existence construction above. The restriction \(n\geq 3\) enters through simple connectedness; the circle \(\operatorname {Spin}(2)\) does not have the same unrestricted integration property.

                                  Proposition. The central sign determines descent to the special orthogonal group [fcap-003M]
                                  ✍️source

                                    Keep the hypotheses and notation of Theorem [fcap-003L], and let \(q:G\to SO(n)\) be the vector action. The integrated representation \(R\) factors through a smooth representation \(\overline R\) of \(SO(n)\) precisely when \[R(-1)=\operatorname {Id}_S.\] Equivalently, let \(J\in \mathfrak {so}(n)\) send \(e_1\mapsto -e_2\), \(e_2\mapsto e_1\), and vanish on the remaining coordinate vectors. Then the descent condition is \[\exp \bigl (2\pi r(J)\bigr )=\operatorname {Id}_S.\]

                                    Proof. 

                                      The covering Proposition [fcap-0039] has kernel \(\{1,-1\}\). A factorization forces \(R(-1)=\overline R(1)=\operatorname {Id}_S\). Conversely, under that condition set \(\overline R(q(g))=R(g)\). Any two lifts differ by \(1\) or \(-1\), so the value is independent of the lift. Surjectivity of \(q\) proves both the homomorphism law and uniqueness of \(\overline R\). The differential of \(q\) is an isomorphism by Proposition [fcap-0037]; its local smooth inverse sections express \(\overline R\) locally as \(R\) composed with a smooth section. Hence the descended representation is smooth. Finally, Example [fcap-0038] gives \[\exp \bigl (2\pi b(J)\bigr )=-1,\] so exponential naturality identifies \(R(-1)\) with the displayed matrix exponential.

                                      This criterion compares the integrated action with Clifford modules. Suppose \[f:\mathcal {C}\kern -2pt\ell ^0(Q_n^+)\longrightarrow \operatorname {End}_F(S)\] is a unital real-algebra homomorphism from the even Clifford algebra. Its restriction \(R_f(g)=f(g)\) takes Spin to invertible operators, with inverse \(f(g^{-1})\). Finite-dimensional linearity makes this restriction smooth. Since \(b(A)\) is even, the exponential power series stays inside \(\mathcal {C}\kern -2pt\ell ^0(Q_n^+)\) and gives \[R_f\bigl (\exp (t b(A))\bigr ) =\exp \bigl (t f(b(A))\bigr ).\] Since \(f\) preserves commutators, \(r(A)=f(b(A))\) is a Lie-algebra action. Consequently \(d(R_f)_1(b(A))=f(b(A))\). The uniqueness in Theorem [fcap-003L] identifies \(R_f\) with the integrated action for \(r(A)=f(b(A))\); it is an equality on the chosen module, not merely an unspecified representation equivalence.

                                      Unitality gives \(R_f(-1)=-\operatorname {Id}_S\). Thus a nonzero such module does not descend to \(SO(n)\). This includes the complex spin and half-spin modules: they are restrictions of modules for the complexified even Clifford algebra, as described in [meinrenken2013clifford, Section 3.7.5, pp. 80--81]. No extension of a half-spin module to the full Clifford algebra is needed. The central scalar \(-1\) is fixed by the even-algebra sign comparison in Proposition [fcap-0039], so this obstruction is unchanged by the two Clifford sign conventions.

                                      The same calculation shows why tensor constructions can descend. On \(S\otimes _F S\) the central element acts by \((-\operatorname {Id})\otimes (-\operatorname {Id})=\operatorname {Id}\); on \(\operatorname {End}_F(S)\) its conjugation action is also the identity. Both actions therefore factor through \(SO(n)\). Differentiating their defining group actions gives, respectively, \[\begin {aligned} A\cdot (s\otimes t)&=r(A)s\otimes t+s\otimes r(A)t,\\ A\cdot T&=r(A)T-Tr(A). \end {aligned}\] The tensor formula agrees with [fulton2004representation, Section 8.1, equation (8.12), p. 110]. Descent concerns the central action of the whole group, even though these differentiated formulas use only its Lie algebra.

                                      For an action of the full real Clifford algebra, TauCeti's AlgHom.lieMap_realCliffordSpinSmoothHom_eq identifies its differentiated smooth restriction with the quadratic Clifford action. The declaration uses the closed Spin range in Clifford units and its Lie-algebra coordinates; the natural carrier equivalence transports the action back to \(G\). Its input is a full-Clifford algebra homomorphism into a finite-dimensional normed real algebra. It does not state the even-module extension or the descent criterion proved here.

                                      The actual orthogonal differential fixes its coordinates as well. Let \(X\in T_1\operatorname {Spin}(n)\) and put \(A=d_1q(X)\), expressed as a skew-symmetric matrix. With the normalized \(b\) from Proposition [fcap-0037], the refined identity is \[d(R_f)_1(X)=f\bigl (b(A)\bigr ) =f\bigl (\eta (\kappa ^{-1}(A))\bigr ).\] AlgHom.unitsLieAlgebraLieEquiv_lieMap_realCliffordSpinSmoothHom_eq_bivectorExterior proves this after the canonical identification of the target units Lie algebra with its ambient algebra. Its \(A\) comes from the differential of the actual Spin projection, so the formula has the normalization already checked in Proposition [fcap-0037]. The input remains a homomorphism from the full \(\mathcal {C}\kern -2pt\ell (Q_n^+)\) into a finite-dimensional normed real algebra. It supplies the differential comparison for that restriction; the integration, even-only and half-spin cases, and central-sign descent argument retain their separate proofs above and in Theorem [fcap-003L].

                                      Backlinks

                                        Proposition. Real matrix blocks control Spin module complexification [fcap-0042]

                                          Let \(A=M_d(D)\), where \(d\geq 1\) and \(D\in \{\mathbb R,\mathbb C,\mathbb H\}\), regarded as a real algebra. Its unique irreducible real left module is \(U=D^d\), with commutant \(D^{\mathrm {op}}\) acting by right multiplication. Its complexification has the following form: \[\begin {array}{c|c|c|c} D&A\otimes _{\mathbb R}\mathbb C&U\otimes _{\mathbb R}\mathbb C &\dim _{\mathbb C}S\\\hline \mathbb R&M_d(\mathbb C)&S&d\\ \mathbb C&M_d(\mathbb C)\oplus M_d(\mathbb C)&S\oplus \overline S&d\\ \mathbb H&M_{2d}(\mathbb C)&S\oplus S&2d \end {array}\] In the complex row, the two summands have different central supports; in the quaternionic row, they are isomorphic. For a product of real matrix algebras, first select one simple block. These statements apply to irreducible real Spin modules obtained from even Clifford algebras because the actual Spin group spans the even algebra.

                                          For the matrix-module assertion, the idempotents \(E_{ii}\) split any module into its coordinate corners, and \(E_{ij}\) identify the corners with one another. A simple module therefore has a simple \(D\)-module in its first corner, which is one-dimensional over the division algebra \(D\); this gives \(D^d\). For an endomorphism commuting with the full algebra, the matrix units make all coordinate maps the same. Commutation with the \(D\)-valued diagonal entries makes this common map \(f\) left \(D\)-linear, so \(f(x)=xf(1)\). It is therefore right multiplication by a single element on every coordinate. With \(R_a(u)=ua\), composition is \(R_aR_b=R_{ba}\), explaining the opposite algebra. Conjugation identifies \(D^{\mathrm {op}}\) with \(D\) when only its real algebra type is recorded. This is the real matrix-module classification of [lawson2016spin, Chapter I, Theorem 5.6, pp. 31--32]. The matrix-corner reconstruction has the general formal counterpart ModuleCat.matrixEquivalence, an equivalence between modules over a ring and modules over its matrix ring with a finite nonempty index type. The three real types and their commutants are the specializations calculated here.

                                          The real row complexifies by entrywise scalar extension; conjugation is the resulting real structure. For the other rows, give \(U\) the complex structure \(u\mapsto ui\). The complexification of an underlying real complex space decomposes as \(S\oplus \overline S\), the two eigenspaces of this operator after scalar extension. For \(D=\mathbb C\), the central element \(i1\) acts as \(i\) on one summand and \(-i\) on the other. They are therefore inequivalent. For \(D=\mathbb H\), right multiplication \(J(u)=uj\) commutes with the left algebra action and obeys \(J(uz)=J(u)\overline z\) and \(J^2=-1\). Thus it identifies \(\overline S\) with \(S\). The quaternion matrix embedding Quaternion.toComplexMatrix_apply sends \(1,i,j,k\) to a complex basis of \(M_2(\mathbb C)\). Scalar extension consequently gives \(\mathbb H\otimes _{\mathbb R}\mathbb C\simeq M_2(\mathbb C)\) and then the displayed matrix algebra for general \(d\). Its action on \(S\) is the defining simple module of complex dimension \(2d\).

                                          Here is the promised group-to-algebra bridge in every nondegenerate real signature. Choose orthogonal Clifford generators \(e_i\) with \(e_i^2=\varepsilon _i\in \{1,-1\}\). The real span \(L\) of Spin is a unital subalgebra, since products of linear combinations expand into linear combinations of group products. For \(i\ne j\) with \(\varepsilon _i\varepsilon _j=1\), \(e_ie_j\) itself lies in Spin by Remark [fcap-0028]. For opposite signs put \[v=\frac {5\varepsilon _i}{3}e_i+\frac 43e_j,\qquad Q(v)=\varepsilon _i,\qquad g=e_iv=\frac 53+\frac 43e_ie_j\in \operatorname {Spin}(Q).\] The last inclusion again uses \(Q(e_i)Q(v)=1\), hence the actual norm-one Lipschitz carrier. Therefore \(e_ie_j=\frac 34(g-\frac 53\,1)\in L\). All bivectors lie in \(L\); their products and \(1\) span the even Clifford algebra by its orthogonal monomial basis. Thus \[\operatorname {span}_{\mathbb R}\operatorname {Spin}(p,q)=\mathcal {C}\kern -2pt\ell ^+(p,q).\] It follows that real invariant subspaces and commuting endomorphisms for Spin are exactly those for the even algebra. TauCeti's CliffordAlgebra.span_spinGroup_eq_even_of_isSquare proves the spanning conclusion under a square-normalization hypothesis for every pair of nonisotropic vectors. That hypothesis holds for a definite real form, but fails for opposite-sign pairs. The displayed rational combination supplies the indefinite case separately.

                                          For the compact positive form with \(n\geq 1\), the generators \(e_ie_n\), \(1\leq i<n\), square to \(-1\), anticommute, and generate the even algebra. Equality of dimensions gives \[\mathcal {C}\kern -2pt\ell ^+(n,0)\simeq \mathcal {C}\kern -2pt\ell (0,n-1).\] Combining the real classification Remark [fcap-0016] with the three rows above recovers the compact module types of Theorem [fcap-0041]. Lawson--Michelsohn write \(\mathcal {C}\kern -2pt\ell _n\) for our \(\mathcal {C}\kern -2pt\ell (0,n)\); their even-algebra identification and module table use this convention [lawson2016spin, Chapter I, (5.4)--(5.5) and Theorem 5.8, Table III, pp. 32--33]. Their compact Spin-spanning argument appears in Proposition 5.12, p. 36; the opposite-sign calculation above extends the linear-span argument to indefinite forms.

                                          Signature still changes the real module type: \[\begin {aligned} \mathcal {C}\kern -2pt\ell ^+(2,2)&\simeq M_2(\mathbb R)\oplus M_2(\mathbb R),\\ \mathcal {C}\kern -2pt\ell ^+(4,0)&\simeq \mathbb H\oplus \mathbb H. \end {aligned}\] The split case gives real two-dimensional half-spin modules. The compact case gives quaternionic complex two-dimensional halves, each with real dimension four. The Lorentz even algebra \(M_2(\mathbb C)\) in Example [fcap-002L] has a real four-dimensional simple module; its complexification is the pair of inequivalent complex two-dimensional Weyl modules. Thus the compact Hermitian comparison cannot simply be reused for noncompact signatures. In all cases the scalar \(-1\in \operatorname {Spin}\) acts as \(-\operatorname {id}\), retaining the descent obstruction of Proposition [fcap-003M].

                                          Related

                                            Example. A planar Spin curve records the half-angle [fcap-0038]

                                              Let \(Q(e_1)=Q(e_2)=1\) with \(B_Q(e_1,e_2)=0\), and let \(J(e_1)=-e_2\), \(J(e_2)=e_1\). The normalization in Proposition [fcap-0037] gives \[b(J)=\frac 12e_1e_2, \qquad g(\theta )=\exp \left (\frac \theta 2e_1e_2\right ) =\cos \frac \theta 2+\sin \frac \theta 2e_1e_2.\] Since \((e_1e_2)^2=-1\), direct multiplication gives \[g(\theta )e_1g(\theta )^{-1} =\cos \theta \,e_1-\sin \theta \,e_2.\] Thus differentiating at zero gives \(J\) with the displayed sign, while \[g(2\pi )=-1,\qquad g(4\pi )=1.\] The Spin parameter therefore has twice the period of its vector action. This is the rank-two curve used in the compact-cover calculation below.

                                              [meinrenken2013clifford, Example 3.3, p. 54] computes the same Clifford exponential and planar action. His convention has \(B_M(e_i,e_i)=1\), hence the same generator squares; the preceding polar-form translation fixes the coefficient \(1/2\).

                                              Theorem. Lie-algebra representations integrate uniquely on compact Spin [fcap-003L]

                                                Let \(n\geq 3\), let \(F=\mathbb R\) or \(\mathbb C\), and let \(S\) be a finite-dimensional \(F\)-vector space. Put \(G=\operatorname {Spin}(Q_n^+)\) for the compact positive-square group of Proposition [fcap-0039], and write \(b:\mathfrak {so}(n)\to T_1G\) for the quadratic lift of Proposition [fcap-0037]. Every real-linear Lie-algebra homomorphism \[r:\mathfrak {so}(n)\longrightarrow \mathfrak {gl}_F(S)\] has a unique smooth group representation \(R:G\to GL_F(S)\) satisfying \[dR_1(b(A))=r(A),\qquad R\bigl (\exp (t b(A))\bigr )=\exp (t r(A)).\] Here \(A\in \mathfrak {so}(n)\) and \(t\in \mathbb R\). When \(F=\mathbb C\), the target \(\mathfrak {gl}_{\mathbb C}(S)\) is regarded as a real Lie algebra: the group being represented is compact real Spin, and its operators on \(S\) are complex-linear.

                                                [fulton2004representation, Section 8.3, Proposition 8.41 and Second Principle, pp. 118--119] proves integration by the graph-subgroup construction. The concrete Lie structure in Proposition [fcap-0037] and simple connectedness in Proposition [fcap-003A] supply its hypotheses for the selected Spin carrier.

                                                Proof. 

                                                  Compose \(r\) with \(b^{-1}\) to obtain a Lie homomorphism \(\widetilde r:T_1G\to \mathfrak {gl}_F(S)\). Its graph \[\mathfrak j=\{(X,\widetilde r(X)):X\in T_1G\}\] is a real Lie subalgebra of \(T_1G\oplus \mathfrak {gl}_F(S)\). The Lie-subgroup theorem integrates it to a connected immersed subgroup \(J\subseteq G\times GL_F(S)\). Projection onto the first factor gives a homomorphism \(p:J\to G\) whose differential is an isomorphism.

                                                  Thus \(p\) is a local diffeomorphism. Its image is an open subgroup of connected \(G\), hence all of \(G\). Moreover, \(p\) is a covering: choose an identity neighborhood \(U\subseteq J\) on which \(p\) is a diffeomorphism onto \(V\subseteq G\). The inverse image of \(V\) is the disjoint union of the translates \(kU\), \(k\in \ker p\); every translate maps diffeomorphically to \(V\). Since \(J\) is connected and \(G\) is simply connected, this covering is an isomorphism. Projection onto the second factor after \(p^{-1}\) is the required \(R\).

                                                  A smooth homomorphism carries a one-parameter subgroup to the one-parameter subgroup with the differentiated generator. This gives the exponential identity above. If two homomorphisms have the stated differential, they therefore agree on the image of an exponential neighborhood of zero. An identity neighborhood generates every connected Lie group, so they agree on all of \(G\).

                                                  TauCeti's lieMap_injective proves this uniqueness principle for smooth homomorphisms out of a preconnected finite-dimensional real Lie group. It does not supply the existence construction above. The restriction \(n\geq 3\) enters through simple connectedness; the circle \(\operatorname {Spin}(2)\) does not have the same unrestricted integration property.

                                                  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 differential of the actual Spin action is the quadratic lift [fcap-0037]

                                                      Let \(V\) be a positive-dimensional finite-dimensional real vector space, and let \(Q\) be nondegenerate. Give \(\mathcal {C}\kern -2pt\ell (Q)\) its ordinary finite-dimensional topology. Inside \(\mathcal {C}\kern -2pt\ell (Q)^\times \), evenness, reverse norm one, and normalization of the embedded vector subspace are closed conditions and define a subgroup. This subgroup is the actual vector-generated \(\operatorname {Spin}(Q)\). Indeed, for any element \(x\) satisfying them, its twisted action lies in \(O(Q)\). Cartan--Dieudonne supplies a vector product \(u\) with the same twisted action. For \(z=u^{-1}x\), \[\alpha (z)\iota (v)=\iota (v)z\qquad (v\in V).\] Graded centrality makes \(z\) a nonzero scalar; no parity of \(u\) has been assumed in this step. If \(Q(w)\ne 0\), every nonzero scalar \(c\) is the two-vector product \[\iota (w)\,\iota \left (\frac {c}{Q(w)}w\right )=c1.\] Thus \(x\) is vector-generated, and its stated evenness and norm place it in Spin. The reverse inclusion is immediate from the carrier definition. The closed-subgroup theorem now gives this concrete Spin group its finite-dimensional real Lie-group structure.

                                                      For \(A\in \mathfrak {so}(V,B_Q)\), let \(b(A)\) be the normalized quadratic Clifford lift of Theorem [fcap-000R]. For every \(t\in \mathbb R\), \[g_A(t)=\exp \bigl (t b(A)\bigr )\in \operatorname {Spin}(Q), \qquad g_A(t)\,\iota (v)\,g_A(t)^{-1} =\iota \bigl (\exp (tA)v\bigr ).\] Indeed, reversal sends \(b(A)\) to \(-b(A)\), so the exponential is even and has reverse norm one. The commutator identity \([b(A),\iota (v)]=\iota (Av)\) gives the displayed conjugation formula by the exponential series. Hence \(g_A(t)\) satisfies the three closed conditions above and belongs to the actual Spin group.

                                                      The tangent Lie algebra at \(1\) is exactly the image of \(b\). One inclusion is supplied by the curves \(g_A\). Conversely, let \(X\) be tangent at \(1\). Differentiating evenness, reverse norm one, and vector normalization gives \[X\text { even},\qquad \operatorname {rev}(X)=-X, \qquad [X,\iota (V)]\subseteq \iota (V).\] Write \([X,\iota (v)]=\iota (Av)\). Differentiating preservation of \(Q\) makes \(A\) skew-adjoint. Then \(X-b(A)\) is even and commutes with every vector, so it is scalar; reverse antisymmetry forces that real scalar to vanish. Therefore \[T_1\operatorname {Spin}(Q)=b\bigl (\mathfrak {so}(V,B_Q)\bigr ), \qquad d_1(\operatorname {spinVectorAction})\bigl (b(A)\bigr )=A.\] This is the genuine differential statement whose algebraic commutator precursor appears in Theorem [fcap-000R] and whose polar-dual coordinate formula is Theorem [fcap-001Z].

                                                      If \(\pi :\mathcal {C}\kern -2pt\ell (Q)\to \operatorname {End}_{\mathbb R}(S)\) is a finite-dimensional real Clifford module, continuity of the power series gives \[\pi (g_A(t))=\exp \bigl (t\pi (b(A))\bigr ), \qquad d\pi _1\bigl (b(A)\bigr )=\pi (b(A)).\] A complex Clifford module may be regarded here as a real module; this does not assert a separately constructed complex Lie-group structure.

                                                      [meinrenken2013clifford, Proposition 2.12, p. 40; Proposition 3.2, pp. 53--54] proves the normalized bivector realization and the Spin exponential/action identity. [lawson2016spin, I.2, Remark 2.1 and (2.6)--(2.7), pp. 13--14] independently give the ambient Clifford exponential and its conjugation derivative. The carrier completion and tangent converse above identify the exact vector-generated group used here; Lawson's ambient exponential formula alone does not supply that membership.

                                                      For the convention match, Meinrenken's bilinear form \(B_M\) satisfies \(B_Q=2B_M\). If \((e_M^i)\) is \(B_M\)-dual to \((e_i)\), then the \(B_Q\)-dual vectors are \(e_M^i/2\), and \[b(A)=\frac 12\sum _i\beta _Q\left (Ae_i,\frac 12e_M^i\right ) =\frac 14\sum _i\beta _Q(Ae_i,e_M^i) =\frac 14\sum _i(Ae_i)e_M^i.\] The last equality uses \(\operatorname {tr}(A)=0\); it does not rescale the half-commutator \(\beta _Q\). TauCeti proves the algebraic lift and generator action at the pinned revision through CliffordAlgebra.quadraticLift_lie_ι and the coordinate formula CliffordAlgebra.soEquivQuadratic_eq_sum_bivector. The same normalization governs the actual compact differential below.

                                                      For the standard positive form \(Q_n^+\), TauCeti equips the closed range of Spin in Clifford units with a Lie-group structure. The continuous multiplicative equivalence TauCeti.CliffordAlgebra.realCliffordSpinContinuousMulEquivUnitsRange identifies this range with the original vector-generated carrier. Write \(\eta :\Lambda ^2\mathbb R^n\to \mathfrak {cl}^2(Q_n^+)\) for the exterior-bivector realization and \(\kappa :\Lambda ^2\mathbb R^n\to \mathfrak {so}(n)\) for the standard bivector Lie equivalence. In these coordinates the differential of the actual projection \(q:\operatorname {Spin}(n)\to SO(n)\) satisfies \[(d_1q)_{\mathrm {coord}}\bigl (\eta (z)\bigr )=\kappa (z), \qquad b(A)=\eta \bigl (\kappa ^{-1}(A)\bigr ).\] The first equality is TauCeti.CliffordAlgebra.realCliffordSpinToSpecialOrthogonalCoordinateLieHom_eq_bivectorEquivSo. Its proof differentiates conjugation by the Clifford exponential and identifies the resulting action with the commutator above. Thus neither an extra sign nor a factor of two is inserted in passing from the algebraic lift to the group differential.

                                                      There is also an all-signature exponential criterion. For the standard real form \(Q_{p,q}\), CliffordAlgebra.forall_expUnit_smul_mem_realCliffordSpinGroup_iff_mem_quadraticLieSubalgebra states, for an ambient Clifford element \(x\), \[\bigl (\forall t\in \mathbb R,\ \exp (tx)\in \operatorname {Spin}(Q_{p,q})\bigr ) \quad \Longleftrightarrow \quad x\in \mathfrak {cl}^2(Q_{p,q}).\] Here the exponential is first formed as a Clifford unit and membership is in the actual Spin carrier. This quantifies over every real \(t\); it does not identify quadratic elements from a single exponential value. The differential declaration uses the compact form \(Q_n^+\); the criterion ranges over all standard real signatures. The argument above continues to supply the assertion for an arbitrary nondegenerate \(Q\).