Proposition. The differential of the actual Spin action is the quadratic lift [fcap-0037]
AGENTDRAFTED
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\).