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.

In the setting of Definition 1, 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.

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 2, 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.

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

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

The constructions in Definition 1--Example 5 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 7. Thus the generic Lie functor and the Clifford calculation retain distinct hypotheses and meet only after the actual group structure has been established.

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

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

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 7. 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 7 and simple connectedness in Proposition [fcap-003A] supply its hypotheses for the selected Spin carrier.

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.

Keep the hypotheses and notation of Theorem 9, 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.\]

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 9 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 7, 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 7. 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 9.