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

    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.

      References

        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]
                              ✍️source

                                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]

                                    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

                                        Theorem. A pinned three-cycle integrates to compact triality [fcap-003T]

                                          Let \(G=\operatorname {Spin}(Q_8^+)\) be the compact positive-square Clifford group, and let \(V\) denote its complexified vector representation. There is a smooth outer automorphism \(\tau :G\to G\) of exact order three for which \[V\circ \tau \simeq S^+,\qquad V\circ \tau ^2\simeq S^-.\] Here \(S^+=L(\omega _4)\) and \(S^-=L(\omega _3)\) use the exterior convention of Proposition [fcap-003B]. These are literal pullbacks of representations of the compact real group.

                                          Proof. 

                                            Choose a real orthonormal basis \(a_i,b_i\), \(1\leq i\leq 4\), and set \(u_i=(a_i+\mathrm i b_i)/2\), \(u_i'=\overline {u_i}\). Since \(B_Q=2\langle \ ,\ \rangle \), these are polar-dual isotropic bases. In the complexified Clifford algebra, \[u_i u_j'+u_j'u_i=\delta _{ij},\qquad u_i u_j+u_j u_i=u_i'u_j'+u_j'u_i'=0.\] Use precisely the quadratic generators of Proposition [fcap-002X]: \[\begin {aligned} H_i&=u_i u_i'-\tfrac 12,\\ E_i&=u_i u_{i+1}',&F_i&=u_{i+1}u_i',&h_i&=H_i-H_{i+1} && (i<4),\\ E_4&=u_3u_4,&F_4&=u_4'u_3',&h_4&=H_3+H_4. \end {aligned}\] They belong to the complexified quadratic Lie algebra \(\mathfrak g_{\mathbb C}\) of Proposition [fcap-0037]. The simple roots are \(\epsilon _i-\epsilon _{i+1}\) for \(i<4\) and \(\epsilon _3+\epsilon _4\) for node \(4\); node \(2\) is central.

                                            Let \(A\) be the corresponding \(D_4\) Cartan matrix: its diagonal entries are \(2\), adjacent-node entries \(-1\), and all others \(0\). The displayed Clifford relations give \[\begin {aligned} [h_i,h_j]&=0,&[E_i,F_j]&=\delta _{ij}h_i,\\ [h_i,E_j]&=A_{ij}E_j,&[h_i,F_j]&=-A_{ij}F_j, \end {aligned}\] \[\begin {aligned} (\operatorname {ad}E_i)^{1-A_{ij}}E_j&=0,\\ (\operatorname {ad}F_i)^{1-A_{ij}}F_j&=0\qquad (i\ne j). \end {aligned}\] The positive-root generation in Proposition [fcap-002X], its lowering counterpart and the brackets \([E_i,F_i]\) generate all of \(\mathfrak g_{\mathbb C}\). The Serre presentation and pinned extension theorem in [fulton2004representation, Section 21.3, pp. 337--338] therefore apply to this Lie algebra.

                                            The permutation \(\sigma =(1\ 3\ 4)\), fixing \(2\), preserves \(A\). Reindexing each generator family preserves the presentation, so it defines a unique complex Lie automorphism \(\theta \) with \[\theta (E_i)=E_{\sigma (i)},\qquad \theta (F_i)=F_{\sigma (i)},\qquad \theta (h_i)=h_{\sigma (i)}.\] Inverse reindexing supplies its inverse. Its cube fixes all generators, hence \(\theta ^3=1\).

                                            The compact real form must also be preserved. Let \(\kappa \) be conjugation of the complexified real Clifford algebra. The same Clifford relations, with the reversed factor order in \(F_4\), give \[\begin {aligned} \kappa (H_i)&=u_i'u_i-\tfrac 12=-H_i,\\ \kappa (E_i)&=u_i'u_{i+1}=-F_i&& (i<4),\\ \kappa (E_4)&=u_3'u_4'=-F_4. \end {aligned}\] Also \(\kappa (F_i)=-E_i\) and \(\kappa (h_i)=-h_i\). Thus the antilinear maps \(\kappa \theta \) and \(\theta \kappa \) agree on the generators and everywhere. By Proposition [fcap-0037], the \(\kappa \)-fixed quadratic Lie algebra is exactly \(T_1G\). Consequently \(\theta \) restricts to a real Lie automorphism of the actual compact group's tangent algebra.

                                            The group \(G\) is connected and simply connected by Proposition [fcap-003A]. The general group-to-group integration theorem, the Second Principle in [fulton2004representation, pp. 118--119], therefore integrates this restriction to a smooth homomorphism \(\tau :G\to G\). Its graph-subgroup proof is the construction in Theorem [fcap-003L] with target \(G\): first projection is a surjective covering and hence an isomorphism. Integrating \(\theta ^{-1}\) too gives the inverse of \(\tau \), because a homomorphism from connected \(G\) is determined by its differential. Indeed, equal differentials give equality on an exponential neighborhood, which generates \(G\). The same uniqueness proves \(\tau ^3=1\).

                                            For a highest weight \(\omega _j\), literal pullback along \(\theta \) gives \[(\omega _j\circ \theta )(h_i)=\delta _{j,\sigma (i)} =\omega _{\sigma ^{-1}(j)}(h_i).\] Since \(\theta \) also permutes the positive generators, the new highest weight is \(\omega _{\sigma ^{-1}(j)}\). Starting with \(V=L(\omega _1)\), the pullbacks therefore have labels \(\omega _1,\omega _4,\omega _3\): they are \(V,S^+,S^-\) in that order. These are distinct irreducible classes. Inner automorphisms preserve each representation class, so \(\tau \) is outer and nontrivial; together with \(\tau ^3=1\), this proves exact order three.

                                            The outer-class calculation in Theorem [fcap-003C] is thereby realized by a chosen cube-one automorphism. TauCeti's Serre diagram automorphism formalizes generator reindexing and its order relation on the presented Lie algebra. Its compact real-form identification and integration to this Clifford group are additional steps proved above. The tripled-carrier automorphism discussed in Proposition [fcap-003B] remains a different construction.

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

                                              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].

                                                Related

                                                  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.

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