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

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

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

Reference. Clifford algebras and lie theory [meinrenken2013clifford]

Reference. Spin Geometry [lawson2016spin]

Differentiating and integrating Spin representations [fcap-001Q]

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

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

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

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

Proof.

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

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]

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

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

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

Proof.

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

Proof.

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

Proof.

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

Remark. Horizons beyond the exterior model [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, pp. 59--60]; [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287]; [lawson2016spin, I.2, pp. 13--19] [fcap-0017]

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

Proof.

Theorem. The actual compact \(\operatorname {Spin}(8)\) has outer Lie-automorphism group \(S_3\) [fcap-003C]

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

Proof.

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

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

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]

Theorem. Quadratic elements realize the orthogonal Lie algebra [meinrenken2013clifford, Section 2.2.10, Proposition 2.12, p. 40] [fcap-000R]

soEquivQuadratic soEquivQuadratic_lie_ι
L∃∀N

Theorem. Reconstructing a skew Clifford lift in polar-dual coordinates [fcap-001Z]

soEquivQuadratic_eq_sum_bivector
L∃∀N

Proof.