Chevalley constructs the classical filtration after choosing a finite basis of a vector space over a field. TauCeti's coordinate-free version below is defined for a quadratic form on a module over a commutative ring. The leading-symbol equivalences in Lemma [fcap-000H][fcap-000H] and Theorem [fcap-000I][fcap-000I] additionally assume that \(2\) is invertible.

Let \(R\) be a commutative ring, let \(M\) be an \(R\)-module, and let \(Q:M\to R\) be a quadratic form. In the Clifford algebra \(\mathcal {C}\kern -2pt\ell (Q)\), define \(F_n\mathcal {C}\kern -2pt\ell (Q)\) to be the \(R\)-submodule spanned by all products of at most \(n\) generators: \[F_n\mathcal {C}\kern -2pt\ell (Q)=\operatorname {span}_R\left \{\iota (v_1)\cdots \iota (v_r):0\le r\le n\right \}.\] The empty product gives \(F_0\mathcal {C}\kern -2pt\ell (Q)=R1\). Concatenating words makes the filtration multiplicative; in fact, \[F_i\mathcal {C}\kern -2pt\ell (Q)\,F_j\mathcal {C}\kern -2pt\ell (Q)=F_{i+j}\mathcal {C}\kern -2pt\ell (Q).\] Thus multiplication descends to the successive quotients and makes \[\operatorname {gr}_F\mathcal {C}\kern -2pt\ell (Q)=\bigoplus _{n\ge 0}F_n\mathcal {C}\kern -2pt\ell (Q)/F_{n-1}\mathcal {C}\kern -2pt\ell (Q)\] a graded algebra, with \(F_{-1}\mathcal {C}\kern -2pt\ell (Q)=0\).

Retain the coordinate-free commutative-ring and module setting of Definition [fcap-000G][fcap-000G], and assume that \(2\) is invertible in \(R\). This is TauCeti's extension of Chevalley's finite-basis, vector-space leading-symbol argument. For vectors \(v_1,\ldots ,v_n\in M\), the Clifford relation replaces an interchange by its alternating term plus a scalar contraction. Each contraction removes two generators. Consequently \[\iota (v_1)\cdots \iota (v_n) \equiv v_1\wedge \cdots \wedge v_n\pmod {F_{n-2}},\] where the right-hand side is read through the zero-form exterior model. In particular, the class of the Clifford word in \(F_n/F_{n-1}\) depends alternately on the vectors and is the leading exterior symbol.

Let \(R\), \(M\), and \(Q\) be as in Lemma [fcap-000H][fcap-000H]. Chevalley's finite-dimensional field argument motivates the identification. TauCeti proves the following coordinate-free commutative-ring and module equivalence. For every \(n\ge 0\), the leading-symbol map gives \[F_n\mathcal {C}\kern -2pt\ell (Q)/F_{n-1}\mathcal {C}\kern -2pt\ell (Q)\simeq \bigwedge ^n_R M.\] At \(n=0\) this is the scalar equivalence \(F_0/0\simeq R=\bigwedge ^0_RM\). For \(n>0\), the inverse sends a decomposable exterior product to the class of the corresponding Clifford word.

The point of the quotient is that every contraction term has already fallen into a lower filtration step. Alternation is therefore exact in the graded piece even though it is not exact in the Clifford algebra itself.

Meinrenken's Proposition 2.6 assumes a finite-dimensional vector space over a characteristic-zero field. TauCeti proves the corresponding extension for an additive commutative group \(M\) with a module structure over a commutative ring \(R\), a quadratic form \(Q\) on \(M\), and invertible \(2\in R\). Under these hypotheses, the equivalences of Theorem [fcap-000I][fcap-000I] respect multiplication of homogeneous classes and assemble into a graded-algebra equivalence \[\operatorname {gr}_F\mathcal {C}\kern -2pt\ell (Q)\simeq _{\mathrm {grAlg}}\bigwedge _R M.\] The class of a product of an \(i\)-word and a \(j\)-word is carried to the exterior product of their leading symbols in degree \(i+j\).

This is a PBW theorem for the Clifford filtration. It does not make \(\mathcal {C}\kern -2pt\ell (Q)\) and \(\bigwedge _RM\) isomorphic as algebras. The quadratic form survives in the lower-degree contraction terms of Clifford multiplication; only the associated graded multiplication forgets it.

Let \(R\), \(M\), and \(Q\) be as in Definition [fcap-000G][fcap-000G], and assume \(2\) is invertible in \(R\), as in Lemma [fcap-000H][fcap-000H]. For \(u,v\in M\), the degree-two leading-term map sends their exterior product to the class of the corresponding Clifford word. Writing that word as \[\iota (u)\iota (v) =\frac 12\bigl (\iota (u)\iota (v)-\iota (v)\iota (u)\bigr ) +\frac 12B_Q(u,v)1.\] The second summand belongs to \(F_0\), so it vanishes in \(F_2/F_1\). Thus \(u\wedge v\) maps to the class of \(\iota (u)\iota (v)\); equivalently, under the graded-piece equivalence, that class maps to \(u\wedge v\). This is the two-generator instance of Chevalley's leading-symbol calculation cited in the title. The surviving half-commutator is the Clifford bivector studied next; the scalar polar term is invisible to the leading symbol.

Chevalley's proof chooses a basis, proves that ordered Clifford monomials form a basis, and identifies the underlying vector space with the exterior algebra [chevalley1954algebraic, II.1.2 and II.1.6, pp. 40--42]. Panyushev uses the resulting stable filtration and exterior associated graded as standard representation-theoretic background [panyushev2001exterior, Section 2, p. 7].

The quotient construction above is TauCeti's coordinate-free commutative-ring and module extension of that finite-dimensional field proof. It builds each graded piece from the word-length submodule and its predecessor, handles degree zero separately, and then takes their direct sum. This is a change of packaging and generality, not a stronger claim about unfiltered Clifford multiplication.

Changing the field need not require new generators or a new quadratic basis. Let \(L/K\) be a field extension with \(\operatorname {char}K\ne 2\), and let \((V,Q)\) be a finite-dimensional quadratic space, possibly degenerate. Its scalar extension is \(V_L=L\otimes _K V\) with quadratic form \(Q_L\) characterized by \(Q_L(a\otimes v)=a^2Q(v)\) and the extended polar form. There are canonical \(L\)-algebra isomorphisms \[\begin {aligned} \beta _Q:L\otimes _K\mathcal {C}\kern -2pt\ell _K(Q)&\longrightarrow \mathcal {C}\kern -2pt\ell _L(Q_L),\\ a\otimes \iota _Q(v)&\longmapsto a\,\iota _{Q_L}(1\otimes v),\\ \beta _\wedge :L\otimes _K\bigwedge _K V&\longrightarrow \bigwedge _L V_L,\\ a\otimes (v_1\wedge \cdots \wedge v_r)&\longmapsto a(1\otimes v_1)\wedge \cdots \wedge (1\otimes v_r). \end {aligned}\] The first preserves the word-length filtration and parity; the second preserves exterior degree. No nondegeneracy hypothesis or chosen basis is needed to define either map.

The Clifford statement is [chevalley1954algebraic, II.1.5, p. 41]. The proof below uses the universal property; applying it to the zero form gives the exterior algebra statement.

Write \(C=\mathcal {C}\kern -2pt\ell _K(Q)\) and \(C_L=\mathcal {C}\kern -2pt\ell _L(Q_L)\), and denote the leading-symbol equivalences of Theorem [fcap-000I][fcap-000I] by \(\sigma _K,\sigma _L\). Scalar extension and taking the exterior symbol commute:

For example, \(\beta _Q(1\otimes \iota _Q(v)^2)=Q(v)1\), whereas \((1\otimes v)\wedge (1\otimes v)=0\). The square compares associated graded multiplication. It does not turn the linear Clifford-to-exterior coordinates of Definition [fcap-0003][fcap-0003][fcap-0003] into an algebra map. Chevalley makes this product distinction immediately after II.1.5.

The marked declarations give the two algebra equivalences in the reverse direction. Mathlib allows arbitrary commutative base and extension rings with \(2\) invertible; TauCeti's exterior equivalence needs neither invertible two nor flatness. The symbol square above is the consequence proved here, using the existing leading-symbol equivalence. The separate Spin-lifting consequences remain in Theorem [fcap-003N][fcap-003N] and Proposition [fcap-003O][fcap-003O].

Why does the complex Clifford algebra forget a real signature, while its real vectors still remember it? Let \(V\) be a finite-dimensional real space with nondegenerate quadratic form \(Q\). Its complexification is the scalar extension \(V_{\mathbb C}=\mathbb C\otimes _{\mathbb R}V\). Complex conjugation on the first factor fixes \(V\) and induces the conjugate-linear algebra involution \[\sigma (z\otimes a)=\overline z\otimes a\] on \(\mathbb C\otimes _{\mathbb R}\mathcal {C}\kern -2pt\ell _{\mathbb R}(Q)\). It preserves product order and conjugates scalar coefficients; the grade reversion instead reverses product order and is complex-linear after scalar extension. A real structure on a complex vector space or algebra means a map with \(\sigma (\lambda v+\mu w)=\overline \lambda \sigma (v)+ \overline \mu \sigma (w)\) and \(\sigma ^2=1\), an algebra automorphism in the algebra case. The fixed algebra here is \(1\otimes \mathcal {C}\kern -2pt\ell _{\mathbb R}(Q)\): write an element uniquely as \(1\otimes a+i\otimes b\) with \(a,b\) real to check this.

For the underlying real module of \(\mathcal {C}\kern -2pt\ell _{\mathbb R}(Q)\), this coefficient map is TauCeti.tmulConj. Its involution law is TauCeti.tmulConj_involutive, and its fixed vectors are described by TauCeti.tmulConj_eq_self_iff. These supporting declarations concern the conjugate-linear involution and fixed vectors; multiplicativity and the coordinate comparisons below are the algebra calculations given here.

This is the conjugation construction in [meinrenken2013clifford, Section 2.2.6, p. 34]. Meinrenken's symmetric form is \(B=B_Q/2\), so his generator relation is \(uv+vu=2B(u,v)=B_Q(u,v)\). The following coordinate calculation applies that construction to the scalar-extension isomorphism of Theorem [fcap-003V][fcap-003V].

Choose an orthogonal real basis \(e_1,\ldots ,e_n\) with \(Q(e_j)=1\) for \(j\le p\) and \(Q(e_j)=-1\) for \(j>p\), where \(n=p+q\). These are the signature signs of Convention [fcap-0011][fcap-0011]. On \(\mathbb C^n\), put \(Q_0(z)=\sum _j z_j^2\), with coordinate vectors \(u_j\). The chosen complex isometry \[T(e_j)=\begin {cases}u_j&j\le p,\\i u_j&j>p\end {cases}\] induces \(\mathcal {C}\kern -2pt\ell (T):\mathcal {C}\kern -2pt\ell _{\mathbb C}(Q_{\mathbb C}) \simeq \mathcal {C}\kern -2pt\ell _{\mathbb C}(Q_0)\). Transporting \(\sigma \) through this map and Theorem [fcap-003V][fcap-003V] gives \(\sigma _T\) on the standard complex algebra. On its generators, \[\sigma _T(\iota (u_j))=\begin {cases} \iota (u_j)&j\le p,\\-\iota (u_j)&j>p. \end {cases}\] Indeed, \(T^{-1}(u_j)=-i e_j\) for a negative direction, and conjugation sends this to \(i e_j\), whose image under \(T\) is \(-u_j\). The fixed real generators are consequently \(\iota (u_j)\) and \(i\iota (u_j)\) in the positive and negative directions, respectively.

Already in dimension one, the same complex algebra \(A=\mathbb C[u]/(u^2-1)\) has two different real structures: \[\begin {aligned} \sigma _+(z+wu)&=\overline z+\overline w u, & A^{\sigma _+}&=\mathbb R[ u]\simeq \mathbb R\oplus \mathbb R,\\ \sigma _-(z+wu)&=\overline z-\overline w u, & A^{\sigma _-}&=\mathbb R[iu]\simeq \mathbb C. \end {aligned}\] The first real-algebra isomorphism evaluates at \(u=1,-1\); the second uses \((iu)^2=-1\). Thus forgetting the real structure loses the distinction between \(\mathcal {C}\kern -2pt\ell (1,0)\) and \(\mathcal {C}\kern -2pt\ell (0,1)\). If a different complex isometry is \(T'=UT\), then \(\sigma _{T'}=\mathcal {C}\kern -2pt\ell (U)\sigma _T\mathcal {C}\kern -2pt\ell (U)^{-1}\). The real structure moves with the coordinates; it is not generally entrywise conjugation in every model.

The real-algebra identifications in this example are formalized as TauCeti.realCliffordOneZeroEquivProd and TauCeti.realCliffordZeroOneEquivComplex. These declarations identify the two real Clifford algebras; the comparison of their conjugations inside \(A\) is the calculation above.

Choosing the polarization data for a spinor carrier is a further choice. For \(Q(x,y)=x^2+y^2\), the complex isotropic lines \[W=\mathbb C(e_1+i e_2),\qquad W'=\mathbb C(e_1-i e_2)\] are complementary, and conjugation exchanges them. Their polar pairing is nonzero, so they give the split model after normalizing a dual basis. The carrier \(S=\bigwedge W\) uses \(W\) for creation and \(W'\) for contraction, as in Definition [fcap-001I][fcap-001I]. Conjugation therefore maps this exterior space to \(\bigwedge W'\), rather than supplying a conjugation on \(S\) compatible with the same chosen operators. Comparing these carriers needs an additional intertwining map. This explains why the canonical real structure on the Clifford algebra alone does not choose a real structure on a particular spinor module. The creation/contraction construction is [chevalley1954algebraic, II.2.1--II.2.2, pp. 42--44].

Let \(R\) be a commutative ring with invertible \(2\), let \(M\) be an \(R\)-module, and let \(Q\) be a quadratic form on \(M\). Write \(\alpha \) for the grading involution and \(\operatorname {rev}\) for reversal. For the half-commutator bivector of Convention [fcap-000N][fcap-000N], \[\begin {aligned} \alpha (\beta _Q(u,v))&=\beta _Q(u,v),\\ \operatorname {rev}(\beta _Q(u,v))&=-\beta _Q(u,v). \end {aligned}\] The same reversal sign holds for every bivector in the image of \(\bigwedge _R^2 M\); reversal acts as minus the identity there.

Chevalley defines the main antiautomorphism by reversing products while fixing generators [chevalley1954algebraic, Section 2.1, p. 38]. His parity decomposition identifies even exterior degree with the even Clifford part [chevalley1954algebraic, II.1.6, p. 42]. Those are finite-dimensional field-space conventions; the displayed bivector statement is Tau Ceti's commutative-ring extension.

The same reversal and parity conventions determine the scalar norm signs and the distinction between even-unitary and Spin units in Remark [fcap-0028][fcap-0028].

Let \(R\) be a commutative ring, let \(M\) be an \(R\)-module, and let \(Q\) be a quadratic form on \(M\). Write \(\widehat v=\iota _Q(v)\) for a Clifford generator. Before imposing any invertibility condition, consider the two algebra-valued norm expressions \(N_{\mathrm {rev}}(x)=\operatorname {rev}(x)x\) and \(N_*(x)=x^*x\), where \(x^*=\operatorname {rev}(\alpha (x))\). Identifying a scalar with its image in the Clifford algebra gives \[\begin {aligned} N_{\mathrm {rev}}(\widehat v)&=Q(v), &N_*(\widehat v)&=-Q(v),\\ N_{\mathrm {rev}}(\widehat u\widehat v) &=\widehat v\widehat u\widehat u\widehat v =Q(u)Q(v), &N_*(\widehat u\widehat v)&=Q(u)Q(v). \end {aligned}\] Thus the two signs differ on one generator and agree on a product of two. More generally, reversal gives the product of the quadratic values on every vector word CliffordAlgebra.reverse_prod_map_ι_mul_prod_map_ι, and the two norm expressions agree on every even Clifford element CliffordAlgebra.star_mul_self_eq_reverse_mul_self_of_mem_even.

For a Clifford unit \(x\), membership in the even-unitary carrier is equivalent to evenness together with \(N_{\mathrm {rev}}(x)=1\) CliffordAlgebra.evenUnitaryGroup.mem_iff_reverse_mul_self_eq_one. Those two conditions do not establish Lipschitz membership, which must be retained in the Spin criterion. Precisely, \[\operatorname {im}\bigl (\operatorname {Spin}(Q)\longrightarrow \operatorname {Cl}(Q)^\times \bigr ) =\operatorname {Lipschitz}(Q)\cap \operatorname {EvenUnitary}(Q)\] CliffordAlgebra.range_spinGroup_toUnits. Consequently, if \(Q(u)Q(v)=1\), then \(\widehat u\widehat v\) is an even product of Lipschitz vector units with reverse norm one, hence a Spin element CliffordAlgebra.ι_mul_ι_mem_spinGroup_of_norm_mul_norm_eq_one. This is an unquotiented scalar calculation. The passage to square classes, including the odd reflection sign and its cancellation on even products, is recorded separately in Theorem [fcap-0023][fcap-0023].

Chevalley obtains the same norm from what he calls the main antiautomorphism and records \(\lambda (v)=Q(v)\) and the paired values \(Q(u)Q(v)\) [chevalley1954algebraic, II.3.5--6, pp. 52--53]. His symbol \(\alpha \) in that passage denotes reversal, whereas \(\alpha \) in Lemma [fcap-0021][fcap-0021] denotes the grading involution. Meinrenken calls reversal transposition, writes \(N(x)=x^\top x\), and defines Spin as its norm-one subgroup inside the special Clifford group [meinrenken2013clifford, Sections 2.2.6 and 3.1.1--2, pp. 34, 49--51]. His convention has \(Q(v)=B(v,v)\), so his \(B\) is the half-polar form \(b_Q\) of Convention [fcap-0027][fcap-0027]. Both sources work in narrower finite-dimensional field settings; Meinrenken here assumes characteristic zero and a nondegenerate form. The formal identities linked above hold under the commutative-ring and module hypotheses stated here.

Let \(R\) be a commutative ring, \(M\) an \(R\)-module, and \(Q\) a quadratic form on \(M\). For a pairwise \(Q\)-orthogonal list \(\ell =(v_1,\ldots ,v_n)\), set \[\omega _\ell =\iota _Q(v_1)\cdots \iota _Q(v_n).\] Its square is the scalar \[\omega _\ell ^2 =(-1)^{\binom n2}\left (\prod _{i=1}^{n}Q(v_i)\right )1.\] The empty list gives \(\omega _\ell =1\). No basis, nondegeneracy, finite-dimensionality, or invertibility of \(2\) is required.

Chevalley computes the corresponding square for an orthogonal basis of a nondegenerate even-dimensional quadratic space over a field of characteristic different from \(2\) [chevalley1954algebraic, Proof of II.2.3, p. 45]. His generator relation \(v_i^2=Q(v_i)1\) matches the convention above. Tau Ceti's list identity extends that calculation to arbitrary lengths and the stated commutative-ring setting.

Lawson and Michelsohn write \[v^2=-q(v)1, \qquad vw+wv=-2q(v,w),\] where \(2q(v,w)=q(v+w)-q(v)-q(w)\). Mathlib and TauCeti instead use a quadratic form \(Q\) with \[\iota (v)^2=Q(v)1.\] The conventions agree after setting \(Q=-q\). The orthogonal group and its reflections are unchanged by this global sign reversal. A vector with \(q(v)=1\) therefore has \(Q(v)=-1\) in the convention used below. Mathlib's generator-square rule CliffordAlgebra.ι_sq_scalar uses this \(Q\)-convention.

Let \(F\) be a field of characteristic different from \(2\), let \(Q\) be a quadratic form on an \(F\)-vector space \(V\), and write \[B_Q(x,y)=Q(x+y)-Q(x)-Q(y)\] for its polar form. If \(Q(v)\ne 0\), the reflection with normal vector \(v\) is \[\rho _v(w)=w-\frac {B_Q(v,w)}{Q(v)}v.\] It fixes \(v^\perp \) pointwise, sends \(v\) to \(-v\), and preserves \(Q\). Multiplying \(v\) by a nonzero scalar does not change \(\rho _v\).

Let \(\alpha \) denote the grading involution of \(\mathcal {C}\kern -2pt\ell (Q)\). For \(Q(v)\ne 0\), the Clifford generator \(\iota (v)\) is invertible with \[\iota (v)^{-1}=Q(v)^{-1}\iota (v).\] Its twisted adjoint action on a generator is the reflection in Definition [fcap-0009][fcap-0009]: \[\alpha (\iota (v))\,\iota (w)\,\iota (v)^{-1}=\iota (\rho _v(w)).\]

Lawson--Michelsohn make this product-and-scaling argument for a finite-dimensional quadratic vector space over a field. The statement below is TauCeti's extension to a quadratic module over a commutative ring. It assumes that \(2\) and \(Q(v)\) are invertible.

Let \(R\) be a commutative ring, let \(Q\) be a quadratic form on an \(R\)-module \(M\), and suppose \(2\) and \(Q(v)\) are invertible. If there is a scalar \(c\) such that \[c^2=-Q(v)^{-1},\] then \(Q(cv)=-1\). The normalized Clifford generator \(\iota (cv)\) belongs to the Pin group and its twisted adjoint action is \(\rho _v\), because \(\rho _{cv}=\rho _v\). Consequently \[\rho _v\in \operatorname {range}(\operatorname {pinToOrthogonal}).\] Equivalently, the required hypothesis is that \(-Q(v)^{-1}\) is a square. The conclusion is existential: it asserts that a Pin lift exists, not that a canonical square root has been chosen.

The cited product formulas are stated for a finite-dimensional quadratic vector space over a field. TauCeti packages the same scaling and Clifford-product calculation over the commutative-ring and module hypotheses inherited from Lemma [fcap-000B][fcap-000B].

Let \(R\), \(M\), and \(Q\) be as in Lemma [fcap-000B][fcap-000B]. Suppose \(Q(v)\), \(Q(w)\), and \(2\) are invertible. If there is a scalar \(c\) such that \[c^2=Q(v)^{-1}Q(w)^{-1},\] then \[Q(cv)Q(w)=1.\] Set \(x=\iota (cv)\iota (w)\). The element \(x\) is a product of invertible Clifford generators, and \[x^{*}x =\iota (w)\iota (cv)^2\iota (w) =Q(cv)Q(w)=1.\] Thus \(x\) is a unitary element of the Lipschitz group. It has even degree, so it belongs to the Spin group. Its twisted adjoint action is the ordered product of reflections, and therefore \[\rho _v\rho _w\in \operatorname {range}(\operatorname {spinToOrthogonal}).\]

Equations (2.24)--(2.26) give the product descriptions and scaling invariance used here. The product-square condition is sharper than asking for separate normalizations of \(v\) and \(w\): one scalar normalizes the product even when neither vector has been normalized separately.

Let \(V=\mathbb {R}^n\) with Euclidean inner product and use the sign convention \[Q(x)=-\langle x,x\rangle .\] For a unit vector \(v\), one has \(Q(v)=-1\); thus \(c=1\) satisfies the square condition in Lemma [fcap-000B][fcap-000B]. The Clifford generator \(\iota (v)\) is already Pin-normalized, and its action is the familiar hyperplane reflection \[\rho _v(w)=w-2\langle v,w\rangle v.\] For orthonormal \(v,w\), the even product \(\iota (v)\iota (w)\) lies in Spin and lifts the composition \(\rho _v\rho _w\). This is the Euclidean specialization of the general Pin and paired-Spin lifting statements in Lemma [fcap-000B][fcap-000B] and Theorem [fcap-000C][fcap-000C].

Lawson and Michelsohn supply the twisted-adjoint reflection formula, the definitions of Pin and Spin, the description by products of normalized vectors, and the square-root obstruction to normalization. The square-witness statements in Lemma [fcap-000B][fcap-000B] and Theorem [fcap-000C][fcap-000C] isolate the precise algebraic hypotheses under which one or two reflections lift.

An individual lift does not by itself show that all orthogonal transformations lift. That global conclusion requires finite dimension, nondegeneracy, and the Cartan--Dieudonne factorization developed next.

One reflection can enlarge the fixed subspace of an orthogonal transformation. Iterating this correction proves reflection generation and makes the unnormalized Lipschitz action onto the orthogonal group. Passing to the norm-one Pin and Spin carriers requires scalar normalization: determinant parity controls evenness, while the spinor norm measures the remaining obstruction over a general field.

Extending the field preserves the spinor norm through the map on square classes. A quadratic extension can make a nontrivial obstruction vanish; the resulting pair of Spin lifts records this change through its Galois action.

Isotropic transvections give a complementary explicit family in the Spin image: their nilpotent Clifford lifts add through the quotient \(u^{\perp }/Ku\). A null-frame calculation exhibits the quadratic action term, while a separate factorization retains a radical PGA shear inside the vector-generated carrier.

Theorem. Surjectivity of the Spin action [lawson2016spin, I.2, Theorem 2.9, pp. 18--19] [fcap-001B]

spinToSpecialOrthogonal_surjective_of_isSquarespinToSpecialOrthogonal_surjective

L∃∀NAGENTDRAFTED

Let \(K\) be a field of characteristic different from \(2\), let \(V\) be finite-dimensional, and let \(Q\) be nondegenerate. Suppose that for every nonisotropic \(v\in V\), the scalar \(-Q(v)^{-1}\) is a square in \(K\). Then the twisted-adjoint action restricts to a surjection \[\operatorname {Spin}(V,Q)\twoheadrightarrow SO(V,Q).\] The underlying homomorphism is CliffordAlgebra.spinToSpecialOrthogonal, and its action on vectors is the usual Spin action by CliffordAlgebra.coe_spinToSpecialOrthogonal_apply.

Indeed, the square-normalization hypothesis and Cartan--Dieudonne generation give the Pin surjection of Theorem [fcap-000X][fcap-000X]. It lifts an element of \(SO(V,Q)\) to Pin; the lift has determinant \(1\), so Lemma [fcap-001A][fcap-001A] shows that it is even and therefore lies in Spin. The restriction square

commutes because both vertical maps are induced by the same twisted Clifford conjugation. Over a separably closed field the square condition is automatic, so nondegeneracy and finite dimension suffice. The general restriction principle from a surjective Pin action is CliffordAlgebra.spinToSpecialOrthogonal_surjective_of_pinToOrthogonal_surjective.

The square condition is TauCeti's fixed-sign sufficient hypothesis, stronger in general than Lawson--Michelsohn's option to normalize each vector to either sign; see Theorem [fcap-000X][fcap-000X]. For a positive-definite real geometric form \(q\), the Clifford convention is \(Q=-q\); hence \(-Q(v)^{-1}>0\) for every nonzero \(v\), so the reflecting vectors can be normalized over \(\mathbb {R}\). This observation does not assert the square condition for arbitrary real signatures.

Proposition. The reverse norm descends through the Lipschitz action [fcap-002D]

AGENTDRAFTED

Let \(K\) be a field of characteristic different from two, let \(V\) be a positive-dimensional finite-dimensional \(K\)-space, and let \(Q\) be nondegenerate. Write \(\Gamma (Q)\) for the vector-generated Lipschitz group, and \(\tau _Q:\Gamma (Q)\to O(V,Q)\) for its twisted action. For \(x\in \Gamma (Q)\), let \(N_{\mathrm {rev}}(x)\in K^{\times }\) be the unique scalar unit satisfying \(\operatorname {rev}(x)x=N_{\mathrm {rev}}(x)\,1\). Set \(\mathcal {S}_K=K^{\times }/(K^{\times })^2\). The top row is exact, and the square commutes:

The determinant arrow is a separate branch: \(SO(V,Q)=\ker (\det )\). It is not part of a longer exact row after \(O(V,Q)\). Positive dimension supplies an anisotropic vector, so scalar units form the displayed kernel; the Lipschitz action is onto CliffordAlgebra.scalarUnits_injective CliffordAlgebra.ker_lipschitzToOrthogonal CliffordAlgebra.lipschitzToOrthogonal_surjective. The right vertical map is the orthogonal spinor norm, while \(\nu _Q=\nu _Q^O|_{SO(V,Q)}\) is its restriction used in Theorem [fcap-0023][fcap-0023]. The square expresses descent through the action, not surjectivity of \(\nu _Q^O\) CliffordAlgebra.orthogonalSpinorNorm_lipschitzToOrthogonal.

If \(Q(v)\) is nonzero, then \[N_{\mathrm {rev}}(\widehat v)=Q(v),\qquad \nu _Q^O(r_v)=[Q(v)]\] CliffordAlgebra.cliffordNorm_unitι CliffordAlgebra.orthogonalSpinorNorm_reflectionOrthogonal. Consequently, for an even product \(x=\widehat v_1\cdots \widehat v_{2k}\) of nonisotropic vector lifts, \[\tau _Q(x)=r_{v_1}\cdots r_{v_{2k}}\in SO(V,Q),\qquad \nu _Q(r_{v_1}\cdots r_{v_{2k}}) =\left [\prod _{i=1}^{2k}Q(v_i)\right ].\] Multiplying a lift by \(c\in K^\times \) changes its reverse norm by \(c^2\), so the square class is independent of the chosen lift. [chevalley1954algebraic, II.3.5--6, pp. 52--53] gives these vector and paired-product values. The scalar exact sequence, reflection factorization, and the same square-scaling law appear in [meinrenken2013clifford, Theorem 3.1, pp. 50--51]. Chevalley's quotient statement assumes positive dimension; Meinrenken works with a finite-dimensional characteristic-zero nondegenerate bilinear space.

If \(e:(V,Q)\simeq (V',Q')\) is an isometry equivalence, then conjugation transport preserves both norms: for \(g\in O(V,Q)\) and \(h\in SO(V,Q)\), \[\nu _{Q'}^O(ege^{-1})=\nu _Q^O(g),\qquad \nu _{Q'}(ehe^{-1})=\nu _Q(h).\] It therefore carries \(\ker \nu _Q\) onto \(\ker \nu _{Q'}\) QuadraticMap.IsometryEquiv.orthogonalSpinorNorm_orthogonalGroupCongr QuadraticMap.IsometryEquiv.spinorNorm_specialOrthogonalGroupCongr kernel-transport source. The induced kernel equivalence also commutes with Spin transport Spin-transport source. These are isometry-equivalence statements; they do not assert scalar-extension or orthogonal-product naturality. This is the norm-square companion to the vector-action square in Proposition [fcap-0029][fcap-0029].

Meinrenken works throughout this chapter with finite-dimensional vector spaces over a characteristic-zero field. The cards below retain his normalization and formulas but follow TauCeti's extensions. Each card states the commutative-ring, module, invertible-\(2\), finite-dimensional, or nondegeneracy assumptions it needs.

Meinrenken starts with a symmetric bilinear form \(B\) and the relation \[uv+vu=2B(u,v)1.\] For the associated quadratic form \(Q(v)=B(v,v)\), the polar form used here is \(B_Q=2B\).

Meinrenken's quantization formula and the half-commutator agree: \[q(u\wedge v)=uv-B(u,v)1 =\frac 12(uv-vu)=:\beta (u,v).\] The induced action on a vector is \[[\beta (u,v),x] =B_Q(v,x)u-B_Q(u,x)v =2\bigl (B(v,x)u-B(u,x)v\bigr ).\] This is Meinrenken's formula \(-2\iota _{B(x,-)}(u\wedge v)\) and Kostant's formula \(-2\iota _x(u\wedge v)\) in the corresponding contraction convention [kostant1997clifford, Section 2.4, (12) and Theorem 8, pp. 283, 286]. The factor of two belongs to the passage from \(B\) to the unhalved polar form \(B_Q\); it is not an additional rescaling of \(\beta \).

For the formalized extension described in Convention [fcap-000N][fcap-000N], let \(R\) be a commutative ring in which \(2\) is invertible, let \(M\) be an \(R\)-module, and let \(Q\) be a quadratic form on \(M\). The Clifford bivector of \(u,v\in M\) is \[\beta _Q(u,v)=\frac 12\bigl (\iota (u)\iota (v)-\iota (v)\iota (u)\bigr ).\] It is alternating in \(u\) and \(v\), so it induces a linear map \[\beta _Q:\bigwedge _R^2M\longrightarrow \mathcal {C}\kern -2pt\ell (Q).\] The exterior model is a left inverse on its image: \[\operatorname {equivExterior}_Q\bigl (\beta _Q(z)\bigr )=z \qquad (z\in \bigwedge _R^2M).\] Hence \(\beta _Q\) is injective.

For \(u,v,x\in M\), the commutator of the bivector with a Clifford generator is \[[\beta _Q(u,v),\iota (x)] =\iota \left (B_Q(v,x)u-B_Q(u,x)v\right ).\] The endomorphism \[A_{u\wedge v}(x)=B_Q(v,x)u-B_Q(u,x)v\] is skew-adjoint for \(B_Q\), since \[B_Q(A_{u\wedge v}x,y)+B_Q(x,A_{u\wedge v}y)=0.\] Thus commutation by a degree-two Clifford element preserves the generating module and realizes the elementary infinitesimal orthogonal transformation attached to \(u\wedge v\).

Over the commutative ring and module of Definition [fcap-000O][fcap-000O], let \(\mathfrak {cl}^{(2)}(Q)\) be the submodule of \(\mathcal {C}\kern -2pt\ell (Q)\) spanned by the elements \(\beta _Q(u,v)\). This is TauCeti's module-general extension of Meinrenken's characteristic-zero vector-space construction. The commutator formula of Lemma [fcap-000P][fcap-000P], together with the Jacobi identity, shows that this submodule is closed under commutators. Transporting its bracket across \(\beta _Q\) gives a Lie algebra structure on \(\bigwedge _R^2M\) and a Lie equivalence \[\bigwedge _R^2M\simeq _{\mathrm {Lie}}\mathfrak {cl}^{(2)}(Q).\] On a decomposable bivector the equivalence is exactly \[u\wedge v\longmapsto \frac 12(uv-vu).\] No choice of basis enters this identification.

Meinrenken states this realization over a characteristic-zero field. TauCeti proves the extension below over any field of characteristic different from \(2\). Let \(K\) be such a field, let \(V\) be finite-dimensional, and let \(Q\) be nondegenerate. Write \(\mathfrak {so}(V,B_Q)\) for the Lie algebra of endomorphisms skew-adjoint for the polar form. Then commutation on generators gives a Lie equivalence \[\mathfrak {so}(V,B_Q)\simeq _{\mathrm {Lie}}\mathfrak {cl}^{(2)}(Q).\] If \(A\in \mathfrak {so}(V,B_Q)\) corresponds to \(z_A\in \mathfrak {cl}^{(2)}(Q)\), then \[[z_A,\iota (x)]=\iota (Ax)\qquad (x\in V).\] Combining this equivalence with Theorem [fcap-000Q][fcap-000Q] gives the basis-free chain \[\bigwedge _K^2V\simeq _{\mathrm {Lie}}\mathfrak {so}(V,B_Q) \simeq _{\mathrm {Lie}}\mathfrak {cl}^{(2)}(Q).\] Kostant identifies the same degree-two subspace with \(\operatorname {Lie}(\operatorname {Spin}(V))\) and the first equivalence with the differential of the double cover [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287].

This coordinate example specializes TauCeti's extension of the characteristic-zero construction summarized in Convention [fcap-000N][fcap-000N]. Take \(V=R^n\) with the standard sum-of-squares quadratic form, and let \(e_i,e_j\) be distinct coordinate vectors. Under the standard-coordinate realization, \[e_i\wedge e_j\longmapsto 2(E_{ij}-E_{ji}).\] Thus its action on \(x=(x_k)\) is \[x\longmapsto 2x_j e_i-2x_i e_j.\] The factor \(2\) is the polar-form normalization from Convention [fcap-000N][fcap-000N]: for the sum-of-squares form, \(B_Q(x,y)=2\sum _kx_ky_k\). The displayed matrix is the standard-coordinate specialization of the basis-free isomorphism in Meinrenken's proposition. Dividing the skew matrix by two would correspond to using the associated bilinear form \(B_Q/2\) instead.

Let \(K\) be a field in which \(2\) is invertible, \(V\) a finite-dimensional \(K\)-space, and \(Q\) a nondegenerate quadratic form. Write \(B_Q\) for its unhalved polar form. For a basis \((b_i)\) let \((d_i)\) be its \(B_Q\)-dual basis, and let \(f\in \mathfrak {so}(V,B_Q)\). The quadratic Clifford element \(z_f=\operatorname {soEquivQuadratic}(f)\) has the coordinate expression \[z_f=\frac 12\sum _i\beta _Q\bigl (f(b_i),d_i\bigr ),\] where \(\beta _Q(u,v)=\tfrac 12(\iota (u)\iota (v)-\iota (v)\iota (u))\) is the bivector normalization of Convention [fcap-000N][fcap-000N].

[goodman2009symmetry, Definition 6.1.1(C1), p. 302] uses the complex Clifford relation \[\{\gamma (u),\gamma (v)\}=\beta (u,v)1.\] Thus their \(\beta \) is \(B_Q\), with \(Q(v)=\beta (v,v)/2\).

[goodman2009symmetry, Section 6.2.1, Lemmas 6.2.1--2 and (6.13), pp. 312--313] gives the complex, nondegenerate basis-free construction through \(R_{a,b}(x)=\beta (b,x)a-\beta (a,x)b\) and its half-commutator lift. The displayed polar-dual sum is the coordinate reconstruction; Tau Ceti proves it over the stated wider class of fields.

Let \(K\) be a field in which \(2\) is invertible, and let \(L\) be a finite-dimensional \(K\)-Lie algebra whose Killing form \(\kappa \) is nondegenerate (the formal hypothesis is \(\operatorname {IsKilling}_K(L)\)). Set \(Q_\kappa (y)=\kappa (y,y)\). If \((b_i)\) is a basis and \((b_i^\vee )\) its Killing-dual basis, then for \(x\in L\) the quadratic Clifford lift of the adjoint action is \[\operatorname {adjointCliffordHom}(x) =\frac 14\sum _i\beta _{Q_\kappa } \bigl ([x,b_i],b_i^\vee \bigr ).\] Here \(\beta _{Q_\kappa }\) is the half-commutator bivector of Convention [fcap-000N][fcap-000N]; the summand is the value of CliffordAlgebra.adjointBivector_apply.

Kostant identifies the complex orthogonal Lie algebra with \(\bigwedge ^2L\) and constructs the adjoint map from a complex semisimple \(L\) using its Killing pairing [kostant1997clifford, Sections 1.1--1.2, pp. 275--276]. This supports the complex adjoint construction. The coordinate expression and its \(1/4\) normalization are the calculation here; Tau Ceti's theorem uses the stated \(\operatorname {IsKilling}\) hypothesis over a wider field class.

The quadratic Clifford Lie algebra is the infinitesimal part of the same conjugation action that produces reflections. Kostant proves that \(\bigwedge ^2V=\operatorname {Lie}(\operatorname {Spin}(V))\), that its map to \(\mathfrak {so}(V)\) is the differential of \(\operatorname {Spin}(V)\to SO(V)\), and that its commutator action extends as the corresponding derivation of the exterior algebra [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287]. Chevalley obtains the same two-vector Lie algebra inside the Clifford group [chevalley1954algebraic, II.2.9, pp. 67--68].

The cards above identify the algebraic Lie layer and reconstruct its lifts in coordinates. They do not construct Lie-group structures or identify a differential of a Lie-group covering map. The module-action card that follows uses the quadratic lift; the global orthogonal group is reached elsewhere by finite products of reflections.

Let \(K\) be a field in which \(2\) is invertible, let \(V\) be finite-dimensional, and let \(Q\) be nondegenerate. Suppose a \(K\)-Lie algebra \(L\) acts orthogonally on \(V\) through \[\theta :L\longrightarrow \mathfrak {so}(V,B_Q),\] and let \(\rho :\mathcal {C}\kern -2pt\ell (Q)\to \operatorname {End}_K(S)\) be any Clifford module. The equivalence of Theorem [fcap-000R][fcap-000R] lifts \(\theta \) to quadratic Clifford elements; composing with \(\rho \) gives a Lie representation \[\rho _{\mathcal {C}\kern -2pt\ell }:L\longrightarrow \operatorname {End}_K(S),\qquad \rho _{\mathcal {C}\kern -2pt\ell }(y)=\rho \bigl (\operatorname {soEquivQuadratic}(\theta (y))\bigr ).\] Kostant constructs this lift for a complex reductive group representation and then lets its quadratic elements act on the spin module. The formalized statement isolates the algebraic mechanism over the stated field and for an arbitrary Clifford module; it does not assert that \(\theta \) is a differential of a group representation.

Let \(\mathfrak g\) be a finite-dimensional complex semisimple Lie algebra with Killing form \(\kappa \), and put \(Q_\kappa (x)=\kappa (x,x)\). If \((b_i)\) is a basis and \((b_i^\vee )\) its Killing-dual basis, the normalized quadratic lift of the adjoint action is \[\delta (x)=\frac 14\sum _i \beta _{Q_\kappa }([x,b_i],b_i^\vee )\in \mathcal {C}\kern -2pt\ell (Q_\kappa )^0.\] The coefficient is the one derived in Theorem [fcap-0020][fcap-0020]: the polar form is \(B_{Q_\kappa }=2\kappa \), so the polar-dual basis contributes one factor \(1/2\), and the general lift contributes the other. This is a grade-two element, not the canonical generator \(\iota _{Q_\kappa }(x)\).

There are two natural actions on the same Clifford vector space: \[L_x(c)=\delta (x)c,\qquad D_x(c)=\delta (x)c-c\delta (x).\] If \(R_a(c)=ca\), then \[D_x=L_x-R_{\delta (x)},\qquad [L_x,R_a]=0.\] Under equivariant Clifford antisymmetrization, \(D\) is the derivation extension of the adjoint action to \(\bigwedge \mathfrak g\). The action \(L\) is instead left multiplication on the Clifford algebra. On matrix coordinates \(\operatorname {End}(S)\simeq S\otimes S^*\), it acts on the \(S\) factor and leaves \(S^*\) as a multiplicity space.

TauCeti defines the selected left action and proves these comparisons in CliffordAlgebra.kostantLieModule CliffordAlgebra.kostant_lie_def CliffordAlgebra.kostant_lie_sub_mul CliffordAlgebra.kostantRightMul. The generic module lift in Theorem [fcap-001O][fcap-001O] supplies the same algebraic mechanism, but it does not identify the left action with the exterior derivation action.

[kostant1997clifford, Sections 3.1 and 5.2, pp. 294 and 311] defines the left action through this quarter-normalized lift and separately identifies the commutator with the exterior extension. [panyushev2001exterior, Section 2, internal preprint pp. 7--8] studies the exterior/spin action under the same complex semisimple hypotheses. The following example shows why their roles cannot be exchanged.

Take the basis \(e,f,h\) of \(\mathfrak {sl}_2(\mathbb C)\) with \[[h,e]=2e,\qquad [h,f]=-2f,\qquad [e,f]=h.\] The Killing form satisfies \(\kappa (e,f)=4\) and \(\kappa (h,h)=8\). Hence the Clifford relations are \[e^2=f^2=0,\qquad ef+fe=8,\qquad h^2=8,\qquad he=-eh,\quad hf=-fh.\] Substitution in the lift of Proposition [fcap-003E][fcap-003E] gives \[E=\delta (e)=\frac {he}{8},\qquad F=\delta (f)=\frac {fh}{8},\qquad H=\delta (h)=\frac {ef-fe}{8}=\frac {ef}{4}-1.\] Direct Clifford multiplication yields \[E^2=F^2=0,\qquad H^2=1,\qquad EF=\frac {1+H}{2},\qquad FE=\frac {1-H}{2}.\] Thus \(E,F,EF,FE\) are the four matrix units of the lifted \(\mathfrak {sl}_2\) action.

For left multiplication, the \(H=+1\) and \(H=-1\) subspaces are interchanged by \(F\) and \(E\); the two maps are inverse on the corresponding projected spaces because \(EF\) and \(FE\) are their identity projectors. They have equal dimension, and \(\dim \mathcal {C}\kern -2pt\ell (Q_\kappa )=8\), so each has dimension four. Choosing a basis of the positive space and its \(F\)-images displays \[(\mathcal {C}\kern -2pt\ell (Q_\kappa ),L)\simeq 4V_1,\] four copies of the standard two-dimensional module.

For the commutator action \(D\), antisymmetrization identifies the same vector space with \(\bigwedge \mathfrak {sl}_2\). The exterior powers are \[\bigwedge ^0\mathfrak g\simeq V_0,\qquad \bigwedge ^1\mathfrak g\simeq V_2,\qquad \bigwedge ^2\mathfrak g\simeq V_2,\qquad \bigwedge ^3\mathfrak g\simeq V_0,\] where the middle identification uses the bracket and the last uses the invariant volume. Therefore \[(\mathcal {C}\kern -2pt\ell (Q_\kappa ),D)\simeq 2V_0\oplus 2V_2.\] The dimensions agree but the characters do not. [kostant1997clifford, Theorem 39, pp. 312--313] gives the first answer through Kostant's primary-type theorem. [panyushev2001exterior, Example 2.5(1), internal preprint p. 8] independently gives the exterior decomposition. The displayed matrix-unit calculation directly verifies which action produces which answer.

Let \(\mathfrak g\) be a finite-dimensional complex semisimple Lie algebra of rank \(\ell \). Choose positive roots \(\Phi ^+\), put \(r=\lvert \Phi ^+\rvert \), and write \(\rho =\frac 12\sum _{\alpha >0}\alpha \). Then \[\dim \mathfrak g=\ell +2r.\] Give \(\mathcal {C}\kern -2pt\ell (Q_\kappa )\) the left action \(L\) of Proposition [fcap-003E][fcap-003E]. As a \(\mathfrak g\)-module it is \[\mathcal {C}\kern -2pt\ell (Q_\kappa )\simeq 2^{\ell +r}V_\rho .\] Here the exponent is the multiplicity; \(\dim V_\rho =2^r\), so the total dimension is \(2^{\ell +2r}\), as required. For the zero Lie algebra this reads as the one-dimensional trivial module.

First compute the spinor constituent. The weights of the adjoint orthogonal module are zero with multiplicity \(\ell \) and the roots in opposite pairs. The exterior spinor character is therefore \[\operatorname {ch}S= 2^{\lfloor \ell/2\rfloor } \prod _{\alpha >0} \left (e^{\alpha/2}+e^{-\alpha/2}\right ).\] The Weyl character formula for highest weight \(\rho \), together with the Weyl denominator identity applied to \(2\rho \) and divided by the ordinary denominator, gives \[\operatorname {ch}V_\rho =e^\rho \prod _{\alpha >0}(1+e^{-\alpha }) =\prod _{\alpha >0} \left (e^{\alpha/2}+e^{-\alpha/2}\right ).\] Complete reducibility and independence of irreducible characters now give \[S\simeq 2^{\lfloor \ell/2\rfloor }V_\rho .\] [panyushev2001exterior, Example 2.5(1), internal preprint p. 8] records this adjoint specialization under the complex semisimple hypotheses. The character calculation above supplies the comparison in the fixed normalization rather than substituting that conclusion without proof.

It remains to pass from a spinor carrier to the full Clifford algebra. If \(n=\ell +2r\) is even, the matrix range of Theorem [fcap-002V][fcap-002V] gives \[\mathcal {C}\kern -2pt\ell (Q_\kappa )\simeq \operatorname {End}(S)\simeq S\otimes S^*.\] Left multiplication acts on the first factor, so \(S^*\) is a trivial multiplicity space of dimension \(2^{n/2}\). If \(n\) is odd, the odd structure of Proposition [fcap-002W][fcap-002W] gives two matrix blocks \(\operatorname {End}(S_1)\oplus \operatorname {End}(S_2)\). The two full Clifford actions differ, but their restrictions to the even algebra are equivalent; since \(\delta (\mathfrak g)\) is even, both blocks contain the same \(\mathfrak g\)-module. Their combined multiplicity-space dimension is \(2\cdot 2^{(n-1)/2}=2^{\lceil n/2\rceil }\).

In both parity cases the multiplicity of \(V_\rho \) is \[2^{\lceil n/2\rceil } 2^{\lfloor \ell/2\rfloor } =2^{\ell +r}.\] This proves the displayed decomposition. [kostant1997clifford, Theorem 39, pp. 312--313] independently proves the exact left-regular primary-type statement by a highest-weight right ideal. TauCeti formalizes the selected left action and its commuting right multiplications, but the character, matrix-block, and multiplicity synthesis here is not a packaged formal theorem.

The conclusion is a module decomposition only. It does not assert the stronger algebra factorization \(\operatorname {End}(V_\rho )\otimes \mathcal {C}\kern -2pt\ell (P)\), identify the full commutant, or invoke the Hopf--Koszul--Samelson primitive algebra. The normal-ordered \(\mathfrak {gl}_N\) calculation in the separate CAR section uses a trace shift and is not a substitute for this Killing-adjoint theorem.

Let \(\mathfrak g\) be complex semisimple of rank \(\ell \), with \(r\) positive roots and \(\rho \) their half-sum. Put \(A=\mathcal {C}\kern -2pt\ell (Q_\kappa )\), where \(Q_\kappa (x)=\kappa (x,x)\), and use the lift \(\delta \) of Proposition [fcap-003E][fcap-003E]. Define the unital algebra \(E=\delta (U(\mathfrak g))\subseteq A^0\) and the commutator invariants \[J=\{a\in A:[\delta (x),a]=0\text { for every }x\in \mathfrak g\}.\] Then \(J=\operatorname {Cent}_A(E)\), \(E\simeq \operatorname {End}(V_\rho )\), and multiplication is an isomorphism of ordinary complex algebras \[E\otimes J\longrightarrow A,\qquad e\otimes j\longmapsto ej.\] In particular, \(\dim J=2^\ell \). These assertions include the zero Lie algebra, where \(A=E=J=\mathbb C\).

An element commutes with the generators \(\delta (\mathfrak g)\) exactly when it commutes with their unital associative algebra, proving the centralizer assertion. Set \(d=2^{\lfloor \ell /2\rfloor }\). The spinor calculation in Theorem [fcap-003G][fcap-003G] gives \(S\simeq V_\rho \otimes \mathbb C^d\). The associative algebra generated by an irreducible complex representation is its full endomorphism algebra (Burnside's theorem). Thus the image of \(U(\mathfrak g)\) on \(S\) is \(\operatorname {End}(V_\rho )\otimes 1\). This is the primary-representation calculation in [kostant1997clifford, equations (74)--(76), p. 295].

If \(\ell \) is even, then \(\dim \mathfrak g=\ell +2r\) is even, and Theorem [fcap-002V][fcap-002V] identifies \(A\) with \(\operatorname {End}(S)\). Matrix units in \(\operatorname {End}(V_\rho )\) show that its commutant on \(V_\rho \otimes \mathbb C^d\) is \(1\otimes \operatorname {End}(\mathbb C^d)\): commuting with diagonal units forces a block-diagonal operator, and commuting with off-diagonal units makes all its diagonal blocks equal. Consequently \[J\simeq \operatorname {End}(\mathbb C^d),\qquad E\otimes J\simeq \operatorname {End}(V_\rho \otimes \mathbb C^d)=A.\] This also gives \(\dim J=d^2=2^\ell \).

If \(\ell \) is odd, Proposition [fcap-002W][fcap-002W] identifies \(A\) with \(\operatorname {End}(S_+)\oplus \operatorname {End}(S_-)\). The two spinor restrictions to \(A^0\) are equivalent and faithful. After identifying them, \(E\subseteq A^0\) is the diagonal copy of \(\operatorname {End}(V_\rho )\otimes 1\). The same matrix-unit argument in each block gives \[J\simeq \operatorname {End}(\mathbb C^d) \oplus \operatorname {End}(\mathbb C^d).\] Multiplication \(E\otimes J\to A\) is the preceding matrix isomorphism in each of the two summands, and \(\dim J=2d^2=2^\ell \). This proves both parity cases without assuming that the full odd-dimensional Clifford algebra is simple. [kostant1997clifford, Propositions 17--20, pp. 294--297] gives this centralizer factorization for any primary spin representation.

Under the commutator action, \(\mathfrak g\) acts trivially on \(J\) and by conjugation on \(E\). Equivariant antisymmetrization from Proposition [fcap-003E][fcap-003E] therefore yields the exterior-module consequence \[\bigwedge \mathfrak g\simeq 2^\ell (V_\rho \otimes V_\rho ^*).\] This multiplicity concerns the commutator action; the left-action multiplicity in Theorem [fcap-003G][fcap-003G] is \(2^{\ell +r}\). The algebra factorization and its proof here are not a packaged formal theorem.

Keep the hypotheses and notation of Theorem [fcap-003P][fcap-003P], and let \(L_x(c)=\delta (x)c\). The internal centralizer \(J\subseteq A\), the right-multiplication operators on \(A\), and the full algebra of \(\mathfrak g\)-module endomorphisms of \((A,L)\) have distinct roles.

Left multiplication by \(j\in J\) commutes with every \(L_x\). Right multiplication by any \(a\in A\) also commutes with every \(L_x\), purely by associativity. Thus there are injective algebra maps \[J\longrightarrow \operatorname {End}_{\mathfrak g}(A,L), \qquad j\longmapsto (c\longmapsto jc),\] \[A^{\mathrm {op}}\longrightarrow \operatorname {End}_{\mathfrak g}(A,L), \qquad a\longmapsto (c\longmapsto ca).\] Evaluation at \(1\) proves injectivity. The opposite algebra in the second map records the reversed order of right compositions.

By Theorem [fcap-003G][fcap-003G], \((A,L)\simeq V_\rho \otimes \mathbb C^m\) with \(m=2^{\ell +r}\). Schur's lemma and the same block calculation as in Theorem [fcap-003P][fcap-003P] give \[\operatorname {End}_{\mathfrak g}(A,L) \simeq M_m(\mathbb C).\] The dimensions of the three algebras are therefore \[\dim J=2^\ell ,\qquad \dim A^{\mathrm {op}}=2^{\ell +2r},\qquad \dim \operatorname {End}_{\mathfrak g}(A,L)=2^{2\ell +2r}.\] For \(\mathfrak g=\mathfrak {sl}_2\), these are \(2\), \(8\), and \(16\), respectively: \(J\simeq \mathbb C\oplus \mathbb C\), while \(\operatorname {End}_{\mathfrak g}(A,L)\simeq M_4(\mathbb C)\). The four-copy left-module calculation is explicit in Example [fcap-003F][fcap-003F]. For every nonzero complex semisimple \(\mathfrak g\), the dimensions show that right multiplications form a proper subalgebra of the full module commutant. They do not by themselves identify that commutant.

Let \(\mathfrak g\) be finite-dimensional complex semisimple of rank \(\ell \). Write \(I=(\bigwedge \mathfrak g)^{\mathfrak g}\) for the adjoint invariants and \(I^+\) for their positive-degree part. Extend the Killing form \(\kappa \) to the determinant pairing \(\langle -,-\rangle \) on each exterior degree, with different degrees orthogonal. Let \(\pi :\bigwedge \mathfrak g\to I\) be the invariant projection along \(\mathfrak g\mathbin {\cdot }\bigwedge \mathfrak g\), the span of all adjoint derivatives. The coproduct on \(I\) is \[\Delta =(\pi \otimes \pi )\Delta _0|_I,\] where \(\Delta _0(x)=x\otimes 1+1\otimes x\) for \(x\in \mathfrak g\). It is this projected coproduct that defines primitive invariants: \[P=\{p\in I:\Delta p=p\otimes 1+1\otimes p\} =I^+\cap ((I^+)^2)^\perp .\] The ordinary exterior coproduct need not take \(I\) into \(I\otimes I\). The Lie-homology construction makes \(I\), with the displayed \(\Delta \), a graded super Hopf algebra; multiplication on \(I\otimes I\) uses the Koszul rule \((a\otimes b)(c\otimes d)=(-1)^{\lvert b\rvert \lvert c\rvert }ac\otimes bd\) for homogeneous elements. The coproduct is dual to the wedge product. This is the input from [meinrenken2013clifford, Theorem 10.1 and Proposition 10.11, pp. 240--241].

The Hopf--Koszul--Samelson theorem says that inclusion extends to \[\bigwedge P\xrightarrow {\sim }I.\] Here every primitive has odd exterior degree. Indeed, a nonzero homogeneous even primitive \(p\) would have a least nilpotent power \(p^k=0\); the component \(k p\otimes p^{k-1}\) of \(\Delta (p^k)\) could not vanish in characteristic zero. The orthogonal decomposition \(I^+=P\oplus (I^+)^2\) then proves generation: substituting it repeatedly expresses every element as a polynomial in \(P\), since the augmentation ideal is nilpotent. For independence, contraction by a primitive acts as an odd derivation on \(I\), and contraction of two primitives is a scalar. The first assertion is dual to \(\Delta \) preserving multiplication; the second follows from \(P\perp (I^+)^2\). Successive contractions by a dual primitive basis extract the coefficients of an exterior-monomial relation, starting with the largest number of factors. All coefficients vanish. This proves the stated isomorphism; compare [meinrenken2013clifford, Theorem 10.2 and Proposition 10.13, pp. 242--243]. By Theorem [fcap-003P][fcap-003P], \(\dim I=2^\ell \), so \(\dim P=\ell \).

For \(x\in \mathfrak g\), let \(\iota _x\) be contraction using \(\kappa \), and set \(\iota _{x_1\wedge \cdots \wedge x_k}=\iota _{x_1}\cdots \iota _{x_k}\). Exterior reversion is \(\operatorname {rev}(u)=(-1)^{k(k-1)/2}u\) on degree \(k\). The form relevant to Clifford multiplication is \[B_\wedge (u,v)=(\iota _u v)_0 =\langle \operatorname {rev}(u),v\rangle ,\qquad Q_P(p)=B_\wedge (p,p).\] In particular, on primitive degree \(2m+1\), \(B_\wedge (p,q)=(-1)^m\langle p,q\rangle \). The Clifford polar relation for \(Q_P\) is therefore \(pq+qp=2B_\wedge (p,q)\), with the same generator-square convention as \(Q_\kappa (x)=\kappa (x,x)\).

This restriction of \(B_\wedge \) to \(P\) is nondegenerate. Choose a compact real form. Its Killing form is negative definite; on exterior degree \(k\), the determinant pairing is \((-1)^k\) times a positive definite real form. The subspace \(P\) is graded and preserved by compact conjugation, so the determinant pairing and its degreewise sign multiple \(B_\wedge \) are nondegenerate there. This also explains the normalization change from [meinrenken2013clifford, Section 11.3, p. 260], which starts with a positive compact form. Replacing that form by its negative preserves the graded orthogonal subspaces while changing the indicated degree signs.

With \(P,Q_P\) as in Theorem [fcap-003R][fcap-003R], put \(A=\mathcal {C}\kern -2pt\ell (Q_\kappa )\) and \(J=A^{\mathfrak g}\) for the commutator invariants of Theorem [fcap-003P][fcap-003P]. Let \(q:\bigwedge \mathfrak g\to A\) be antisymmetrization. Then \(p\mapsto q(p)\) extends to an isomorphism of complex superalgebras \[\mathcal {C}\kern -2pt\ell (Q_P)\xrightarrow {\sim }J.\] Consequently multiplication gives \[\operatorname {End}(V_\rho )\otimes \mathcal {C}\kern -2pt\ell (Q_P) \xrightarrow {\sim }\mathcal {C}\kern -2pt\ell (Q_\kappa ).\] The endomorphism factor is purely even. Thus the displayed tensor product has the ordinary multiplication as well as the superalgebra interpretation. The proof below establishes the Clifford relation and generation separately.

We use the Lie-homology Hodge decomposition \[\bigwedge \mathfrak g =I\oplus \operatorname {im}d\oplus \operatorname {im}\partial =I\oplus (\mathfrak g\mathbin {\cdot }\bigwedge \mathfrak g),\] orthogonal for \(B_\wedge \). Here \(\partial \) is the Lie-homology boundary and \(d\) is the cohomology differential transported by \(\kappa \). The needed contraction identities are \[\iota _{\operatorname {im}d}I\subseteq \operatorname {im}\partial , \qquad \iota _{\operatorname {im}\partial }I\subseteq \operatorname {im}d,\] \[\ker \partial \wedge \operatorname {im}\partial \subseteq \mathfrak g\mathbin {\cdot }\bigwedge \mathfrak g.\] Proposition 10.8 and Lemmas 10.4--10.5 of [meinrenken2013clifford, pp. 238--239] give these identities. Changing the compact form's sign multiplies contractions and the transported differential by degreewise nonzero scalars, so the displayed ranges and identities also hold for \(\kappa \).

Choose a homogeneous basis \(\tau _a\) of the exterior algebra adapted to the three Hodge summands, and its \(B_\wedge \)-dual basis \(\tau ^a\). For odd \(p\in P\) and \(q'\in P\), the Clifford product formula is \[q^{-1}(q(p)q(q'))= \sum _a\iota _{\tau _a}p\wedge \iota _{\tau ^a}q'.\] This is the contraction expansion in [meinrenken2013clifford, equation (11.10), p. 260]; using the \(B_\wedge \)-dual basis incorporates the reversion signs. Terms indexed by \(\operatorname {im}d\) lie in \(\mathfrak g\mathbin {\cdot }\bigwedge \mathfrak g\) by the two contraction identities and the boundary-product identity. Terms indexed by \(\operatorname {im}\partial \) lie in \(\operatorname {im}d\), because \(d\) is a derivation and the wedge product of two exact elements is exact. Their combined sum is zero: the full product and the terms indexed by \(I\) are invariant, whereas the remaining terms lie in the complementary Hodge summand.

Take a homogeneous basis \(p_1,\ldots ,p_\ell \) of \(P\) and its \(B_\wedge \)-dual basis \(p^1,\ldots ,p^\ell \). The HKS monomials give a basis of \(I\). Repeated primitive contractions of a primitive vanish after the first contraction, which is already scalar. Moreover, \(\mathbb C\oplus P\oplus (I^+)^2\) is orthogonal, so the dual vectors belonging to the single primitives are \(p^i\). Only the constant monomial and the single primitives survive in the preceding sum. Hence \[q^{-1}(q(p)q(q')) =p\wedge q'+\sum _i B_\wedge (p_i,p)B_\wedge (p^i,q') =p\wedge q'+B_\wedge (p,q').\] Both primitives are odd, so swapping them cancels their wedge products and yields \[q(p)q(q')+q(q')q(p)=2B_\wedge (p,q').\] This is Kostant's primitive Clifford relation in the fixed sign convention; see [meinrenken2013clifford, Theorem 11.6 and equation (11.13), pp. 260--261] and [kostant1997clifford, Theorem 35, pp. 306--308].

The universal property now gives a homomorphism \(\mathcal {C}\kern -2pt\ell (Q_P)\to J\). To prove generation, order the HKS monomials by their total exterior degree. The product \(q(p_{i_1})\cdots q(p_{i_s})\) has leading exterior term \(p_{i_1}\wedge \cdots \wedge p_{i_s}\) under \(q^{-1}\); its other terms have lower degree, by the Clifford filtration. They are invariant, hence linear combinations of lower-degree HKS monomials. Induction therefore puts every \(q(p_{i_1}\wedge \cdots \wedge p_{i_s})\) in the generated algebra. This proves surjectivity. Both algebras have dimension \(2^\ell \), so the map is an isomorphism. It preserves parity, since all elements of \(P\) have odd degree.

Finally, substitute this identification of \(J\) in the multiplication isomorphism of Theorem [fcap-003P][fcap-003P]. This yields the claimed factorization, also displayed in [meinrenken2013clifford, equation (11.14), p. 262]. For \(\mathfrak {sl}_2\), \(P\) has dimension one in exterior degree three. As an ordinary algebra, its nondegenerate complex Clifford algebra is \(\mathbb C\oplus \mathbb C\); the underlying ordinary algebra factorization becomes \(M_2(\mathbb C)\oplus M_2(\mathbb C)\), in agreement with Remark [fcap-003Q][fcap-003Q]. The primitive relation, HKS argument, and factorization here are mathematical proofs without a packaged formal theorem.

Let \(K\) be a field in which \(2\) is invertible. On \(V=M_N(K)\) take \[Q_{\mathrm {tr}}(Y)=\operatorname {Tr}(Y^2),\qquad B_{Q_{\mathrm {tr}}}(X,Y)=2\operatorname {Tr}(XY),\] and write \(d_{ij}=\iota _{Q_{\mathrm {tr}}}(E_{ij})\). The Clifford relation is \[d_{ij}d_{kl}+d_{kl}d_{ij} =2\delta _{jk}\delta _{li}.\] Let \(q(X)\) be the quadratic Clifford lift of the adjoint action \(Y\mapsto [X,Y]\). The normal-ordered lift used for the CAR module is \[D(X)=q(X)+\frac N2\operatorname {Tr}(X)1.\] On a matrix unit it has the concrete form \[D(E_{ij})=\frac 12\sum _{k=0}^{N-1}d_{ik}d_{kj}.\] Indeed, \(d_{ik}d_{kj}=\beta _{Q_{\mathrm {tr}}}(E_{ik},E_{kj}) +\delta _{ij}1\); summing the contraction term over \(k\) gives \((N/2)\delta _{ij}1\). This derives both the coefficient and its positive sign.

There are three different actions here. The ordinary exterior extension of the adjoint action is the derivation \[\delta _X(Y_1\wedge \cdots \wedge Y_r) =\sum _sY_1\wedge \cdots \wedge [X,Y_s]\wedge \cdots \wedge Y_r.\] The quadratic Clifford action is the inner derivation \([q(X),-]=[D(X),-]\). The CAR representation on the full Clifford algebra is instead left multiplication, \[\rho _{\mathrm {CAR}}(X)c=D(X)c, \qquad \rho _{\mathrm {CAR}}(X)c-cD(X)=[D(X),c].\] On the central matrix the three formulas read: \[\operatorname {ad}_I=0,\qquad q(I)=0, \qquad D(I)=\frac {N^2}{2}1.\] The left-regular carrier has dimension \(2^{N^2}\). For \(N\geq 1\) it is not an irreducible exterior spinor carrier; \(N=0\) is the one-dimensional trivial exception.

The exact identities are formalized at the pinned TauCeti revision. The normal-ordered lift, its matrix-unit and generator formulas, and the left-action comparison have the field and inverse-two hypotheses stated above. They do not identify this module with an irreducible spinor representation.

[pressley1986loop, Section 12.1, pp. 230--233] let the determinant-square-root cover of \(U(W)\) act on \(\bigwedge ^kW\) by \(u^{-1}\bigwedge ^k(A)\), with \(u^2=\det A\). Differentiating first along a unitary curve gives \(d\bigwedge (X)-\frac 12\operatorname {Tr}_W(X)\) for \(X\in \mathfrak u(W)\); complexifying then gives the corresponding \(\mathfrak {gl}(W)\) formula. No arbitrary complex matrix is being presented as the derivative of a unitary curve.

[panyushev2001exterior, Section 2, Example 2.5(3), preprint pp. 8--9] works over an algebraically closed field of characteristic zero and gives the ordinary spinor correction as \(\mathbb k_{-\nu }\otimes \bigwedge W\), where \(\nu \) is half the sum of the weights with multiplicity. Evaluating \(\nu \) is half the exterior trace. These two sources agree on the ordinary minus-half-trace normalization. They do not produce the positive \((N/2)\operatorname {Tr}\) term above: the trace of \(\operatorname {ad}_X\) on \(M_N\) is zero, while that term is the contraction created by normal ordering on the full left-regular Clifford module.

Let \(K\) be a field in which \(2\) is invertible. Begin with \(N=2\) and put \(v_+=d_{01}\). The relations are \[d_{01}^2=d_{10}^2=0,\qquad d_{00}^2=d_{11}^2=1, \qquad d_{01}d_{10}+d_{10}d_{01}=2.\] The only raising operator is \[D(E_{01})=\frac 12(d_{00}d_{01}+d_{01}d_{11}),\] and each summand kills \(v_+\). For the diagonal operators, the same CAR relations give \[D(E_{00})v_+=\frac 32v_+,\qquad D(E_{11})v_+=\frac 12v_+.\] Thus \(v_+\) has weight \((3/2,1/2)\), and \(D(I)v_+=2v_+\). Subtracting the central correction \((N/2)\operatorname {Tr}\) leaves \((1/2,-1/2)\). In characteristic zero this is the usual \(\mathfrak {sl}_2\) value \(\rho \).

For general \(N\), order the indices as \(0<1<\cdots <N-1\) and form the lexicographically ordered product \[v_+=\prod _{0\leq i<j<N}^{\mathrm {lex}}d_{ij}.\] Every positive matrix unit is \(Q_{\mathrm {tr}}\)-null, and distinct positive matrix units are polar-orthogonal. Their Clifford generators therefore anticommute. PBW linear independence shows that the ordered product is nonzero over a field.

Let \(i<j\). In \[D(E_{ij})v_+=\frac 12\sum _kd_{ik}d_{kj}v_+,\] a term with \(k<j\) vanishes because the positive generator \(d_{kj}\) already occurs in \(v_+\). If \(k\geq j\), then \(i<k\); first anticommute \(d_{ik}\) past \(d_{kj}\), using \(i\ne j\), and the repeated positive factor \(d_{ik}\) makes the term zero. Hence every raising operator annihilates \(v_+\).

For a diagonal generator, \[D(E_{ii})v_+=\frac 12\sum _kd_{ik}d_{ki}v_+.\] The contributions for \(k<i\), \(k=i\), and \(k>i\) are respectively \(0\), \(v_+\), and \(2v_+\). Therefore \[D(E_{ii})v_+ =\frac 12\bigl (1+2|\{k:k>i\}|\bigr )v_+.\] For \(i\in \operatorname {Fin}(N)\), the weight and its quadratic-lift part are \[\lambda _i=N-i-\frac 12,\qquad \lambda _i-\frac N2=\frac {N-1}{2}-i,\qquad \sum _i\lambda _i=\frac {N^2}{2}.\] The last equality agrees with the direct central calculation \(D(I)=N^2/2\).

TauCeti defines this ordered product and proves its nonvanishing, raising equations, and diagonal weight. See the exact pinned product and PBW nonvanishing and half-staircase theorems. Nonvanishing needs a field; the highest-vector statement adds invertible \(2\). Identifying the subtracted weight with the rational staircase requires characteristic zero.

[panyushev2001exterior, Section 2, Example 2.5(1), preprint p. 8] identifies, over an algebraically closed field of characteristic zero, the reduced adjoint spin module with highest weight \(\rho \). The subtracted weight above is exactly that semisimple staircase. The added \((N/2)\operatorname {Tr}\) character records the reductive center of this normal-ordered left action. This comparison does not attribute the selected product or the full left-regular CAR module to Panyushev, and it makes no irreducibility or whole-module decomposition claim.

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 [fcap-001R][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.

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

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 [fcap-001R][fcap-001R]--Example [fcap-001V][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][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.

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][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][fcap-000R] and whose polar-dual coordinate formula is Theorem [fcap-001Z][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 [fcap-0037][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\).

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][fcap-0039], and write \(b:\mathfrak {so}(n)\to T_1G\) for the quadratic lift of Proposition [fcap-0037][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][fcap-0037] and simple connectedness in Proposition [fcap-003A][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 [fcap-003L][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.\]

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][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][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][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][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][fcap-003L].

Let \(K\) be a commutative ring, let \(V\) be a \(K\)-module, and let \(Q\) be a quadratic form. Polarization data consists of isotropic submodules \(W,W'\subseteq V\), an orthogonal remainder \(L\), and a linear equivalence \[(W\oplus W')\oplus L\simeq V.\] The polar form identifies \(W'\) with \(W^*\); the pairing is separating in both variables. A coordinate \(\ell :L\to K\) is injective and satisfies \(\ell (z)^2=Q(z)\). Thus \(L\) is an orthogonal remainder equipped with an injective coordinate. Over a field it is at most one-dimensional; it vanishes in the classical even split model. The carrier of the exterior spinor model is \[S=\bigwedge _K W.\]

Chevalley treats complementary totally singular subspaces in the split, even-dimensional field case. Meinrenken uses the equivalent Lagrangian model \(V=F^*\oplus F\) [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, pp. 56--57]. The packaged remainder and commutative-ring hypotheses are TauCeti's stated generalization.

Let \(Q\) be a quadratic form on a module \(V\) over a commutative ring \(K\). Write \[B_Q(u,v)=Q(u+v)-Q(u)-Q(v)\] for its unhalved polar form, and reserve \(\iota _Q:V\to \mathcal {C}\kern -2pt\ell (Q)\) for the canonical Clifford generator map. Then \[\iota _Q(u)\iota _Q(v)+\iota _Q(v)\iota _Q(u) =B_Q(u,v)1.\] If \(2\) is invertible, write \(b_Q=\tfrac 12B_Q\); the same relation is then \(\{\iota _Q(u),\iota _Q(v)\}=2b_Q(u,v)1\). No use of \(b_Q\) is made when division by two is unavailable.

For polarization data \(V\simeq (W\oplus W')\oplus L\) and \(S=\bigwedge _K W\), the definitions are in Definition [fcap-001I][fcap-001I]. Write \(\varepsilon _x:S\to S\) for creation, \(a_y=\iota _{\varphi _y}:S\to S\) for contraction, \(\alpha :S\to S\) for parity, \(\lambda _z:S\to S\) for the orthogonal-line action, and \(c(v):S\to S\) for the assembled Clifford operator. In particular, \[a_y\varepsilon _x+\varepsilon _xa_y =B_Q(x,y)\operatorname {id}_S.\] This is the normalization of TauCeti.SpinPolarizationData.contract_wedge; the assembled square \(c(v)^2=Q(v)\operatorname {id}_S\) is TauCeti.SpinPolarizationData.cliffordOperator_sq. The contracted notation \(\iota _y\) in Lemma [fcap-001J][fcap-001J] and Example [fcap-001P][fcap-001P] is a legacy alias for \(a_y=\iota _{\varphi _y}\); it does not denote the generator map \(\iota _Q\).

The source conventions translate as follows. Fulton--Harris use a symmetric bilinear form \(Q_{\mathrm {FH}}\) and write the anticommutator as \(2Q_{\mathrm {FH}}\); their contraction functional is also \(2Q_{\mathrm {FH}}(-,w')\) [fulton2004representation, Section 20.1, (20.1), Lemma 20.9 and (20.11), pp. 301, 304--305]. Meinrenken likewise starts from \(B\) with Clifford relation \(2B\) and, after choosing \(V=F^*\oplus F\), acts on \(\bigwedge F^*\) by creation from \(F^*\) and contraction from \(F\) [meinrenken2013clifford, Section 3.2.1--3.2.2, Proposition 3.5, pp. 55--57]. Thus \(Q_{\mathrm {FH}}=B=b_Q\) whenever \(b_Q\) exists. Goodman--Wallach instead name the anticommutator form \(\beta \); under their identification \(W_{\mathrm {GW}}^*=W\) and \(W_{\mathrm {GW}}=W'\), one has \(\beta =B_Q\) [goodman2009symmetry, Definition 6.1.1 and Theorem 6.1.3, proof, pp. 302, 304--305]. The formulas agree after these substitutions; the different letters do not signal different Clifford actions.

Let \(P\) be polarization data as in Definition [fcap-001H][fcap-001H], over a commutative ring \(K\), and set \(S=\bigwedge _K W\). For \(x\in W\), creation is exterior multiplication \[\varepsilon _x(s)=x\wedge s.\] For \(y\in W'\), let \(\varphi _y(x)=B_Q(x,y)\). Annihilation is contraction against this functional, \[a_y(s)=\iota _{\varphi _y}(s).\] If \(z\in L\), its operator is \[\lambda _z=\ell (z)\,\alpha ,\] where \(\alpha (s)=(-1)^r s\) for homogeneous \(s\in \bigwedge ^r W\). The Clifford operator attached to the decomposed vector \(v=x+y+z\) is therefore \[c(v)=\varepsilon _x+a_y+\lambda _z.\]

These symbols separate three maps that sources often denote similarly. The canonical generator map is \(\iota _Q:V\to \mathcal {C}\kern -2pt\ell (Q)\); the representation then satisfies \[\rho (\iota _Q(x))=\varepsilon _x,\qquad \rho (\iota _Q(y))=a_y,\qquad \rho (\iota _Q(z))=\lambda _z.\] Thus contraction is an operator on \(S\), not another use of the symbol for the Clifford generator. The normalization and source dictionary are fixed in Convention [fcap-0027][fcap-0027].

Chevalley obtains creation and contraction from left multiplication on a minimal ideal: one totally singular summand acts by exterior multiplication, and the complementary summand by antiderivations [chevalley1954algebraic, II.2.1--II.2.2, pp. 42--44]. Meinrenken's Lagrangian-complement construction gives the same pair as \(\varepsilon (\mu )+\iota (v)\) [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, p. 57]. Fulton--Harris independently writes the two actions as exterior multiplication and derivation, with the derivation paired by their anticommutator form [fulton2004representation, Section 20.1, Lemma 20.9 and (20.11), pp. 304--305]. Fulton--Harris and Goodman--Wallach extend the model in odd dimension by sending a normalized orthogonal generator to parity [fulton2004representation, Lemma 20.16, p. 306], and [goodman2009symmetry, Theorem 6.1.3, proof, p. 305]. TauCeti packages this last step as the supplied coordinate \(\ell :L\to K\), so that every \(z\in L\) acts by \(\ell (z)\alpha \). Chevalley's cited result is the field case of maximal index; Meinrenken assumes a field of characteristic different from two, a split form, and a chosen Lagrangian complement; Fulton--Harris and Goodman--Wallach work with finite-dimensional nondegenerate complex spaces and chosen maximal isotropics. Once \(P\) is supplied, the four displayed TauCeti operators require no additional field, finite-dimensionality, nondegeneracy, or division-by-two hypothesis.

Creation and contraction satisfy \[\iota _y\varepsilon _x+\varepsilon _x\iota _y =B_Q(x,y)\operatorname {id}_S.\] Creation and contraction each square to zero. Parity anticommutes with both, while \(\lambda _z^2=Q(z)\operatorname {id}_S\). Consequently the operator \(c(v)\) assembled from the three polarization coordinates obeys \[c(v)^2=Q(v)\operatorname {id}_S.\] This is the quadratic form of the usual polarized anticommutation relation \(c(v)c(w)+c(w)c(v)=B_Q(v,w)\). Meinrenken states the latter as the defining condition for a Clifford module.

The square relation of Lemma [fcap-001J][fcap-001J] extends uniquely to an algebra homomorphism \[\rho :\mathcal {C}\kern -2pt\ell (Q)\longrightarrow \operatorname {End}_K(S).\] On the three summands it is determined by \[\rho (\iota (x))s=x\wedge s,\qquad \rho (\iota (y))s=\iota _y(s),\qquad \rho (\iota (z))s=\ell (z)\alpha (s).\] The corresponding formalized equations are TauCeti.spinAction_ι_wedge, TauCeti.spinAction_ι_contract, and TauCeti.spinAction_ι_lineOperator. Chevalley's split even-dimensional model has no remainder term; the third formula is TauCeti's odd-line extension of that construction.

Assume that \(W\) is finite and free over the commutative ring \(K\). The subalgebra of \(\operatorname {End}_K(\bigwedge W)\) generated by all creation operators and all contractions is the whole endomorphism algebra. Since the polar pairing identifies \(W'\) with \(W^*\), these generators lie in the image of the exterior Clifford action. Hence \[\rho :\mathcal {C}\kern -2pt\ell (Q)\twoheadrightarrow \operatorname {End}_K(\bigwedge W)\] is surjective.

Meinrenken proves generation first in rank one by four matrix units and then by tensor decomposition. Over a split field he combines surjectivity with a dimension calculation to obtain an isomorphism and irreducibility. TauCeti formalizes the generation and surjectivity statements over a finite free module. This card does not claim that \(S\) is irreducible, or that \(\rho \) is injective.

The groups \(\operatorname {Spin}(Q)\) and \(\operatorname {Pin}(Q)\) consist of units in the Clifford algebra. Restricting the action \(\rho \) of Theorem [fcap-001K][fcap-001K] along these two inclusions gives representations on the same exterior carrier: \[\operatorname {spinRep}:\operatorname {Spin}(Q)\longrightarrow \operatorname {Aut}_K(S), \qquad \operatorname {pinRep}:\operatorname {Pin}(Q)\longrightarrow \operatorname {Aut}_K(S).\] Meinrenken calls the restriction of a Clifford module to the Clifford group the spin representation. The definitions here require only the commutative ring, module, quadratic form, and polarization data already used for \(\rho \); no nondegeneracy or finite-dimensionality is added.

For every \(g\in \operatorname {Spin}(Q)\) and \(h\in \operatorname {Pin}(Q)\), the two representations act through their underlying Clifford units: \[\operatorname {spinRep}(g)=\rho (g),\qquad \operatorname {pinRep}(h)=\rho (h).\] Thus the group actions introduce no new formula on \(S\); they are the same Clifford action with a smaller domain. In particular, any equation proved for the action of the underlying Clifford element applies to its Spin or Pin restriction.

Let \(K\) be a commutative ring in which \(2\) is invertible, and consider polarization data for which \(W=Ke\) is free of rank one. Let \(e'\in W'\) be the dual vector, so \(B_Q(e,e')=1\). Following Convention [fcap-0027][fcap-0027], put \(c=\varepsilon _e\) and \(a=a_{e'}=\iota _{e'}\); the last expression uses the legacy contraction notation. In the ordered basis \((1,e)\) of \(S=\bigwedge W\), \[c=\begin {pmatrix}0&0\\1&0\end {pmatrix}, \qquad a=\begin {pmatrix}0&1\\0&0\end {pmatrix}.\] Thus \(c^2=a^2=0\), \(ca+ac=I_2\), and \[ac=\begin {pmatrix}1&0\\0&0\end {pmatrix}=E_{00}, \quad a=E_{01},\quad c=E_{10},\quad ca=\begin {pmatrix}0&0\\0&1\end {pmatrix}=E_{11}.\] These are all four matrix units of \(\operatorname {End}_K(S)\).

The product \[N:=ca\] is the one-mode number operator: \(N(1)=0\) and \(N(e)=e\). Centering its two eigenvalues gives \[H:=N-\tfrac 12 I_2 =\begin {pmatrix}-\tfrac 12&0\\0&\tfrac 12\end {pmatrix}.\] In several modes, \(N_i=c_i a_i\) tests whether the \(i\)-th exterior coordinate is occupied, and \(H_i=N_i-\frac 12\) is the diagonal operator used in Theorem [fcap-0025][fcap-0025].

Over his characteristic-not-two field, Meinrenken supplies the general creation--contraction exterior model [meinrenken2013clifford, Proposition 3.5, p. 57] and the normal-ordered isomorphism onto the full endomorphism space [meinrenken2013clifford, Remark 3.5 and (3.6), p. 60]. The four matrices above are the direct rank-one specialization made here. The centered occupation operator independently appears in the Fulton--Harris calculation [fulton2004representation, Proposition 20.15, proof, pp. 305--306].

The occupation identity for every exterior basis vector is TauCeti.SpinPolarizationData.wedge_contract_dualVector_basis, and the general finite-free statement that the Clifford action reaches every endomorphism is TauCeti.spinAction_surjective. The displayed \(2\times 2\) matrices and their labels \(E_{rs}\) are a basis calculation, not separately named formal declarations.

Let \(K\) be a field of characteristic different from \(2\), and let \(V\) be a finite-dimensional split quadratic space with a chosen polarization \(V=W\oplus W'\) into complementary isotropic subspaces. Put \(\dim _KW=\ell \), choose polar-dual bases \(e_i\in W\) and \(e_i'\in W'\) with \(B_Q(e_i,e_j')=\delta _{ij}\), and set \(S=\bigwedge W\). In the notation of Convention [fcap-0027][fcap-0027], write \[c_i=\varepsilon _{e_i},\qquad a_i=a_{e_i'},\qquad N_i=c_i a_i,\qquad P_0=\prod _i(1-N_i)=\prod _i a_i c_i.\] The commuting idempotents \(N_i\) record occupation, so \(P_0\) is the projection onto the vacuum line \(K1\). For increasing subsets \(I=\{i_1<\cdots <i_p\}\) and \(J=\{j_1<\cdots <j_q\}\), put \[c_I=c_{i_1}\cdots c_{i_p},\qquad a_J=a_{j_q}\cdots a_{j_1},\qquad F_{I,J}=c_IP_0a_J.\] The reversed contraction order is essential. If \(e_K\) denotes the increasing exterior basis vector, then \[F_{I,J}(e_K)=\delta _{J,K}e_I,\qquad F_{I,J}F_{K,L}=\delta _{J,K}F_{I,L}.\] Indeed, \(a_J(e_J)=1\). A missing index makes the contraction zero, while a properly larger \(K\) leaves positive exterior degree and is killed by \(P_0\). Finally \(c_I(1)=e_I\). Thus the \(F_{I,J}\) are all matrix units in the image of the Clifford action. This is the multimode extension of the rank-one calculation in Example [fcap-001P][fcap-001P].

The matrix units prove surjectivity, and the dimension equality \[\dim _K\mathcal {C}\kern -2pt\ell (Q)=2^{2\ell }=(2^\ell )^2 =\dim _K\operatorname {End}_K(S)\] then proves injectivity. Hence \[\mathcal {C}\kern -2pt\ell (Q)\simeq \operatorname {End}_K(S).\] This full equivalence is formalized by TauCeti.spinAction_bijective and TauCeti.SpinPolarizationData.cliffordEquivEnd. The displayed multi-index matrix units are the basis calculation supplied here, not a separately named declaration.

Every factor in \(P_0\) is even, so the Clifford parity of \(F_{I,J}\) is \(|I|+|J|\) modulo \(2\). The even matrix units are therefore exactly those with \(|I|\equiv |J|\pmod {2}\); they span the two diagonal blocks and give \[\mathcal {C}\kern -2pt\ell (Q)^0\simeq \operatorname {End}_K(S^+)\oplus \operatorname {End}_K(S^-),\qquad S^+=\bigwedge ^{\mathrm {even}}W,\quad S^-=\bigwedge ^{\mathrm {odd}}W.\] The exact formal block equivalence is TauCeti.SpinPolarizationData.evenCliffordEquivProdEnd. If \(\ell \geq 1\), each block has size \(2^{\ell -1}\) and each parity summand is simple for its full endomorphism block TauCeti.SpinPolarizationData.evenCliffordEquivProdMatrix. For \(\ell =0\), the full action still identifies \(K\) with \(\operatorname {End}_K(K)\), but \(S^-=0\) and is not called a simple summand.

At the group level, the block calculation alone does not prove irreducibility after restriction to \(\operatorname {Spin}(Q)\). When \(K\) is additionally separably closed and \(\ell \geq 1\), the formal Spin-spanning argument gives the two irreducible half-spin representations TauCeti.isIrreducible_spinPlusSubrep TauCeti.isIrreducible_spinMinusSubrep. This is stronger input than the occupation weights of Theorem [fcap-0025][fcap-0025].

[fulton2004representation, Lemma 20.9 and (20.13), pp. 304--305] derive the full complex action and its two exterior-parity blocks; their bilinear form is the half-polar form \(b_Q\), so their contraction coefficient \(2Q_{\mathrm {FH}}\) is our \(B_Q\).

[meinrenken2013clifford, Section 3.2.4, Theorem 3.3 and (3.5)--(3.6), pp. 59--60] give the split action as a superalgebra isomorphism and prove it by the rank-one tensor calculation; their creation space \(F^*\) is our \(W\) and their bilinear form is \(b_Q\).

[goodman2009symmetry, Theorem 6.1.3, proof, pp. 304--305] independently obtain the complex creation--contraction carrier; their creation space \(W_{\mathrm {GW}}^*\) is our \(W\), and their form \(\beta \) is our unhalved \(B_Q\). The formula \(F_{I,J}=c_IP_0a_J\) synthesizes these arguments in the fixed FCAP order rather than quoting one source verbatim.

Work over \(\mathbb C\) with \(V=W\oplus W'\oplus \mathbb C z\), where \(W,W'\) are polar-dual isotropic spaces of dimension \(\ell \), \(z\) is orthogonal to them, and \(Q(z)=1\). On \(S=\bigwedge W\), the two Clifford actions agree on \(W\oplus W'\) and differ on the last generator: \[\rho _+(\iota _Q(z))=\alpha ,\qquad \rho _-(\iota _Q(z))=-\alpha ,\] where \(\alpha \) is exterior parity. For polar-dual bases, normalize the hyperbolic chirality element by \[\Gamma =\prod _{i=1}^{\ell } \bigl (1-2\iota _Q(e_i)\iota _Q(e_i')\bigr ).\] The even-dimensional action sends \(\Gamma \) to \(\prod _i(1-2N_i)=\alpha \). Moreover \(\Gamma ^2=1\), and \(\Gamma \) anticommutes with every hyperbolic vector. Consequently \[\chi =\Gamma \iota _Q(z),\qquad \chi ^2=1\] is central in \(\mathcal {C}\kern -2pt\ell (Q)\). The complementary central idempotents \[p_+=\frac {1+\chi }{2},\qquad p_-=\frac {1-\chi }{2}\] satisfy \[\rho _+(p_+)=1,\quad \rho _+(p_-)=0,\qquad \rho _-(p_+)=0,\quad \rho _-(p_-)=1.\] Thus each odd action has a visible nonzero kernel.

The central idempotents also identify the whole algebra, rather than only showing a dimension mismatch. Given \(A\in \operatorname {End}_{\mathbb C}(S)\), the preceding theorem supplies a hyperbolic Clifford element \(a\) with common image \(A\). Therefore the joint map obeys \[(\rho _+,\rho _-)(p_+a)=(A,0),\qquad (\rho _+,\rho _-)(p_-a)=(0,A).\] It is surjective. Since \[\dim _{\mathbb C}\mathcal {C}\kern -2pt\ell (Q)=2^{2\ell +1} =2\dim _{\mathbb C}\operatorname {End}_{\mathbb C}(S),\] it is an isomorphism \[\mathcal {C}\kern -2pt\ell (Q)\simeq \operatorname {End}_{\mathbb C}(S)\oplus \operatorname {End}_{\mathbb C}(S).\] The corresponding abstract two-block existence theorem is CliffordAlgebra.nonempty_algEquiv_matrix_prod_of_finrank_eq_two_mul_add_one. The explicit joint-map proof determines how the two actions select its summands.

The restrictions \(\rho _+|_{\mathcal {C}\kern -2pt\ell (Q)^0}\) and \(\rho _-|_{\mathcal {C}\kern -2pt\ell (Q)^0}\) are parity-conjugate. When \(\ell \geq 1\) they are unequal, as the Spin element below shows; for \(\ell =0\) both are the same scalar action. For every even Clifford word, the number of hyperbolic factors has the same parity as the number of \(z\)-factors. Conjugation by \(\alpha \) contributes exactly that sign, so \[\rho _-(x)=\alpha \rho _+(x)\alpha ^{-1} \qquad (x\in \mathcal {C}\kern -2pt\ell (Q)^0).\] If \(\rho _+(x)=0\), conjugacy makes both coordinates of the joint isomorphism zero, hence \(x=0\). The even source and target have the same dimension, so either restriction is an isomorphism \[\mathcal {C}\kern -2pt\ell (Q)^0\simeq \operatorname {End}_{\mathbb C}(S).\] This faithful range is formalized by TauCeti.evenSpinAction_surjective and TauCeti.SpinPolarizationData.evenCliffordEquivEnd.

When \(\ell \geq 1\), exterior parity is not a decomposition into invariant odd-dimensional Spin modules. Fix \(i\), put \(u=e_i+e_i'\), and note \(Q(u)=Q(z)=1\). The even product \[g=\iota _Q(z)\iota _Q(u)\in \operatorname {Spin}(Q)\] belongs to the actual Spin carrier by the norm-one pair criterion CliffordAlgebra.ι_mul_ι_mem_spinGroup_of_norm_mul_norm_eq_one. Its plus action is \(\alpha (c_i+a_i)\) and satisfies \[1\longmapsto -e_i,\qquad e_i\longmapsto 1.\] Its minus action is the negative of this operator. Thus the two even restrictions are unequal, and this actual Spin element exchanges even and odd exterior degree. For \(\ell =0\), the carrier \(S\) is one-dimensional and \(S^-=0\); no two-summand parity claim is made.

[fulton2004representation, Lemma 20.16 and (20.18), p. 306] give the odd complex product algebra and the faithful even restriction. Their second full-Clifford module is written on \(\bigwedge W'\), rather than as a second sign on the same carrier.

[goodman2009symmetry, Theorem 6.1.3, proof, pp. 304--305] construct the exterior carrier. [goodman2009symmetry, Lemma 6.1.4(3), p. 306] put the two normalized odd-vector signs on this common carrier. This supplies the common-carrier translation used above.

[meinrenken2013clifford, Section 3.2.4, (3.5), p. 60] supplies the normalized chirality product on the hyperbolic block. His Theorem 3.3 is an even split theorem, not an odd product theorem. The two-idempotent conclusion here is restricted to the split complex setting; an odd Clifford center over a general real field need not split.

Let \(W=\mathbb C^m\), \(m\geq 1\), with ordered basis \(e_1,\ldots ,e_m\), and use the exterior action on \(S=\bigwedge W\) from Theorem [fcap-002V][fcap-002V]. Write \([u]_{\mathrm {top}}\) for the coefficient of \(e_1\wedge \cdots \wedge e_m\), and let \(r\) reverse exterior products: \(r|_{\wedge ^kW}=(-1)^{k(k-1)/2}\). Then \[B(s,t)=[r(s)\wedge t]_{\mathrm {top}},\qquad B(t,s)=\epsilon _e B(s,t),\qquad \epsilon _e=(-1)^{m(m-1)/2}\] defines a nondegenerate complex bilinear Spin-invariant form in dimension \(2m\). It pairs complementary degrees. Hence for even \(m\) it restricts nondegenerately to each half-spin module; for odd \(m\) it pairs the two halves perfectly and vanishes on either half alone. In dimension \(2m+1\), use the odd action Proposition [fcap-002W][fcap-002W] and the adjusted form \[B_o(s,t)=B(\alpha ^m s,t),\qquad B_o(t,s)=\epsilon _o B_o(s,t),\qquad \epsilon _o=(-1)^{m(m+1)/2},\] where \(\alpha |_{\wedge ^kW}=(-1)^k\). This form is again nondegenerate and Spin-invariant.

In the exterior basis the matrix of \(B\) has one entry \(\pm 1\) in each row and column, pairing an index set with its complement; this proves nondegeneracy. The underlying perfect wedge pairing has the formal counterpart exteriorPower.instIsPerfPairWedgePairing, for complementary exterior powers of a finite free module over a commutative ring with a chosen top-degree trivialization. Reversal supplies the additional signs here. For degrees \(k\) and \(m-k\), commuting the two wedge factors and comparing their reversal signs gives \(\epsilon _e\). Also \(B(\alpha s,t)=(-1)^mB(s,\alpha t)\), proving the stated odd flip sign.

Every creation and contraction operator is self-adjoint for \(B\): \[B(c_i s,t)=B(s,c_i t),\qquad B(a_i s,t)=B(s,a_i t).\] For creation, \(r(e_i\wedge s)=r(s)\wedge e_i\). For contraction on degree \(k\), \(r(a_i s)=(-1)^{k-1}a_i r(s)\). Apply the contraction derivation rule to \(r(s)\wedge t=0\) in degree \(m+1\); its two terms give the second identity. All other degree combinations vanish on both sides. Thus \(B(\rho (x)s,t)=B(s,\rho (\operatorname {rev}x)t)\). The reverse-norm-one condition in Remark [fcap-0028][fcap-0028] proves invariance under the actual Spin group. For \(B_o\), every hyperbolic vector has adjoint sign \((-1)^m\), because it anticommutes with \(\alpha \); the extra generator \(\alpha \) has the same sign. These signs cancel on even words, giving the same reversion identity and Spin invariance.

These bilinear forms also determine conjugate-linear structures for the compact real form \(\operatorname {Spin}(n,0)\), where \(n=2m\) or \(2m+1\). Give \(S\) the positive Hermitian form \(H(s,t)=\overline {s}^{\,T}t\) in the exterior basis, conjugate-linear in its first argument. The operators \(c_i+a_i\), \(i(c_i-a_i)\), and, in odd dimension, \(\alpha \), are self-adjoint, square to \(1\), and anticommute pairwise. They realize the positive real Clifford generators. Consequently reversion is Hermitian adjunction on this real algebra, and \(H\) is Spin-invariant.

Let \(M\) be the real signed permutation matrix of \(B\) or \(B_o\), and let \(\epsilon \) be its flip sign. Then \[J(s)=M^T\overline {s},\qquad H(Js,t)=s^TMt,\qquad J^2=\epsilon \,1.\] Indeed, \(M^T=\epsilon M\) and \(MM^T=1\). Invariance of both forms and nondegeneracy of \(H\) imply that \(J\) commutes with compact Spin. Writing \(\mathcal B\) for the chosen bilinear form, the comparison is the following commuting triangle of complex linear maps:

For \(\epsilon =1\), \(J\) is a real structure as in Example [fcap-003W][fcap-003W], and its fixed vectors form a real Spin module whose complexification is \(S\) Representation.IsRealStructure.isRealForm. Explicitly, \[s=\frac {s+Js}{2}+i\frac {s-Js}{2i},\] with both displayed components fixed by \(J\). For \(\epsilon =-1\), \(J\) is a quaternionic structure: a conjugate-linear equivariant map squaring to \(-1\) Representation.IsQuaternionicStructure. It has no nonzero fixed vector; together with multiplication by \(i\) it gives the quaternion relations on the underlying real space.

To apply this to irreducible compact spinors, the restriction to Spin needs justification. Every even monomial in an orthonormal positive real Clifford basis has reverse norm one and lies in Spin. Such monomials span the real even algebra, hence their complex span is the complex even algebra. Therefore the block descriptions in Theorem [fcap-002V][fcap-002V] and Proposition [fcap-002W][fcap-002W] give irreducible compact half-spin modules in even dimension and an irreducible compact spin module in odd dimension. The even-dimensional halves are inequivalent because their two matrix blocks have different central supports.

In even dimension \(n=2m\), \(J\) preserves each half when \(m\) is even and exchanges them when \(m\) is odd. In the latter case no equivariant conjugate-linear bijection of one half to itself can exist: composing it with \(J\) would give a complex linear equivalence between the inequivalent halves. Thus the compact types follow directly from the two flip signs: \[\begin {array}{c|c} n\bmod 8&\text {type of an irreducible complex spinor}\\\hline 0,1,7&\text {real}\\ 3,4,5&\text {quaternionic}\\ 2,6&\text {two conjugate, inequivalent half-spin modules} \end {array}\] In the even rows the statement applies to each half-spin module. The general passage from an invariant nondegenerate complex bilinear form, symmetric or alternating, and a supplied positive definite invariant Hermitian form to a real or quaternionic structure is formalized, for finite-dimensional irreducible complex representations, by Representation.exists_isRealStructure_of_isInvariantForm_of_isInvariantSesqForm and Representation.exists_isQuaternionicStructure_of_isInvariantForm_of_isInvariantSesqForm. The explicit \(M\), odd adjustment, and compact residue calculation are the exterior-basis proof above.

The reversal pairing and its covariance are [meinrenken2013clifford, Section 3.4, Definition 3.6, Example 3.5, and Proposition 3.14, pp. 66--67]. The compact reality classification agrees with [lawson2016spin, Chapter I, items 5.12--5.16, pp. 35--37]. Their negative-square Clifford convention is translated in Proposition [fcap-0042][fcap-0042]. The positive Hermitian argument here is specific to the compact real form; it does not assign the same types to other signatures.

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][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][fcap-0016] with the three rows above recovers the compact module types of Theorem [fcap-0041][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][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][fcap-003M].

Let \(V=W\oplus W'\) be a complex nondegenerate quadratic space of dimension \(2\ell \), with \(\ell \geq 1\). The summands are maximal isotropic and dual under the polar form \(B_Q\). Choose dual bases \(w_i\in W\) and \(w_i'\in W'\) with \(B_Q(w_i,w_j')=\delta _{ij}\). On \(S=\bigwedge W\), write \(u_I\) for the wedge basis vector indexed by \(I\). The even and odd exterior degrees are \(S^+\) and \(S^-\).

The diagonal Clifford bivector of Convention [fcap-000N][fcap-000N] \[\widehat H_i=\beta _Q(w_i,w_i') =\tfrac 12[\iota _Q(w_i),\iota _Q(w_i')]\] has factors acting by \(c_i=\varepsilon _{w_i}\) and \(a_i=a_{w_i'}\) in the notation of Convention [fcap-0027][fcap-0027]. Write \(H_i\) for the resulting endomorphism of \(S\). The relation \(c_i a_i+a_i c_i=1\) gives \[N_i:=c_i a_i,\qquad H_i=N_i-\tfrac 12\operatorname {id}_S.\] Since \(N_i\) projects onto the vectors containing \(i\), \[H_i u_I=\begin {cases} \frac 12 u_I,&i\in I,\\ -\frac 12 u_I,&i\notin I. \end {cases}\] The simultaneous weight space for each sign pattern is the line \(\mathbb C u_I\) TauCeti.spinWeightSpace_spinWeight. The lines with even \(|I|\) sum to \(S^+\), and those with odd \(|I|\) sum to \(S^-\). Each half has dimension \(2^{\ell -1}\), while \(S\) has dimension \(2^\ell \).

For \(\ell =2\), the occupation test gives the complete table \[\begin {array}{c|c|c|c} I&u_I&(H_1,H_2)&\text {summand}\\ \hline \varnothing &1&(-\tfrac 12,-\tfrac 12)&S^+\\ \{1\}&w_1&(\tfrac 12,-\tfrac 12)&S^-\\ \{2\}&w_2&(-\tfrac 12,\tfrac 12)&S^-\\ \{1,2\}&w_1\wedge w_2&(\tfrac 12,\tfrac 12)&S^+ \end {array}\] Every entry is obtained by applying the two rank-one operators of Example [fcap-001P][fcap-001P]; the four displayed lines exhaust \(S\) in this case.

Fulton--Harris use \(B_Q=2Q_{\mathrm {FH}}\), so their standard hyperbolic basis becomes polar-dual here after setting \(w_i=e_i\) and \(w_i'=\frac 12e_{\ell +i}\). Their represented operator is then \(L_{e_i}D_{e_i^*}-\frac 12 I=N_i-\frac 12 I\), assigning the same positive sign to an occupied coordinate [fulton2004representation, Proposition 20.15, proof, pp. 305--306]. Thus their occupation signs and even/odd exterior-degree labels agree with the displayed TauCeti axes.

Goodman--Wallach realize the complex spinor carrier as the exterior algebra of the dual isotropic space [goodman2009symmetry, Theorem 6.1.3, proof, pp. 304--305]. Identify their creation space \(W_{\mathrm {GW}}^*\) with \(W\) here, and their annihilation space \(W_{\mathrm {GW}}\) with \(W'\), taking \(w_i=e_{-i}\) and \(w_i'=e_i\).

The reversed order in [goodman2009symmetry, Lemma 6.2.2 and (6.14), p. 313] gives \[\widehat H_i^{\mathrm {Tau}}=\beta _Q(e_{-i},e_i) =-\widehat H_i^{\mathrm {GW}}.\] Accordingly, their occupied eigenvalue \(-\frac 12\) and unoccupied eigenvalue \(+\frac 12\) negate every pair in the table [goodman2009symmetry, Proposition 6.2.3, proof, pp. 314--315]. The exterior vectors and parity labels remain fixed: \(S^+\) means even \(|I|\), and \(S^-\) means odd \(|I|\). This records the occupation operators, weight lines, and parity decomposition, without a root-system, highest-weight, or irreducibility assertion.

Let \(V=W\oplus W'\) be a complex nondegenerate quadratic space with a chosen split polarization of rank \(\ell \geq 4\). Choose polar-dual bases \(e_i\in W\) and \(e_i'\in W'\) with \(B_Q(e_i,e_j')=\delta _{ij}\), and put \(S=\bigwedge W\). Write \(c_i\) for left creation by \(e_i\), \(a_i\) for contraction by \(e_i'\), \(N_i=c_i a_i\), and \[H_i=N_i-\tfrac 12.\] Thus \(\epsilon _i(H_j)=\delta _{ij}\) fixes the Cartan coordinates, and the occupation signs are those of Theorem [fcap-0025][fcap-0025]. We choose \[\Phi ^+=\{\epsilon _i-\epsilon _j,\ \epsilon _i+\epsilon _j:i<j\}\] and the Borel \(\mathfrak b=\mathfrak h\oplus \bigoplus _{\alpha \in \Phi ^+}\mathfrak g_\alpha \). Equivalently, \(\mathfrak b\) stabilizes the flag \(\langle e_1\rangle \subset \langle e_1,e_2\rangle \subset \cdots \subset W\); in the ordered Witt basis \(e_1,\ldots ,e_\ell ,e_\ell ',\ldots ,e_1'\) it is the upper-triangular Borel.

For the simple roots \(\alpha _i=\epsilon _i-\epsilon _{i+1}\) along the chain and \(\alpha _\ell =\epsilon _{\ell -1}+\epsilon _\ell \) at the fork, take \[\begin {aligned} E_i&=c_i a_{i+1},&F_i&=c_{i+1}a_i && (1\leq i<\ell ),\\ E_\ell &=c_{\ell -1}c_\ell ,& F_\ell &=a_\ell a_{\ell -1}.&& \end {aligned}\] The reversed contraction order in \(F_\ell \) fixes the bracket sign. On an increasing exterior word \(u_I\), a chain operator replaces an occupied \(i+1\) by an absent \(i\), or performs the reverse replacement, with coefficient \(1\); otherwise it gives zero. The fork operators create or remove the final pair, again with coefficient \(1\), when the corresponding occupancy condition holds. The CAR then gives \[[E_i,F_i]=h_i,\qquad h_i=N_i-N_{i+1}\ (i<\ell ),\qquad h_\ell =N_{\ell -1}+N_\ell -1.\] Under the bivector map these are the products \(e_i e_{i+1}'\), \(e_{i+1}e_i'\), \(e_{\ell -1}e_\ell \), and \(e_\ell 'e_{\ell -1}'\). Distinct orthogonal factors contribute no hidden scalar term. TauCeti identifies these exact Clifford representatives with the numbered type-D matrix roots and coroots TauCeti.SpinPolarizationData.typeDQuadraticEquiv_rootGenerator TauCeti.SpinPolarizationData.typeDQuadraticEquiv_cartanGenerator.

It remains to pass from the simple roots to the chosen Borel. Put \[X_{ij}=c_i a_j,\qquad Y_{ij}=c_i c_j\qquad (i<j).\] Their Cartan weights are \(\epsilon _i-\epsilon _j\) and \(\epsilon _i+\epsilon _j\). The identities \[\begin {aligned} [X_{ij},X_{jk}]&=X_{ik},\\ [X_{i,\ell -1},Y_{\ell -1,\ell }]&=Y_{i,\ell },\\ [X_{j,\ell },Y_{i,\ell }]&=Y_{ij} \end {aligned}\] for the indicated distinct ordered indices generate every positive \(X_{ij}\) and \(Y_{ij}\) from the simple operators. These are all positive root spaces of \(\mathfrak {so}(V,Q)\), so their span is the full nilradical \(\mathfrak n^+\). In particular, a vector killed by every \(E_i\) is killed by \(\mathfrak n^+\): brackets and linear combinations preserve its annihilator. This final root-space argument supplies the Borel bridge; the formal file presently proves over \(\mathbb Q\) annihilation by the Lie span of the simple positive generators, without identifying that span with a compatible Borel TauCeti.SpinPolarizationData.typeDSpinSerreRepresentation_positiveSimpleRootLieSpan_le_lieAnnihilator.

Continue with the Cartan and Borel of Proposition [fcap-002X][fcap-002X]. For the increasing exterior basis \(u_I\), set \[\Omega =u_{\{1,\ldots ,\ell \}},\qquad \widehat \Omega =u_{\{1,\ldots ,\ell -1\}}.\] Every positive chain operator kills \(\Omega \) by duplicate creation. It kills \(\widehat \Omega \) either by the same mechanism or, on the final chain edge, because the contracted last coordinate is absent. The positive fork operator kills \(\Omega \) by duplicate creation and \(\widehat \Omega \) because coordinate \(\ell -1\) is already present. The preceding root-space generation therefore makes both vectors highest for \(\mathfrak b\).

Since \(H_i\) has eigenvalue \(+\frac 12\) on an occupied coordinate and \(-\frac 12\) on an unoccupied one, their weights are \[\operatorname {wt}(\Omega ) =\omega _\ell =\tfrac 12(\epsilon _1+\cdots +\epsilon _\ell ),\] \[\operatorname {wt}(\widehat \Omega ) =\omega _{\ell -1} =\tfrac 12(\epsilon _1+\cdots +\epsilon _{\ell -1}-\epsilon _\ell ).\] The first word lies in \(S^+=\bigwedge ^{\mathrm {even}}W\) exactly when \(\ell \) is even, while the second has the opposite parity. Hence, with \(S^\pm \) defined by exterior parity as in Theorem [fcap-0025][fcap-0025], \[\begin {array}{c|cc} &S^+&S^-\\ \hline \ell \text { even}&L(\omega _\ell )&L(\omega _{\ell -1})\\ \ell \text { odd}&L(\omega _{\ell -1})&L(\omega _\ell ) \end {array}\] The parity label is therefore not an independent name for the all-plus weight.

For completeness, each displayed module is irreducible for the type-D Lie action. The commuting \(H_i\) have distinct joint eigenvalues on the one-dimensional lines \(\mathbb C u_I\), so polynomial projections in the \(H_i\) extract a nonzero basis word from any nonzero invariant subspace. The chain operators move occupied coordinates, while the fork pair creates or removes two of them. Their occupancy graph connects all subsets of a fixed parity. The invariant subspace consequently contains every basis word of that parity. This proves irreducibility without identifying it with the separate group-level theorem.

The generator calculation is already defined over \(\mathbb Q\). In the standard model set \(S_{\mathbb Q}=\bigwedge _{\mathbb Q}\mathbb Q^\ell \). The basis map \[\begin {aligned} \mathbb C\otimes _{\mathbb Q}S_{\mathbb Q} &\longrightarrow \bigwedge _{\mathbb C}\mathbb C^\ell ,\\ z\otimes u_I&\longmapsto z u_I. \end {aligned}\] is an equivalence. Every \(E_i\) and \(F_i\) above has matrix entries \(0,1,-1\); the coroot matrices are integral and the \(H_i\) matrices are half-integral. Thus these actions, their annihilation identities, and their weights commute with extension from \(\mathbb Q\) to \(\mathbb C\). A chosen complex polar-dual basis then transports the standard calculation to \(W\oplus W'\). TauCeti proves the two simple-generator annihilation statements and exact fork weights over \(\mathbb Q\) TauCeti.SpinPolarizationData.typeDSpinRep_serreE_exteriorBasis_univ_eq_zero TauCeti.SpinPolarizationData.typeDSpinRep_serreE_exteriorBasis_univ_erase_last_eq_zero TauCeti.SpinPolarizationData.isCartanWeightVector_typeDSpinRep_exteriorBasis_univ TauCeti.SpinPolarizationData.isCartanWeightVector_typeDSpinRep_exteriorBasis_univ_erase_last. The displayed scalar-extension and Borel steps explain how this rational calculation gives the complex highest-weight identities; they do not assert a packaged Lean base-change theorem.

There are also direct highest-vector counterparts over any characteristic-zero field. They use a supplied polarization with no residual line, a basis of \(W\) of rank \(n\geq 4\), and the concrete type-D Cartan and Borel: TauCeti.SpinPolarizationData.isHighestWeightVector_typeDSpinLieRep_exteriorBasis_univ TauCeti.SpinPolarizationData.isHighestWeightVector_typeDSpinLieRep_exteriorBasis_univ_erase_last. With \(n=\ell \), their zero-based Cartan dual-basis indices \(n-1\) and \(n-2\) are our \(\omega _\ell \) and \(\omega _{\ell -1}\), respectively.

The restricted declarations also retain the parity assignment in the table. In even rank, \(\Omega \in S^+\) and \(\widehat \Omega \in S^-\) TauCeti.SpinPolarizationData.isHighestWeightVector_typeDSpinPlusLieRep_exteriorBasis_univ_of_even TauCeti.SpinPolarizationData.isHighestWeightVector_typeDSpinMinusLieRep_exteriorBasis_univ_erase_last_of_even; in odd rank, \(\Omega \in S^-\) and \(\widehat \Omega \in S^+\) TauCeti.SpinPolarizationData.isHighestWeightVector_typeDSpinMinusLieRep_exteriorBasis_univ_of_odd TauCeti.SpinPolarizationData.isHighestWeightVector_typeDSpinPlusLieRep_exteriorBasis_univ_erase_last_of_odd. These assert highest vectors in the indicated modules; the occupancy argument above supplies their irreducibility.

[fulton2004representation, Proposition 20.15 and proof, pp. 305--306] independently identify the two irreducible half-spin modules and give the same parity-dependent fork assignment after the polar-dual rescaling already recorded in Theorem [fcap-0025][fcap-0025]. Their occupied Cartan sign is positive, as it is here.

[goodman2009symmetry, Proposition 6.2.3, pp. 314--315] independently gives the two irreducible modules and their signed half-sum weights. Its creation space is identified with our \(W\), but its occupied Cartan sign is negative. Under \(H_i^{\mathrm {Tau}}=-H_i^{\mathrm {GW}}\) the weights and positive systems both reverse. The exterior-parity labels remain fixed; the assignment of the two fork highest weights to them must be translated with the Cartan sign and Borel.

Let \(V=W\oplus W'\oplus \mathbb C z\) be a nondegenerate quadratic space of dimension \(2\ell +1\), with \(\ell \geq 1\). Assume \(W,W'\) are complementary polar-dual isotropic spaces, \(z\) is orthogonal to both, and \(Q(z)=1\). Choose bases \(e_i,e_i'\) with \(B_Q(e_i,e_j')=\delta _{ij}\) and the plus odd action on \(S=\bigwedge W\), \[\rho (\iota _Q(z))=\alpha ,\] where \(\alpha \) is exterior parity. This sign is part of the choice: \(Q(z)=1\) alone says only that the line coordinate squares to \(1\). Write \(c_i,a_i,N_i,H_i,\epsilon _i\) as in Theorem [fcap-0025][fcap-0025].

Choose the positive roots \[\Phi ^+=\{\epsilon _i-\epsilon _j,\ \epsilon _i+\epsilon _j:i<j\} \cup \{\epsilon _i:1\leq i\leq \ell \}.\] The chain simple roots use \(E_i=c_i a_{i+1}\) and \(F_i=c_{i+1}a_i\). At the terminal short root \(\alpha _\ell =\epsilon _\ell \), take \[E_\ell =c_\ell \alpha ,\qquad F_\ell =\alpha a_\ell ,\qquad [E_\ell ,F_\ell ]=2N_\ell -1.\] The matrix short root has a coefficient \(2\) because \(B_Q(z,z)=2\); the Clifford bivector is nevertheless exactly \(e_\ell z\), with no extra factor \(\frac 12\) TauCeti.SpinPolarizationData.typeBQuadraticEquiv_typeBShortRootGenerator. On an increasing word, the terminal creation or removal sign cancels the parity sign, so the short operators insert or remove coordinate \(\ell \) with coefficient \(1\) TauCeti.SpinPolarizationData.typeBSpinRep_shortRootGenerator_apply TauCeti.SpinPolarizationData.typeBSpinRep_shortNegativeRootGenerator_apply.

This convention gives the same flag Borel as in Proposition [fcap-002X][fcap-002X]. For \(i<j\), put \(X_{ij}=c_i a_j\), \(Y_{ij}=c_i c_j\), and \(K_i=c_i\alpha \). The chain commutators generate every \(X_{ij}\), while \[[X_{ij},K_j]=K_i,\qquad [K_i,K_j]=-2Y_{ij}.\] Because \(2\) is invertible over \(\mathbb C\), the simple chain operators and \(K_\ell \) generate the root spaces of every positive short and long root. They therefore generate the full positive nilradical.

The top word \[\Omega _B=e_1\wedge \cdots \wedge e_\ell \] is killed by each positive chain root and by \(E_\ell \), since the relevant creation coordinate is already occupied. The chain coroots have eigenvalue \(0\), and the terminal coroot \(2N_\ell -1\) has eigenvalue \(1\). Hence \[\operatorname {wt}(\Omega _B) =\omega _\ell =\tfrac 12(\epsilon _1+\cdots +\epsilon _\ell ).\] The chain moves together with the terminal toggle connect all exterior basis words. As in Theorem [fcap-002Y][fcap-002Y], the distinct joint \(H_i\)-weights first project any nonzero invariant subspace onto a basis line; the root moves then reach every line. Thus \(S\) is the irreducible type-\(B_\ell \) module \(L(\omega _\ell )\). The short root changes exterior degree, so neither \(S^+\) nor \(S^-\) is a type-B submodule.

[fulton2004representation, Proposition 20.20, p. 307] independently identifies the odd-dimensional spin representation as the irreducible module of highest weight \(\frac 12(\epsilon _1+\cdots +\epsilon _\ell )\). The preceding short-root and nilradical calculations give that conclusion in the fixed FCAP operator convention.

[goodman2009symmetry, Proposition 6.2.4, p. 315] independently gives the same irreducible type-B module and its half-sign weights. As in Theorem [fcap-0025][fcap-0025], its occupied Cartan sign is opposite ours; negating its Cartan axes and positive system gives the displayed highest weight. TauCeti formalizes the short and difference-root actions and the integral simple-coroot eigenvalues TauCeti.SpinPolarizationData.typeBSpinRep_differenceRootGenerator_apply TauCeti.SpinPolarizationData.spinAction_typeBQuadraticEquiv_typeBSimpleCorootGenerator_basis.

The top word's weight and annihilation data are available over any field with \(2\) invertible, for a supplied polarization, basis of \(W\), and residual vector \(z\) with \(Q(z)=1\). The Cartan acts on \(\Omega _B\) through the terminal fundamental weight TauCeti.SpinPolarizationData.typeBSpinLieRep_apply_cartan_exteriorBasis_univ, and the Lie subalgebra generated by all positive simple-root generators annihilates it TauCeti.SpinPolarizationData.typeBSpinLieRep_lieSpan_range_simpleRootGenerator_le_lieAnnihilator_exteriorBasis_univ. The declarations index the rank by \(n+1=\ell \); their terminal \(\operatorname {Fin.last}(n)\) labels our \(\omega _\ell \).

The general highest-vector criterion is available separately: a nonzero Cartan weight vector is highest exactly when every raising generator kills it LieAlgebra.Basis.isHighestWeightVector_iff_forall_e. It assumes a characteristic-zero field, a finite-dimensional Lie algebra with nondegenerate Killing form, and a Lie basis. For type B, the Killing condition follows when every endomorphism in the full standard action is triangularizable, in particular over \(\mathbb C\) TauCeti.isKilling_typeB. Triangularizability of the diagonal Cartan alone is not this hypothesis. The selected spin-module declarations give the weight and annihilation data, rather than a separately packaged highest-vector conclusion. The Borel-generation and irreducibility arguments above complete the displayed module identification.

Work over the complex split models and positive systems fixed in the preceding type-B and type-D cards. In type \(B_\ell \) assume \(\ell \geq 1\); in type \(D_\ell \) assume \(\ell \geq 4\). For \(I\subseteq \{1,\ldots ,\ell \}\), put \[\lambda _I=\tfrac 12\left ( \sum _{i\in I}\epsilon _i-\sum _{i\notin I}\epsilon _i\right ).\] By Theorem [fcap-0025][fcap-0025], the line \(\mathbb C u_I\) has weight \(\lambda _I\); distinct subsets give distinct weights. Consequently \[\operatorname {ch}S_{B_\ell } =\sum _I e^{\lambda _I} =\prod _{i=1}^{\ell } \left (e^{\epsilon _i/2}+e^{-\epsilon _i/2}\right ),\] and the type-D parity carriers have \[\operatorname {ch}S_D^+ =\sum _{\lvert I\rvert \ {\rm even}}e^{\lambda _I},\qquad \operatorname {ch}S_D^- =\sum _{\lvert I\rvert \ {\rm odd}}e^{\lambda _I}.\] If \(a_i=e^{\epsilon _i/2}\) and \(b_i=e^{-\epsilon _i/2}\), sorting the product by occupied parity gives \[\operatorname {ch}S_D^\pm =\tfrac 12\left [ \prod _i(a_i+b_i)\ \mathbin {\pm }\ \prod _i(b_i-a_i)\right ].\] The order \(b_i-a_i\) makes an occupied coordinate contribute the minus sign. These are finite sums obtained from the exterior basis, without invoking a general character formula.

The complete half-sum weights above become honest characters on the Spin torus. Put \(A_i=e_i e_i'\), so its action is \(N_i\). For \(t\in \mathbb C^\times \), define \[g_i(t)=tA_i+t^{-1}(1-A_i) =(t e_i+t^{-1}e_i')(e_i+e_i').\] Both vector factors have quadratic value \(1\); the pair criterion therefore puts \(g_i(t)\) in the actual Spin carrier CliffordAlgebra.ι_mul_ι_mem_spinGroup_of_norm_mul_norm_eq_one. The elements for different coordinates commute, and \[g_i(t)u_I= \begin {cases}t\,u_I,&i\in I,\\t^{-1}u_I,&i\notin I.\end {cases}\] Their vector action scales \(e_i\) by \(t^2\), \(e_i'\) by \(t^{-2}\), and fixes the other coordinates. Thus \(g(t_1,\ldots ,t_\ell )=\prod _i g_i(t_i)\) covers the standard orthogonal torus by coordinatewise squaring.

The kernel of this parameterization is \[\{(t_i):t_i\in \{1,-1\},\ \prod _i t_i=1\}.\] Indeed, equality of its spinor action with the identity forces \(t_i^2=1\) by comparing weights that differ in coordinate \(i\), and the vacuum weight then forces \(\prod _i t_i=1\). Conversely such a tuple gives the actual Clifford scalar \(\prod _i t_i=1\). Thus both implications hold directly for the group parameterization. The image contains the scalar \(-1\); together with the usual \(\{1,-1\}\) kernel of \(\operatorname {Spin}\to SO\) [fulton2004representation, Proposition 20.28, pp. 308--309], this is the full inverse-image torus.

A Laurent monomial on the parameter torus descends through the displayed sign kernel exactly when all its integer exponents have the same parity. Relative to the orthogonal coordinates \(x_i=t_i^2\), the Spin weight lattice is therefore \[P=\mathbb Z^\ell \cup \left (\mathbb Z+\tfrac 12\right )^\ell .\] The complete signed sums \(\lambda _I\) lie in \(P\), while an individual symbol \(e^{\epsilon _i/2}\) need not itself be a character. The orthogonal torus has character lattice \(\mathbb Z^\ell \); every spinor half-sum takes the scalar \(-1\) to \(-1\) and hence does not descend to it. In type D the adjoint torus has the still smaller root lattice.

[goodman2009symmetry, Corollary 6.3.9, p. 322; Sections 7.1 and 7.2.3, pp. 330 and 346] independently identify complex Spin as algebraically simply connected, explain the single-valued square-root torus factors, and identify the torus-character lattice with the weight lattice. Those group results support the character interpretation. The pinned TauCeti results used above are Lie and Clifford statements; no formal integration or differentiation comparison is asserted.

For \(B_2\), the four distinct weights are summarized by \[\operatorname {ch}S_{B_2} =(x^{1/2}+x^{-1/2})(y^{1/2}+y^{-1/2}),\] with highest weight \((\epsilon _1+\epsilon _2)/2=\omega _2\). For \(D_4\), the even- and odd-cardinality sums contain eight weights each: \(\omega _4=(\epsilon _1+\epsilon _2+\epsilon _3+\epsilon _4)/2\) lies in \(S^+\), while \(\omega _3=(\epsilon _1+\epsilon _2+\epsilon _3-\epsilon _4)/2\) lies in \(S^-\). This is a finite character check, not a triality claim.

Let \(V\) be a three-dimensional complex quadratic space with a supplied nondegenerate polarization \[V=\mathbb C w\oplus \mathbb C z\oplus \mathbb C w',\qquad B_Q(w,w')=1,\quad Q(z)=1,\] and choose the line coordinate so that \(\rho (z)=\alpha \), exterior parity. On \(S=\bigwedge (\mathbb Cw)\), use the ordered basis \((1,w)\). The even Clifford action then gives a homomorphism \[\operatorname {Spin}(Q)\longrightarrow SL(S)\simeq SL_2(\mathbb C).\] Reversal is matrix adjugation in this basis, so reverse norm one forces determinant one. This is the determinant calculation behind the dimension-three case; the target is the complex group, rather than the compact real unit-quaternion group of Example [fcap-002H][fcap-002H].

There is a concrete inverse. For \(c\in \mathbb C\), the two products \[(z+cw)z,\qquad z(z+cw')\] are products of two norm-one vectors and hence are actual Spin elements. Creation, contraction, and parity from Proposition [fcap-002W][fcap-002W] give their matrices \[I+cE_{21},\qquad I+cE_{12}\] in the ordered basis \((1,w)\). These elementary transvections generate \(SL_2(\mathbb C)\). Writing a target matrix as a word in them and replacing each factor by its displayed lift gives a preimage; faithfulness of the even Clifford action makes the result independent of the chosen word. Thus restriction and this lift are inverse group maps, and the same basis intertwines the spin action with the standard two-dimensional module.

TauCeti proves this exact group-and-module statement over any field with \(2\ne 0\), given polarization data and dimension three TauCeti.exists_spinGroup_mulEquiv_specialLinearGroup_and_spinRep_equiv_stdSLRep_of_finrank_eq_three. Its chosen finite basis may reindex the two exterior coordinates; the formulas above use the stated basis \((1,w)\) and the corresponding basis change. The theorem needs no additional separable-closure hypothesis once the polarization is supplied.

Fulton--Harris identify \(\operatorname {Spin}_3(\mathbb C)\) with \(SL_2(\mathbb C)\) and distinguish it from the compact real form \(SU(2)\) [fulton2004representation, Section 10.3, pp. 143--144; Exercise 20.39, p. 311]. Goodman--Wallach independently list the same complex exceptional isomorphism [goodman2009symmetry, Section 6.3.3, Exercise 1, p. 322]. Their statements name the target; the two Clifford products above supply the coordinate lifts used here. Meinrenken's \(\operatorname {Spin}(3)=SU(2)\) is instead the compact real comparison [meinrenken2013clifford, Section 3.7.6, p. 83].

Let \(V=W\oplus W'\) be a split nondegenerate complex quadratic space with \(\dim W=2\), and choose polar-dual bases \(e_1,e_2\) and \(e'_1,e'_2\). Put \(S^+=\bigwedge ^{\mathrm {even}}W\) and \(S^-=\bigwedge ^{\mathrm {odd}}W\), with ordered bases \((1,e_1\wedge e_2)\) and \((e_1,e_2)\). The paired half-spin action from Theorem [fcap-002V][fcap-002V] gives an algebra equivalence \[\Phi :\mathcal {C}\kern -2pt\ell (Q)^0\longrightarrow \operatorname {End}(S^+)\times \operatorname {End}(S^-) \simeq M_2(\mathbb C)\times M_2(\mathbb C)\] TauCeti.SpinPolarizationData.evenCliffordEquivProdEnd. The two factors here are the actions on the fixed exterior-parity summands, not merely two abstract matrix blocks.

For exterior spinors define \[\langle s,t\rangle = [e_1\wedge e_2]\bigl (\operatorname {rev}_{\wedge }(s)\wedge t\bigr ),\] where the bracket takes the coefficient of \(e_1\wedge e_2\). On each displayed half-spin basis its matrix is \[J=\begin {pmatrix}0&1\\-1&0\end {pmatrix},\] and the two parity summands are orthogonal. Each creation operator and each polar-dual contraction operator is self-adjoint for this pairing, so Clifford reversal becomes the symplectic adjoint on each factor. Consequently, if \(\Phi (x)=(A,D)\), then \[\Phi (\operatorname {rev}(x)) =\bigl (J^{-1}A^{\mathsf T}J,J^{-1}D^{\mathsf T}J\bigr ) =\bigl (\operatorname {adj}(A),\operatorname {adj}(D)\bigr ).\] Therefore \(\operatorname {rev}(x)x=1\) is equivalent to \(\det A=\det D=1\).

We use one carrier-completion observation. In any positive-dimensional nondegenerate complex quadratic space, suppose an even Clifford unit \(u\) satisfies \(\operatorname {rev}(u)u=1\) and is already known to normalize the vector subspace. Its conjugation action is an isometry, so choose a vector-generated Lipschitz unit with the same orthogonal action CliffordAlgebra.lipschitzToOrthogonal_surjective. The quotient of that lift and \(u\) satisfies \(\alpha (z)v=vz\); graded centrality makes it a nonzero scalar CliffordAlgebra.exists_eq_algebraMap_of_involute_mul_ι_eq_ι_mul. Such a scalar unit is Lipschitz CliffordAlgebra.unitsMap_algebraMap_mem_lipschitzGroup. Hence \(u\) is Lipschitz, even, and reverse-norm one, and the exact carrier criterion of Remark [fcap-0028][fcap-0028] puts it in Spin.

The forward restriction is thus a group homomorphism \[\operatorname {Spin}(Q)\longrightarrow SL(S^+)\times SL(S^-).\] Conversely, take \((A,D)\in SL_2(\mathbb C)\times SL_2(\mathbb C)\) and let \(x=\Phi ^{-1}(A,D)\). The adjugate calculation makes \(x\) an even Clifford unit with \(\operatorname {rev}(x)x=1\). It remains to prove that this algebraic preimage lies in the actual vector-generated Spin group.

For \(v\in V\), set \(y=xvx^{-1}\). It is odd and reversal-fixed: \[\operatorname {rev}(y) =\operatorname {rev}(x^{-1})v\operatorname {rev}(x)=y.\] In an orthogonal-basis Clifford expansion in dimension four, the odd part has only grades one and three. Reversal has signs \(+1\) and \(-1\) on those grades, so \(y\in V\). Moreover \(y^2=Q(v)1\); conjugation hence induces an isometry of \((V,Q)\). The carrier-completion observation now places \(x\) in the actual Spin group.

The restriction and \((A,D)\mapsto \Phi ^{-1}(A,D)\) are now inverse group maps. Hence \[\operatorname {Spin}_4(\mathbb C)\simeq SL_2(\mathbb C)\times SL_2(\mathbb C),\] and the two half-spin representations are the two standard two-dimensional modules. [fulton2004representation, Exercise 20.39, p. 311] state this group-and-module identification. [goodman2009symmetry, Section 6.3.3, Exercise 1, p. 322] independently give the same complex group. The displayed pairing, adjugate calculation, and carrier argument provide the inverse.

[meinrenken2013clifford, Section 3.7.6, p. 83] identifies the compact real form as \(\operatorname {Spin}(4)=SU(2)\times SU(2)\). Its quaternion-pair model is Example [fcap-002K][fcap-002K], while the Lorentzian real form \(SL_2(\mathbb C)\) is Example [fcap-002L][fcap-002L]; neither replaces the split complex proof above. TauCeti formalizes the paired half-spin algebra and matrix maps TauCeti.SpinPolarizationData.evenCliffordEquivProdMatrix.

The actual group and both modules also have a direct formal counterpart TauCeti.exists_spinGroup_mulEquiv_specialLinearGroup_prod_and_halfSpin_equiv_stdSLRep_of_finrank_eq_four. For a supplied polarization over a field of characteristic different from two and ambient dimension four, it constructs a group equivalence \(\operatorname {Spin}(Q)\simeq SL_2(K)\times SL_2(K)\) together with equivalences from the existing plus and minus half-spin subrepresentations to the standard representations pulled back from the first and second factors. The dimension hypothesis forces the residual line to vanish. The theorem chooses bases of both half-spin spaces, so its matrix coordinates agree with the ordered bases used here after basis transport. The displayed pairing and carrier proof give the comparison in our explicit coordinates.

Let \(V=W\oplus \mathbb Cz\oplus W'\) be a five-dimensional complex quadratic space with a supplied nondegenerate polarization, where \(\dim W=2\), \(Q(z)=1\), and \(\rho (z)=\alpha \). On \(S=\bigwedge W\), use the ordered basis \[(1,e_1\wedge e_2,e_1,e_2).\] Define \[\langle s,t\rangle = [e_1\wedge e_2]\bigl (\operatorname {rev}_{\wedge }(s)\wedge t\bigr ).\] Its matrix is \(\Omega =\operatorname {diag}(J,J)\), where \(J=\left (\begin {smallmatrix}0&1\\-1&0\end {smallmatrix}\right )\). The pairing preserves exterior parity, so parity itself is self-adjoint. Each creation operator and each polar-dual contraction operator is self-adjoint as well. Consequently the faithful even Clifford equivalence from Proposition [fcap-002W][fcap-002W] takes reversal to \[A\longmapsto A^{\dagger } =\Omega ^{-1}A^{\mathsf T}\Omega \] TauCeti.SpinPolarizationData.evenCliffordEquivEnd. Reverse norm one is therefore exactly the symplectic equation \(A^{\mathsf T}\Omega A=\Omega \).

This norm calculation alone does not yet prove membership in the vector-generated Spin group. The five vector operators \[c_1,\ c_2,\ a_1,\ a_2,\ \alpha \] are linearly independent, traceless, and \(\Omega \)-self-adjoint. The self-adjoint subspace of \(M_4(\mathbb C)\) has dimension six, and its trace-zero part has dimension five because \(\operatorname {tr}(I)=4\). Hence the Clifford image of the vector space is exactly \[\rho (V)= \{T:T^{\dagger }=T,\ \operatorname {tr}(T)=0\}.\] Conjugation by every \(A\in Sp_{\Omega }(4,\mathbb C)\) preserves this subspace: symplectic conjugation preserves the adjoint condition, and trace is conjugation-invariant.

The odd Clifford action is injective on the vector subspace. More generally, if an odd Clifford value \(y\) acts by zero, then \(zy\) is even and acts by zero. Faithfulness of the even action and invertibility of \(z\) give \(y=0\). Thus preservation of the displayed matrix subspace lifts to preservation of \(V\) inside the Clifford algebra.

For \(A\in Sp_{\Omega }(4,\mathbb C)\), let \(x\) be its unique preimage under the even Clifford equivalence. The adjoint equation gives \(\operatorname {rev}(x)x=1\), while the preceding calculation proves \(xVx^{-1}=V\). The carrier-completion argument of Proposition [fcap-0032][fcap-0032] now places \(x\) in actual Spin. Conversely, every Spin element has symplectic matrix because its reverse norm is one. These assignments are inverse group maps, and the chosen exterior basis is the module intertwiner: \[\operatorname {Spin}_5(\mathbb C)\simeq Sp_{\Omega }(4,\mathbb C), \qquad S\simeq \mathbb C^4.\]

Fulton--Harris state the same group and standard spin-module identification [fulton2004representation, Exercise 20.39, p. 311]. Goodman--Wallach independently write the target as \(Sp(2,\mathbb C)\), the rank-two symplectic group on a four-dimensional complex space [goodman2009symmetry, Section 6.3.3, Exercise 1, p. 322]. The trace-zero normalization calculation supplies the actual group inverse rather than inferring the image from a dimension count. By contrast, Meinrenken's \(\operatorname {Spin}(5)=Sp(2)\) is the compact quaternionic real form [meinrenken2013clifford, Section 3.7.6, pp. 83--84].

TauCeti proves that in odd dimension the even Clifford action is an equivalence onto the full endomorphism algebra and is faithful TauCeti.SpinPolarizationData.evenCliffordEquivEnd TauCeti.evenSpinAction_injective. It does not package the invariant alternating form or the group image as \(Sp_4\); those calculations are the explicit argument above.

Let \(V=W\oplus W'\) be a split nondegenerate complex quadratic space with \(\dim W=3\). For polar-dual bases \(e_i,e'_i\), use \[S^+:(1,e_{12},e_{13},e_{23}),\qquad S^-:(e_{123},-e_3,e_2,-e_1).\] For \(\langle s,t\rangle =[e_{123}]\bigl ( \operatorname {rev}_{\wedge }(s)\wedge t\bigr )\), the second displayed basis is dual to the first, and the full pairing matrix on \(S^+\oplus S^-\) is \[\Omega =\begin {pmatrix}0&I_4\\-I_4&0\end {pmatrix}.\] Clifford generators are self-adjoint for this pairing. Under the paired even-algebra equivalence \(\Phi \) of Theorem [fcap-002V][fcap-002V], reversal therefore sends \[(A,D)\longmapsto (D^{\mathsf T},A^{\mathsf T}).\] Thus the even reverse-norm-one group is \[\{(A,A^{-\mathsf T}):A\in GL_4(\mathbb C)\}.\] At this stage it is \(GL_4\), not yet the actual Spin group.

The vector-normalization condition cuts out the determinant-one subgroup. If \(v=\sum _i x_i e_i+y_i e'_i\), its odd Clifford action has block form \[\rho (v)=\begin {pmatrix}0&B_v\\B_v^\sharp &0\end {pmatrix},\] where \[B_v=\begin {pmatrix} 0&-y_3&y_2&-y_1\\ y_3&0&x_1&x_2\\ -y_2&-x_1&0&x_3\\ y_1&-x_2&-x_3&0 \end {pmatrix}.\] These matrices run through all skew \(4\times 4\) matrices. For a skew matrix \(B\), define \(B^\sharp \) by \[\begin {aligned} (B^\sharp )_{01}&=B_{23},& (B^\sharp )_{02}&=-B_{13},& (B^\sharp )_{03}&=B_{12},\\ (B^\sharp )_{12}&=B_{03},& (B^\sharp )_{13}&=-B_{02},& (B^\sharp )_{23}&=B_{01}, \end {aligned}\] with skew extension. Then \((B^\sharp )^\sharp =B\), \(BB^\sharp =-\operatorname {Pf}(B)I\), and \(\operatorname {Pf}(B_v)=-\sum _i x_i y_i\). The last two identities give \(\rho (v)^2=Q(v)I\), matching the Clifford convention.

The complementary-minor identity is \[(ABA^{\mathsf T})^\sharp =\det (A)A^{-\mathsf T}B^\sharp A^{-1}.\] One derivation identifies a skew matrix with an alternating two-form: the operation \(B\mapsto B^\sharp \) is the complementary two-form determined by the ordered volume basis, while \(\bigwedge ^4 A\) multiplies that volume by \(\det A\). Evaluating on basis pairs gives the six coordinate rules above and the displayed identity.

Conjugation by \(\operatorname {diag}(A,A^{-\mathsf T})\) sends the two off-diagonal blocks to \[ABA^{\mathsf T},\qquad A^{-\mathsf T}B^\sharp A^{-1}.\] By the complementary-minor identity, it preserves the vector graph \(\{(B,B^\sharp ):B^{\mathsf T}=-B\}\) exactly when \(\det A=1\). Sufficiency is immediate. For necessity, choose any nonzero \(B^\sharp \); equality of the two lower blocks forces \(\det A=1\). Faithfulness of the full Clifford action in this even dimension lifts this matrix statement to normalization of the actual vector subspace.

Every Spin element therefore acts on \(S^+\) through \(SL_4(\mathbb C)\). Conversely, for \(A\in SL_4(\mathbb C)\), let \(x\) be the unique even Clifford preimage of \((A,A^{-\mathsf T})\). It has reverse norm one and, by the graph calculation, normalizes \(V\). The carrier-completion argument of Proposition [fcap-0032][fcap-0032] places \(x\) in actual Spin. The mutually inverse maps are \[g\longmapsto \rho _+(g),\qquad A\longmapsto \Phi ^{-1}(A,A^{-\mathsf T}).\] Hence \[\operatorname {Spin}_6(\mathbb C)\simeq SL_4(\mathbb C).\] In the displayed bases \(S^+\) is the standard four-dimensional module and \(S^-\) is its dual.

[fulton2004representation, Exercise 20.39, p. 311] give the group and standard \(S^+\) module. [goodman2009symmetry, Section 6.3.3, Exercise 1, p. 322] independently give the same complex group. Here the cross-pairing proves \(S^-\) is dual, and the vector-graph calculation proves the actual image.

[meinrenken2013clifford, Section 3.7.6, p. 84] gives the compact real form \(\operatorname {Spin}(6)=SU(4)\).

TauCeti formalizes the paired half-spin algebra and matrix equivalences TauCeti.SpinPolarizationData.evenCliffordEquivProdEnd TauCeti.SpinPolarizationData.evenCliffordEquivProdMatrix. The vector graph, determinant-one group image and inverse are proved above, not by these declarations.

Work over \(\mathbb C\) with the type-\(D_4\) Cartan and Borel of Proposition [fcap-002X][fcap-002X]. In its orthonormal coordinates put \[\begin {aligned} \alpha _1&=\epsilon _1-\epsilon _2,& \alpha _2&=\epsilon _2-\epsilon _3,\\ \alpha _3&=\epsilon _3-\epsilon _4,& \alpha _4&=\epsilon _3+\epsilon _4. \end {aligned}\] The central node is \(2\); the outer nodes are \(1,3,4\). Their fundamental weights are \[\omega _1=\epsilon _1,\qquad \omega _3=\tfrac 12(\epsilon _1+\epsilon _2+\epsilon _3-\epsilon _4),\qquad \omega _4=\tfrac 12(\epsilon _1+\epsilon _2+\epsilon _3+\epsilon _4).\] The established exterior convention identifies the vector class with \(L(\omega _1)\), the all-plus half-spin class with \(S^+=L(\omega _4)\), and the other half-spin class with \(S^-=L(\omega _3)\); see Theorem [fcap-002Y][fcap-002Y] and Proposition [fcap-0030][fcap-0030]. Each has dimension eight.

Let \(\sigma \) be any permutation of \(\{1,3,4\}\). The linear map specified on the simple-root basis by \[T_\sigma (\alpha _i)=\alpha _{\sigma (i)}\quad (i=1,3,4),\qquad T_\sigma (\alpha _2)=\alpha _2\] preserves the \(D_4\) Cartan matrix. Hence it is orthogonal, preserves the root and coroot systems, and preserves the weight and coweight lattices. It is therefore an automorphism of the simply connected based root datum. Duality with the simple coroots gives \[T_\sigma (\omega _i)=\omega _{\sigma (i)}\qquad (i=1,3,4).\] In particular an outer three-cycle has cube one and nontrivially cycles the three labeled highest-weight classes \[L(\omega _1),\qquad S^-=L(\omega _3),\qquad S^+=L(\omega _4).\] This is a permutation of based root data and of irreducible highest-weight labels. A literal pullback of concrete group modules would additionally require an actual group automorphism and a fixed direction; that stronger statement is not inferred from this diagram calculation.

[fulton2004representation, Section 20.3, pp. 312--314] give the same \(D_4\) diagram and identify the vector and two half-spin highest weights. [adams1996exceptional, Chapter 5, Theorem 5.6, pp. 33--35] independently identifies these as the three basic eight-dimensional classes permuted by outer automorphisms. The first source is the complex highest-weight comparison used here; Adams' theorem concerns the compact actual group and is not being claimed as proved by the root-datum calculation alone.

The pinned declaration TauCeti.D4Tripled.trialityAutomorphism has cube one on a tripled type-\(D_4\) toral-closure carrier and permutes its numbered root and represented-torus coordinates. The inspected file does not identify that carrier with standard \(\operatorname {Spin}_8\), prove its torus maximal, or identify its three factors with the vector and half-spin modules. It is precise formal context for the diagram symmetry, not a whole-card formalization of the proposition above.

Let \(Q_8^+\) be the positive quadratic form on \(\mathbb R^8\), and let \[G=\operatorname {Spin}(Q_8^+)\longrightarrow SO(8)\] be the actual vector-generated, reverse-norm-one carrier and its vector action \(\pi \). The concrete Lie-group and covering results of Proposition [fcap-0037][fcap-0037] and Proposition [fcap-003A][fcap-003A] make \(G\) compact, connected, and simply connected, with \(\pi \) its two-sheeted universal cover. The even-word sign-change map of Proposition [fcap-0039][fcap-0039] identifies this positive-square carrier with the compact negative-square convention used in the classical source, compatibly with the vector action.

Let \(\nu _+\) and \(\nu _-\) be the two real eight-dimensional half-spin representations. Their complexifications have highest weights \(\omega _4\) and \(\omega _3\), so the comparison of Proposition [fcap-003B][fcap-003B] and the exterior construction of Theorem [fcap-002Y][fcap-002Y] identify them, up to chosen intertwiners, with the two concrete complex half-spin modules. Average a positive definite inner product over compact \(G\). In an orthonormal basis either representation gives \[\nu :G\longrightarrow O(8).\] Connectedness puts its image in \(SO(8)\). Since \(G\) is simply connected, the universal cover \(\pi \) has a unique based lift \[\Theta :G\longrightarrow G,\qquad \pi \circ \Theta =\nu .\] The two maps \(\Theta (xy)\) and \(\Theta (x)\Theta (y)\) are based lifts on the connected space \(G\times G\), so uniqueness makes \(\Theta \) a group homomorphism.

Its derivative is nonzero because the half-spin representation has nonzero weights. The kernel of the derivative is an ideal of the simple Lie algebra \(\mathfrak {so}_8\), hence it is zero. Equal dimensions make \(\Theta \) a local Lie-group isomorphism. Its image is open, and compactness makes it closed; connectedness of \(G\) makes the image all of \(G\). Thus \(\Theta \) is a covering of a simply connected target by a connected source and is a Lie-group automorphism. Let Lie-group automorphisms act on representation classes by inverse pullback, \[\varphi \mathbin {\cdot }[M]=[M\circ \varphi ^{-1}].\] With this left-action convention, \(\Theta ^{-1}\) sends the vector class to the chosen half-spin class because \(\pi \circ \Theta =\nu \).

Every Lie-group automorphism permutes the three classes. After inner conjugation it preserves a chosen maximal torus and positive Weyl chamber; its differential therefore induces a based \(D_4\) root-datum automorphism. The diagram calculation of Proposition [fcap-003B][fcap-003B] shows that it permutes precisely the outer-node weights \(\omega _1,\omega _3,\omega _4\). Inner automorphisms act trivially on isomorphism classes, so inverse pullback defines a homomorphism \[\operatorname {Out}_{\mathrm {Lie}}(G)\longrightarrow S_3.\] There is a second kind of actual Lie-group automorphism. Conjugation by any unit vector in the Clifford algebra preserves even vector products and reverse norm and has conjugation by its inverse as inverse. On the vector module it gives orthogonal conjugation of \(\pi \); on the odd Clifford action it interchanges \(S^+\) and \(S^-\). Its permutation fixes the vector class and swaps the two half-spin classes. Together with the lifted half-spin automorphism, these permutations generate \(S_3\).

This permutation action has inner kernel. Suppose an automorphism \(\varphi \) fixes all three representation classes. Equivalence of \(\pi \circ \varphi \) with \(\pi \) gives an intertwiner; after polar normalization it is a matrix \(A\in O(8)\). If \(\det A=1\), lift \(A\) to \(g\in G\). After composing \(\varphi \) with the inverse inner automorphism \(\operatorname {Int}(g)\), its projection agrees with \(\pi \). The pointwise discrepancy from the identity lies continuously in \(\ker \pi =\{1,-1\}\), hence is identically \(1\) on connected \(G\). The remaining automorphism is the identity. If \(\det A=-1\), first compose with unit-vector conjugation. The result is inner by the preceding case, but unit-vector conjugation swaps the two half-spin classes, contradicting the hypothesis. Therefore \[\operatorname {Out}_{\mathrm {Lie}}(G)\simeq S_3.\] A suitable composition of the two constructed outer classes maps to a three-cycle and therefore has order three in the outer group. This does not show that the chosen half-spin lift \(\Theta \) has order three, and no representative has been normalized here to cube to the identity. No splitting \(S_3\to \operatorname {Aut}_{\mathrm {Lie}}(G)\) is asserted.

[adams1996exceptional, Chapter 5, Theorem 5.6, pp. 34--35] proves the compact group theorem and the permutation of its three eight-dimensional representations. [fulton2004representation, Section 20.3, pp. 312--314] independently describe the corresponding complex vector/half-spin triality and root diagram. The carrier translation, universal-cover lift, surjectivity, and kernel argument above place that comparison on the actual FCAP Spin group.

The pinned declaration TauCeti.D4Tripled.trialityAutomorphism has literal cube one on a tripled toral-closure carrier. Its source file does not identify that carrier with the actual group \(G\). Accordingly it is not used to claim cube one for \(\Theta \) or as a formal badge for this theorem.

Complexify the compact model and use the split rank-four exterior carrier \(S=\bigwedge W\) with a chosen top form \(\operatorname {vol}=e_1\wedge e_2\wedge e_3\wedge e_4\). Define \[B(s,t)=[\operatorname {rev}_{\wedge }(s)\wedge t]_{\operatorname {vol}}.\] In degree four this form is symmetric; its restrictions \(B_+\) and \(B_-\) to \(S^+\) and \(S^-\) are nondegenerate. Each creation operator and each polar-dual contraction operator is individually self-adjoint for \(B\). Thus the adjoint of Clifford multiplication by \(x\) is multiplication by \(\operatorname {rev}(x)\), and actual Spin elements preserve \(B\).

For \(v\in V\), \(s_+\in S^+\), and \(s_-\in S^-\), put \[F(v,s_+,s_-)=B_-(\rho (v)s_+,s_-).\] Clifford covariance of \(\rho (v)\) and invariance of \(B\) give \[F(\pi (g)v,\rho _+(g)s_+,\rho _-(g)s_-)=F(v,s_+,s_-) \qquad (g\in \operatorname {Spin}_8).\] The form is nonzero: with the displayed orientation, \[F(e_1,1,e_2\wedge e_3\wedge e_4)=1.\] This is an explicit invariant tensor \(V\otimes S^+\otimes S^-\to \mathbb C\); changing the chosen top form rescales it.

It is unique up to scalar. The full odd Clifford range is \[\operatorname {Hom}(S^+,S^-)\oplus \operatorname {Hom}(S^-,S^+).\] Under equivariant antisymmetrization its degrees are \(1,3,5,7\). Multiplication by the normalized Clifford volume element of the eight-dimensional space \(V\) exchanges degrees \(k\) and \(8-k\); projecting to either chirality block therefore gives \[\operatorname {Hom}(S^+,S^-)\simeq V\oplus \bigwedge ^3V.\] The two summands are nonisomorphic irreducible \(\operatorname {Spin}_8\)-modules, so \(V\) occurs exactly once. The nondegenerate forms identify invariant trilinears with \(\operatorname {Hom}_{\operatorname {Spin}_8}(V,S^+\otimes S^-)\), which is therefore one-dimensional.

[adams1996exceptional, Chapter 5, Proposition 5.7, pp. 35--36] states the invariant trilinear and proves the required multiplicity-one decomposition.

[fulton2004representation, Section 20.3, pp. 313--314] independently construct the Clifford-multiplication trilinear in the complex modules. The displayed top-form formula fixes its normalization in the FCAP creation--contraction convention. It does not assert a normed composition algebra or an order-three isometry of the tensor.

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][fcap-003B]. These are literal pullbacks of representations of the compact real group.

The outer-class calculation in Theorem [fcap-003C][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][fcap-003B] remains a different construction.

For the automorphism \(\tau \) of Theorem [fcap-003T][fcap-003T], one can choose real forms of \(S^+,S^-\), invariant positive inner products on them, and real isometries \[J_0:V_{\mathbb R}\longrightarrow S^+_{\mathbb R},\qquad J_1:S^+_{\mathbb R}\longrightarrow S^-_{\mathbb R},\qquad J_2:S^-_{\mathbb R}\longrightarrow V_{\mathbb R}\] whose cyclic direct-sum map \(J\) has \(J^3=1\). Their complex-linear extensions preserve exactly the trilinear \(F\) of Proposition [fcap-003D][fcap-003D]: \[F(J_2s_-,J_0v,J_1s_+)=F(v,s_+,s_-).\] The chosen forward cycle intertwines the diagonal group action with \(\tau ^{-1}\). The real forms and inner products are specified in the construction below.

Proposition 5.7 in [adams1996exceptional, pp. 35--36] supplies the invariant-line and real-valued trilinear statements.

Exercises 20.50--20.51 in [fulton2004representation, pp. 314--315] describe the related cyclic tensor symmetry. The construction above obtains that symmetry from the chosen compact automorphism and the real invariant line. Its isometry claim uses the transported inner products just defined; it does not identify them with preselected exterior bilinear forms or assert a normed composition algebra.

The exterior model now has two distinct faithful-range results. In even split dimension, Theorem [fcap-002V][fcap-002V] constructs all matrix units, identifies the two even endomorphism blocks, and records irreducibility after restriction to Spin under its separably closed, positive-rank hypotheses. In odd complex dimension, Proposition [fcap-002W][fcap-002W] shows that either full Clifford action selects one simple summand, while its restriction to the even algebra is faithful and its actual Spin action exchanges exterior parity in positive rank. Thus exterior parity is not a decomposition into odd-dimensional Spin submodules.

The occupation lines of Theorem [fcap-0025][fcap-0025] have also been joined to root and highest-weight theory. The type-D calculation in Proposition [fcap-002X][fcap-002X] and Theorem [fcap-002Y][fcap-002Y] fixes a Borel, proves positive-nilradical generation, and identifies the two fork modules. The type-B calculation in Theorem [fcap-002Z][fcap-002Z] adds the short root and its irreducible spin module, while Proposition [fcap-0030][fcap-0030] derives the finite type-B and type-D characters on the actual Spin torus. The selected TauCeti declarations formalize the Clifford root actions, annihilation identities, and weight vectors. The complex Borel, scalar-extension, irreducibility, torus-descent, and character conclusions are the mathematical arguments in these notes, not one packaged formal theorem.

The low-dimensional complex group comparisons are explicit in Proposition [fcap-0031][fcap-0031], Proposition [fcap-0032][fcap-0032], Proposition [fcap-0033][fcap-0033], and Proposition [fcap-0034][fcap-0034]: they identify the actual Spin carriers in dimensions three through six and the stated standard or half-spin modules. These group inverses and module intertwiners are separate from the real algebra classification in Remark [fcap-0016][fcap-0016] and its signature-\((1,3)\) instance in Example [fcap-0026][fcap-0026]. The concrete real differential comparison in Proposition [fcap-0037][fcap-0037] realizes Spin as a closed Lie subgroup, identifies its tangent algebra with the quadratic Clifford lift, and differentiates the vector and finite-dimensional Clifford-module actions; Example [fcap-0038][fcap-0038] fixes the planar half-angle normalization. The selected TauCeti declarations formalize the algebraic lift and generator action, while the Lie-group, exponential, and tangent conclusions are the source-grounded arguments in those cards. The based-root calculation in Proposition [fcap-003B][fcap-003B] fixes the permutation of the three eight-dimensional highest-weight classes. The actual compact-group lifts and kernel calculation in Theorem [fcap-003C][fcap-003C] prove \(\operatorname {Out}_{\mathrm {Lie}}(\operatorname {Spin}_8)\simeq S_3\), while Proposition [fcap-003D][fcap-003D] constructs the invariant vector--half-spin trilinear and proves its multiplicity-one uniqueness. The pinned tripled-carrier automorphism is formal context on its stated carrier; it is not used as a packaged theorem about the actual Spin group.

For \(p,q\ge 0\), put \[Q_{p,q}(x)=\sum _{i<p}x_i^2-\sum _{p\le i<p+q}x_i^2\] on \(\mathbb {R}^{p+q}\), and write \(\mathcal {C}\kern -2pt\ell _{p,q}\) for \(\mathcal {C}\kern -2pt\ell (Q_{p,q})\). Thus the first \(p\) Clifford generators square to \(+1\), and the last \(q\) square to \(-1\). This agrees with Chevalley's convention for the quadratic form and with his positive/negative inertia indices.

Lawson--Michelsohn impose \(v^2=-q_{r,s}(v)1\) [lawson2016spin, I.3, Proposition 3.1, p. 21]. This swaps the indices while leaving the mixed \((1,1)\) recurrence unchanged: \[\mathcal {C}\kern -2pt\ell _{p,q}=\mathcal {C}\kern -2pt\ell ^{\mathrm {Lawson}}_{q,p}.\]

Let \(K\) be a field of characteristic different from two, and let \((V,Q)\) and \((V',Q')\) be isometric finite-dimensional nondegenerate quadratic spaces. If \(U\subseteq V\) is any subspace and \(f:U\to V'\) is an injective linear map satisfying \[Q'(f(u))=Q(u),\] then \(f\) extends to an isometry \(\widetilde f:(V,Q)\simeq (V',Q')\). For two subspaces of one quadratic space, the assumption that the ambient spaces are isometric is automatic.

[bourbaki2007algebra, Section 4, no. 3, Theorem 1, pp. 71--72] states the theorem with an arbitrary source subspace. In [serre1973course, Chapter IV, Section 1.5, Theorem 3, pp. 31--32], the proof explains why degeneracy of that subspace is harmless when the ambient form is nondegenerate: a radical vector can be paired with a new vector, enlarging the subspace toward a regular one. The regular case then splits orthogonally and closes by induction.

TauCeti proves a complementary form. For a finite-dimensional quadratic space over a field with \(2\) invertible, an isometry equivalence between subspaces \(W,W'\) extends when \(Q|_W\) is nondegenerate; the ambient form itself may be degenerate QuadraticMap.IsometryEquiv.exists_extension. It also chooses an extension and records its value on \(W\) QuadraticMap.IsometryEquiv.extension QuadraticMap.IsometryEquiv.extension_apply. These formal declarations do not prove the arbitrary-subspace statement above.

The distinction is visible inside \(Q_{1,3}\). The block \[A_0=\begin {pmatrix}5/4&3/4\\3/4&5/4\end {pmatrix}\] on the first positive and first negative coordinates, together with the identity on the other two coordinates, defines an ambient isometry \(A\). It satisfies \(A(e_0+e_1)=2(e_0+e_1)\), so its restriction to the null line is an isometry of a degenerate subspace. The classical theorem covers such a line; the regular-subspace formal declaration does not apply because the source restriction is degenerate.

Let \(V\) be four-dimensional over \(\mathbb R\), and let \(Q\) be a nondegenerate quadratic form with positive and negative indices \((1,3)\). Suppose \[Q(t)=1,\qquad Q(s)=-1,\qquad B_Q(t,s)=0.\] There is an isometry \(e:(\mathbb R^4,Q_{1,3})\simeq (V,Q)\) with \(e(e_0)=t\) and \(e(e_1)=s\). Moreover, \(H=\operatorname {span}(t,s)\) has an orthogonal complement of dimension two on which \(Q\) is negative definite. The sign convention for \(Q_{1,3}\) is the one fixed in Convention [fcap-0011][fcap-0011].

The isometry transport in Proposition [fcap-0029][fcap-0029] carries the standard first two Clifford generators to this prescribed pair and commutes with the Spin vector action. The hyperbolic split and quaternionic matrix calculation are already in Example [fcap-0026][fcap-0026], which yields the abstract model \(\mathcal {C}\kern -2pt\ell (V,Q)\simeq M_2(\mathbb H)\). This does not identify a particular gamma-matrix homomorphism, its kernel, or its image.

For \(Q(a,b,c)=a^2-b^2\) on \(\mathbb R^3\), with \(e_1,e_2,e_3\) the standard coordinate basis, the radical is \(\mathbb R e_3\). The zero-form lines \(\mathbb R e_3\) and \(\mathbb R(e_1+e_2)\) are isometric by \(e_3\mapsto e_1+e_2\), but this map has no ambient isometric extension. Every ambient isometry preserves the radical, whereas \[B_Q(e_1+e_2,e_1)=2,\] so \(e_1+e_2\) is not radical. This example lies outside both guards above: the ambient form is degenerate, and the source line is not regular.

For the projective-geometric-algebra form \(Q_{\mathrm {PGA}}(a,b,c)=a^2+b^2\), the positive, negative, and radical dimensions are \((2,0,1)\), with radical \(\mathbb R e_3\). Its radical quotient is a two-dimensional positive-definite space. Quotienting preserves the positive and negative indices QuadraticForm.sigPos_lift_radical QuadraticForm.sigNeg_lift_radical, but it changes the quadratic space. It therefore cannot silently replace the original degenerate Clifford algebra or its motor carrier. Failure of the classical ambient nondegeneracy hypothesis does not show that extension fails for PGA; TauCeti's regular-subspace theorem may still apply there.

The real hyperbolic plane is \[H=(\mathbb {R}^2,Q_{1,1}),\qquad Q_{1,1}(s,t)=s^2-t^2.\] Its coordinate generators \(e_+\) and \(e_-\) satisfy \[e_+^2=1,\qquad e_-^2=-1,\qquad e_+e_-=-e_-e_+.\] For every signature, separating the last positive and negative coordinates gives an isometry \[(\mathbb {R}^{p+q+2},Q_{p+1,q+1}) \simeq (\mathbb {R}^{p+q},Q_{p,q})\perp H.\] The coordinate order is fixed: the retained \(p\) positive and \(q\) negative axes form the first factor, and the last positive and last negative axes form \(H\).

For finite-dimensional quadratic spaces, Lawson--Michelsohn state the signature recurrence \[\mathcal {C}\kern -2pt\ell _{p+1,q+1}\simeq _{\mathbb {R}\text {-alg}} \mathcal {C}\kern -2pt\ell _{p,q}\otimes _{\mathbb {R}}M_2(\mathbb {R}).\] TauCeti extends the recurrence to any real quadratic module \((M,Q)\) and supplies an explicit formula on generators: \[\mathcal {C}\kern -2pt\ell (Q\perp Q_{1,1})\simeq \mathcal {C}\kern -2pt\ell (Q)\otimes _{\mathbb {R}}M_2(\mathbb {R}).\] With \[\sigma _x=\begin {pmatrix}0&1\\1&0\end {pmatrix},\] the equivalence sends a generator \((m,(s,t))\) to \[\iota _Q(m)\otimes \sigma _x +1\otimes \begin {pmatrix}s&t\\-t&-s\end {pmatrix}.\] The first summand squares to \(Q(m)\), the second to \(s^2-t^2\), and the two anticommute. The universal property therefore gives the forward algebra map. In the other direction, the original Clifford algebra and the matrix algebra act through commuting algebra maps on the hyperbolic Clifford algebra; their tensor lift is inverse to the forward map. The two composites are checked on Clifford generators and pure tensors, which is why TauCeti's extension needs no finite-dimensional hypothesis. Chevalley's split-matrix theorem and orthogonal-sum calculation supply the classical structural mechanism [chevalley1954algebraic, II.2.1 and II.2.5, pp. 42--46].

Writing the displayed generator formula as \(f\), its universal extension is summarized by the commuting diagram

Chevalley splits a finite-dimensional real quadratic space into hyperbolic planes and a definite remainder. TauCeti combines that classical reduction with iteration of Theorem [fcap-0013][fcap-0013] and Kronecker equivalences to synthesize the explicit tensor and matrix packaging below. Iterating \(n\) times gives \[\mathcal {C}\kern -2pt\ell _{p+n,q+n}\simeq \mathcal {C}\kern -2pt\ell _{p,q}\otimes _{\mathbb {R}}M_{2^n}(\mathbb {R}).\] Taking \(n=\min (p,q)\) removes the common positive and negative part: \[\mathcal {C}\kern -2pt\ell _{p,q}\simeq \mathcal {C}\kern -2pt\ell _{p-n,q-n}\otimes _{\mathbb {R}}M_{2^n}(\mathbb {R}), \qquad n=\min (p,q).\] Thus if \(p\le q\), the residual algebra is \(\mathcal {C}\kern -2pt\ell _{0,q-p}\); if \(q\le p\), it is \(\mathcal {C}\kern -2pt\ell _{p-q,0}\). The matrix factors combine through the Kronecker equivalence \[M_{2^a}(\mathbb {R})\otimes M_{2^b}(\mathbb {R}) \simeq M_{2^{a+b}}(\mathbb {R}).\] Chevalley supplies the quadratic-space decomposition. The displayed \(M_{2^n}\) packaging and its named equivalences are TauCeti's formalized synthesis.

With the TauCeti signature convention of Convention [fcap-0011][fcap-0011], there is an algebra equivalence \[\mathcal {C}\kern -2pt\ell _{p+2,q}\simeq _{\mathbb R\text {-alg}} \mathcal {C}\kern -2pt\ell _{q,p}\otimes _{\mathbb R}M_2(\mathbb R).\] The construction first separates the last positive coordinate from \(Q_{p+2,q}\). Adjoining that positive line permits a Clifford sign switch; negating \(Q_{p+1,q}\) exchanges its positive and negative coordinate blocks. The resulting form is \(Q_{q+1,p+1}\), to which the hyperbolic recurrence of Theorem [fcap-0013][fcap-0013] applies.

The accompanying generator theorem SignatureSwitchRecurrenceEquiv_ι records this composition through the positive-coordinate splitter, the sign-switch isometry, and the generator formula for the hyperbolic equivalence. It fixes the equivalence on the canonical Clifford generators rather than asserting only that some algebra isomorphism exists.

After converting between the two signature conventions, inverting Lawson--Michelsohn's equation (4.1), using \(\mathcal {C}\kern -2pt\ell ^{\mathrm {Lawson}}_{0,2}\cong M_2(\mathbb R)\), and swapping the indices yields the displayed algebra isomorphism. Their equation (4.3) is instead the mixed \((1,1)\) recurrence used in Theorem [fcap-0013][fcap-0013]. Chevalley's split-matrix and orthogonal-sum constructions give the same structural ingredients [chevalley1954algebraic, II.2.1 and II.2.5, pp. 42--46]. The exact splitter composition and generator formula are additional data recorded by TauCeti.

The recurrences in Theorem [fcap-0013][fcap-0013], Lemma [fcap-0014][fcap-0014], and Theorem [fcap-001X][fcap-001X] use Clifford universal properties, orthogonal sums, tensor products, coordinate isometries, and the real base entries. They do not use the Spin representation, the structure theorem obtained from a spinor module, or the Pin and Spin double covers. This is the algebraic branch of Layer 7.

The real groups \(\operatorname {Pin}(p,q)\) and \(\operatorname {Spin}(p,q)\) form a different branch. Their actions, kernels, and algebraic extensions specialize the group theory developed in § [fcap-0007][fcap-0007], and therefore genuinely consume the Layer-2 Pin/Spin work. The distinction between these branches is the dependency correction recorded in TauCetiRoadmap PR 225. It changes the order in which the mathematics can be built; it does not turn the roadmap proposal itself into a formal theorem.

With \(\mathcal {C}\kern -2pt\ell _{0,0}\simeq \mathbb {R}\) as the scalar anchor, the signature convention of Convention [fcap-0011][fcap-0011] gives four nontrivial base entries: \[\begin {aligned} \mathcal {C}\kern -2pt\ell _{0,0}&\simeq \mathbb {R}, & \mathcal {C}\kern -2pt\ell _{1,0}&\simeq \mathbb {R}\times \mathbb {R}, & \mathcal {C}\kern -2pt\ell _{0,1}&\simeq \mathbb {C},\\ \mathcal {C}\kern -2pt\ell _{0,2}&\simeq \mathbb {H}, & \mathcal {C}\kern -2pt\ell _{1,1}&\simeq M_2(\mathbb {R}). \end {aligned}\] For \(\mathcal {C}\kern -2pt\ell _{0,2}\), the two negative generators map to the quaternion units \(i\) and \(j\); their product maps to \(k\). Thus they square to \(-1\) and anticommute, as required by the Clifford relations. The exact generator map is recorded by TauCeti.realCliffordZeroTwoEquivQuaternion_ι.

For \(\mathcal {C}\kern -2pt\ell _{1,1}\), the positive and negative generators may be represented by \[e_+\longmapsto \begin {pmatrix}1&0\\0&-1\end {pmatrix}, \qquad e_-\longmapsto \begin {pmatrix}0&1\\-1&0\end {pmatrix}.\] Their squares are \(+I\) and \(-I\), and they anticommute. The last equivalence is also the case \(p=q=0\) of Theorem [fcap-0013][fcap-0013]. The index swap in Convention [fcap-0011][fcap-0011] explains why Lawson's one-generator table lists \(\mathbb {C}\) and \(\mathbb {R}\times \mathbb {R}\) in the opposite order.

Let \(V\) be a three-dimensional real vector space and let \(Q\) be nondegenerate. Suppress the canonical generator map in Clifford products. For \(x\in \mathcal {C}\kern -2pt\ell ^{+}(Q)\), the following are equivalent: \[x\text { is the Clifford value of an element of }\operatorname {Spin}(Q), \qquad \operatorname {rev}(x)x=1.\] The forward implication is the even-unitary condition CliffordAlgebra.evenUnitaryGroup.mem_iff_reverse_mul_self_eq_one CliffordAlgebra.range_spinGroup_toUnits.

For the converse, the scalar--bivector decomposition in dimension three writes \(x=a+Z\). Every nonzero bivector is decomposable. If \(Z\ne 0\), let \(P\) be its supporting two-plane. The plane contains \(u\) with \(Q(u)\ne 0\): otherwise polarization would give \(P\subseteq P^\perp \), impossible because \(\dim P=2\) and nondegeneracy gives \(\dim P^\perp =1\). Since \(\bigwedge ^2P\) is one-dimensional, choose \(w\in P\) so that \(Z=\beta _Q(u,w)\). If \(Z=0\), choose any nonisotropic \(u\) and take \(w=0\). Using the unhalved polar form from Convention [fcap-0027][fcap-0027], \[\beta _Q(u,w)=uw-\frac 12B_Q(u,w),\qquad v:=ux=\left (a-\frac 12B_Q(u,w)\right )u+Q(u)w.\] Thus \(v\) is a vector. Reversal and the norm-one equation give \[Q(v)1=\operatorname {rev}(v)v =\operatorname {rev}(x)uux =Q(u)\operatorname {rev}(x)x=Q(u)1.\] The real scalar map is injective, so \(Q(v)=Q(u)\ne 0\). Consequently \[x=\left (\frac {u}{Q(u)}\right )v, \qquad Q\left (\frac {u}{Q(u)}\right )Q(v)=1.\] This is a product of two actual nonisotropic vectors, and TauCeti's pair criterion places it in Spin CliffordAlgebra.ι_mul_ι_mem_spinGroup_of_norm_mul_norm_eq_one. The proof includes the scalar case \(Z=0\); it uses neither a normalizer characterization nor a connectedness argument. The general distinction between reverse norm one and Lipschitz membership remains the one recorded in Remark [fcap-0028][fcap-0028].

Let \(Q_{3,0}(x_0,x_1,x_2)=x_0^2+x_1^2+x_2^2\) and write \(e_0,e_1,e_2\) for its coordinate basis. TauCeti's chosen algebra equivalence \(\theta :\mathcal {C}\kern -2pt\ell ^{+}(Q_{3,0})\simeq \mathbb H\) has the exact axes \[e_0e_1\longmapsto -k,\qquad e_0e_2\longmapsto i,\qquad e_1e_2\longmapsto j\] TauCeti.realCliffordThreeZeroEvenEquivQuaternion TauCeti.realCliffordThreeZeroEvenEquivQuaternion_ι_single_zero_one TauCeti.realCliffordThreeZeroEvenEquivQuaternion_ι_single_two_zero TauCeti.realCliffordThreeZeroEvenEquivQuaternion_ι_single_one_two. Hence \[\theta (s+A e_0e_1+B e_0e_2+C e_1e_2) =s+B i+C j-A k.\] Under \(\theta \), reversal is quaternion conjugation and reverse norm is \[s^2+A^2+B^2+C^2\] TauCeti.realCliffordThreeZeroEvenEquivQuaternion_reverseEven TauCeti.realCliffordThreeZeroEvenEquivQuaternion_map_reverseEven_mul_self_eq_normSq.

Let \(\mathbb H^1=\{q\in \mathbb H:\bar q q=1\}\). Restricting \(\theta \) to Spin gives a homomorphism \[\operatorname {Spin}(Q_{3,0})\longrightarrow \mathbb H^1.\] For \(q=r+x i+y j+z k\in \mathbb H^1\), the inverse Clifford value is \[r-z e_0e_1+x e_0e_2+y e_1e_2.\] Its reverse norm is one, so the dimension-three carrier lemma places it in the actual Spin group. The algebra inverse proves both compositions and multiplicativity. Therefore \[\operatorname {Spin}(Q_{3,0})\simeq \mathbb H^1.\] TauCeti separately packages the algebra map as an equivalence between the even-unitary carrier and unit quaternions TauCeti.realCliffordThreeZeroEvenUnitaryEquivQuaternionUnitary; the preceding carrier lemma is what identifies that carrier with Spin in this real dimension-three case.

In [gallier2014clifford, Section 1.4, pp. 28--29], the analogous compact calculation writes the even element, obtains its sum-of-four-squares norm, and identifies the unit quaternions. Its generators square to \(-1\). Likewise, [lawson2016spin, I.3, Theorem 3.7, pp. 23--24; I.4, (4.0), p. 25] uses \(v^2=-q(v)\) to reduce an even algebra and identify the quaternion base entry. Translating by \(Q=-q\) and the even sign-change equivalence gives the same compact algebra and norm. The displayed axis signs are the exact TauCeti choice above, rather than a relabeling imported from either source.

For \(Q_{3,0}=x_0^2+x_1^2+x_2^2\), use the algebra map \(\theta :\mathcal {C}\kern -2pt\ell ^+(Q_{3,0})\simeq \mathbb H\) of Example [fcap-002H][fcap-002H]. The vector isometry to pure quaternions is \[\eta _3(v_0e_0+v_1e_1+v_2e_2)=-v_1i+v_0j-v_2k.\] For \(s\in \operatorname {Spin}(Q_{3,0})\) and \(q=\theta (s)\in \mathbb H^1\), the ordinary Clifford conjugation action satisfies \[\eta _3(svs^{-1})=q\eta _3(v)\bar q.\] These are the coordinates and action in TauCeti TauCeti.coe_realCliffordThreeZeroPureQuaternionEquiv_apply TauCeti.realSpinThreeEquivQuaternionUnitary_action.

The volume element \(\omega =e_0e_1e_2\) is central and has \(\omega ^2=-1\). Multiplying a vector by it gives \[v\omega =v_0e_1e_2+v_1e_2e_0+v_2e_0e_1,\qquad \eta _3(v)=\theta (v\omega ).\] The three coefficients are only permuted and signed, so \(\eta _3\) is an isometry onto the pure quaternions. Since \(\omega \) is central, \[(svs^{-1})\omega =s(v\omega )s^{-1}.\] Apply \(\theta \); reversal on the even algebra becomes quaternion conjugation, and \(q^{-1}=\bar q\). This proves the displayed action formula.

The axes also determine the sign of the rotation. For real \(t\), put \(s=\cos t+\sin t\,e_0e_1\). Its reverse norm is one, hence it belongs to Spin by Example [fcap-002H][fcap-002H], and \(q=\cos t-\sin t\,k\). Direct multiplication gives \[\begin {aligned} se_0s^{-1}&=\cos (2t)e_0-\sin (2t)e_1,\\ se_1s^{-1}&=\sin (2t)e_0+\cos (2t)e_1,\\ se_2s^{-1}&=e_2. \end {aligned}\] In quaternion coordinates the first identity is \(qj\bar q=\cos (2t)j+\sin (2t)i\), since \(\eta _3(e_1)=-i\). Thus the rotor parameter is a half-angle with the orientation fixed by the stated Clifford and quaternion axes.

Gallier [gallier2014clifford, Section 1.4, p. 29] proves the same volume-element transport to quaternion conjugation with compact generators of square \(-1\). His volume has square \(+1\), and his map is \(v\mapsto -\omega v\); for the positive squares here it is \(v\mapsto v\omega \), followed by the axes of Example [fcap-002H][fcap-002H]. Porteous [porteous1995clifford, Chapter 8, Propositions 8.19--8.21, pp. 62--63] describes the resulting unit-quaternion rotations of pure quaternions. The signed half-angle calculation above specifies this action in the coordinates used here.

For \(Q_{2,1}(x_0,x_1,x_2)=x_0^2+x_1^2-x_2^2\), set \(A=e_0e_1\), \(B=e_0e_2\), and \(C=e_1e_2\). Then \[A^2=-1,\qquad B^2=C^2=1,\qquad AB=-C.\] The assignments \[A\longmapsto \begin {pmatrix}0&1\\-1&0\end {pmatrix},\qquad B\longmapsto \begin {pmatrix}0&1\\1&0\end {pmatrix},\qquad C\longmapsto \begin {pmatrix}-1&0\\0&1\end {pmatrix}\] satisfy these relations, and the images of \(1,A,B,C\) form a basis of \(M_2(\mathbb R)\). They therefore define an algebra equivalence \(\Phi \) with \[\Phi (s+aA+bB+cC)= \begin {pmatrix}s-c&a+b\\-a+b&s+c\end {pmatrix}.\] Reversal negates \(A,B,C\), so it becomes matrix adjugation, and \[N_{\mathrm {rev}}(s+aA+bB+cC) =s^2+a^2-b^2-c^2=\det \Phi (s+aA+bB+cC)\] CliffordAlgebra.map_reverseEven_eq_adjugate_of_finrank_eq_three CliffordAlgebra.reverseEven_mul_eq_one_iff_det_eq_one_of_finrank_eq_three.

Restriction gives \(\operatorname {Spin}(Q_{2,1})\to SL_2(\mathbb R)\). Conversely, if \(M=(m_{ij})\in SL_2(\mathbb R)\), put \[\begin {aligned} s&=\frac {m_{00}+m_{11}}2,& a&=\frac {m_{01}-m_{10}}2,\\ b&=\frac {m_{01}+m_{10}}2,& c&=\frac {m_{11}-m_{00}}2. \end {aligned}\] Then \(\Phi (s+aA+bB+cC)=M\), and its reverse norm is \(\det M=1\). The carrier lemma puts this inverse value in the actual Spin group; the algebra maps give two-sided multiplicative inverses. Thus \[\operatorname {Spin}(Q_{2,1})\simeq SL_2(\mathbb R).\]

The source translation matters. Lawson--Michelsohn's convention turns this even algebra into \(\operatorname {Cl}_{0,2}\simeq M_2(\mathbb R)\) via [lawson2016spin, I.3, Theorem 3.7, pp. 23--24; I.4, (4.0), p. 25]. With the reversed index convention, [gallier2014clifford, Example 1.3, p. 33] independently records \(\operatorname {Cl}_{2,0}\simeq M_2(\mathbb R)\), the same real matrix base algebra. Their indefinite Pin/Spin carrier conventions allow factors of quadratic value \(\pm 1\) [lawson2016spin, I.2, (2.24)--(2.25), p. 18] [gallier2014clifford, Section 1.5, Definition 1.6, p. 31]. We use their algebra identifications but impose the displayed reverse-norm-one equation. For example, \(e_0e_2\) has reverse norm \(-1\) and maps to a determinant \(-1\) matrix, so it is excluded here.

This split form has polarization \(W=\mathbb R(e_0+e_2)\), \(W'=\mathbb R((e_0-e_2)/4)\), and line \(\mathbb R e_1\): the unhalved polar pairing of the displayed generators is \(1\), and the line coordinate squares to \(Q_{2,1}\). TauCeti's polarized dimension-three theorem therefore gives an independent abstract group equivalence with \(SL_2(\mathbb R)\) TauCeti.exists_spinGroup_mulEquiv_specialLinearGroup_and_spinRep_equiv_stdSLRep_of_finrank_eq_three. The concrete map \(\Phi \) above is not asserted to be definitionally that map, and the theorem's representation refinement belongs to the later module packet. Likewise, the vector-action image is the spinor-norm kernel from Theorem [fcap-0023][fcap-0023], not all of \(SO(2,1)\). No component or covering-space claim is made.

For \(Q_{2,1}(v)=v_0^2+v_1^2-v_2^2\), keep the algebra map \(\Phi :\mathcal {C}\kern -2pt\ell ^+(Q_{2,1})\simeq M_2(\mathbb R)\) of Example [fcap-002I][fcap-002I]. Multiplication by the last generator gives symmetric matrix coordinates \[X(v)=\Phi (ve_2)= \begin {pmatrix}-v_2-v_1&v_0\\v_0&-v_2+v_1\end {pmatrix}, \qquad \det X(v)=-Q_{2,1}(v).\] The inverse sends \(\begin {pmatrix}a&b\\b&d\end {pmatrix}\) to \((b,(d-a)/2,-(a+d)/2)\). Thus \(X\) is a real linear equivalence onto the symmetric matrices, with the stated negative determinant form TauCeti.coe_realCliffordTwoOneVectorEquivSymmetric_apply TauCeti.realCliffordTwoOneVectorEquivSymmetric_det. For \(s\in \operatorname {Spin}(Q_{2,1})\) and \(M=\Phi (s)\in SL_2(\mathbb R)\), the vector action becomes \[X(svs^{-1})=M X(v)M^{\mathsf T}.\]

To prove the formula, write \(A=e_0e_1\), \(B=e_0e_2\), and \(C=e_1e_2\). Since \(e_2^2=-1\), conjugation by \(e_2\) is \(\gamma (x)=-e_2xe_2\). It fixes \(A\) and negates \(B,C\). On their three matrices in Example [fcap-002I][fcap-002I], and on the identity, this gives \[\Phi (\gamma (x))=\operatorname {adj}(\Phi (x))^{\mathsf T}.\] Both sides are linear in \(x\), so the basis check proves the equality on the whole even algebra. Moreover, \[(svs^{-1})e_2=s(ve_2)\gamma (s^{-1}).\] The determinant-one equation gives \(\operatorname {adj}(M^{-1})=M\); applying \(\Phi \) proves the action. TauCeti's bilinear-generator formula sends \(A,B,C\) to exactly these three matrices, so its group map and action use this same \(\Phi \) TauCeti.realCliffordTwoOneEvenEquivMatrix_ι TauCeti.realSpinTwoOneEquivSpecialLinear_action.

For example, let \(M=\operatorname {diag}(a,a^{-1})\) with \(a>0\), and choose its Spin preimage using Example [fcap-002I][fcap-002I]. Put \(c=(a^2+a^{-2})/2\) and \(h=(a^2-a^{-2})/2\). The congruence action is \[v_0'=v_0,\qquad v_1'=cv_1+hv_2,\qquad v_2'=hv_1+cv_2.\] Here \(c^2-h^2=1\). The two null coordinates \(v_1+v_2\) and \(v_1-v_2\) are multiplied by \(a^2\) and \(a^{-2}\), respectively. This exhibits the action on both null directions in the chosen coordinates.

For comparison, the compact quaternion action of Example [fcap-003J][fcap-003J] has a complex matrix realization. Distinguish quaternion units \(\mathbf i,\mathbf j,\mathbf k\) from the complex scalar \(i\). The map \[\iota (a+b\mathbf i+c\mathbf j+d\mathbf k)= \begin {pmatrix}a+ib&c+id\\-c+id&a-ib\end {pmatrix}\] preserves multiplication and sends quaternion conjugation to conjugate transpose. Its determinant is \(a^2+b^2+c^2+d^2\), so it identifies the unit quaternions with \(SU(2)\). Indeed a special unitary matrix has the form \(\begin {pmatrix}z&w\\-\bar w&\bar z\end {pmatrix}\) with \(|z|^2+|w|^2=1\), which recovers the four real coordinates. These are Gallier's axes [gallier2014clifford, Section 1.1, pp. 8--9], and the exact embedding and group equivalence in TauCeti Quaternion.toComplexMatrix Quaternion.unitaryEquivSpecialUnitaryGroup.

Keep \(\eta _3(v)=-v_1\mathbf i+v_0\mathbf j-v_2\mathbf k\) from Example [fcap-003J][fcap-003J], and put \(K(v)=i\iota (\eta _3(v))\). It is a traceless Hermitian matrix. Applying \(i\iota \) to the already proved quaternion action gives \[K(svs^{-1})=U K(v)U^*,\qquad U=\iota (\theta (s))\in SU(2),\] where \(U^*\) is conjugate transpose. The composite Spin-to-\(SU(2)\) isomorphism is available in TauCeti TauCeti.realSpinThreeEquivSpecialUnitary. Its action theorem uses the unscaled matrix \(\iota (\eta _3(v))\) TauCeti.realSpinThreeEquivSpecialUnitary_action; multiplication by the central scalar \(i\) gives the displayed \(K\) formula. Thus neither quaternion nor vector axes change. The split formula uses real symmetric matrices and \(SL_2(\mathbb R)\) instead. The fixed-vector transport underlying these formulas is illustrated by [porteous1995clifford, Chapter 16, Proposition 16.9, pp. 143--144]. For the indefinite vector-action image, retain the spinor-norm kernel of Theorem [fcap-0023][fcap-0023]; no component or covering-space assertion is needed.

Let \(V\) be a four-dimensional real vector space and let \(Q\) be nondegenerate. Suppress the canonical generator map in Clifford products. For \(x\in \mathcal {C}\kern -2pt\ell ^{+}(Q)\), the following are equivalent: \[x\text { is the Clifford value of an element of }\operatorname {Spin}(Q), \qquad \operatorname {rev}(x)x=1.\] The forward implication follows from the exact Spin-carrier description CliffordAlgebra.range_spinGroup_toUnits.

Conversely, suppose \(\operatorname {rev}(x)x=1\). Since the Clifford algebra is finite-dimensional, the displayed left inverse is also a right inverse, so \(x\) is a unit and \(x^{-1}=\operatorname {rev}(x)\). For \(v\in V\), put \(w=xvx^{-1}\). The element \(w\) is odd, and \[\operatorname {rev}(w) =\operatorname {rev}(x^{-1})v\operatorname {rev}(x) =xvx^{-1}=w.\] In an orthogonal-basis Clifford expansion in dimension four, the odd part has only degrees one and three. Reversal is \(+1\) on degree one and \(-1\) on degree three, so \(w\in V\). Gallier uses this observation in the compact calculation [gallier2014clifford, p. 30]; the same basis-and-reversal argument applies to every nondegenerate real form in dimension four. Also \(w^2=Q(v)1\). Conjugation is injective, and its restriction to the finite-dimensional space \(V\) is therefore an automorphism. Thus it defines \(g\in O(V,Q)\).

Choose \(y\) in the vector-generated Lipschitz group whose twisted action is \(g\) CliffordAlgebra.lipschitzToOrthogonal_surjective, and set \(z=y^{-1}x\). Since \(x\) is even, equality of the two actions rearranges for the grading involution \(\alpha \) to \[\alpha (z)v=vz\qquad (v\in V).\] The graded-centrality theorem therefore gives \(z=c1\) for some real \(c\) CliffordAlgebra.exists_eq_algebraMap_of_involute_mul_ι_eq_ι_mul. The unit \(z\) has \(c\ne 0\). Nondegeneracy and positive dimension supply a nonisotropic vector, so every nonzero scalar unit belongs to the generated Lipschitz group CliffordAlgebra.unitsMap_algebraMap_mem_lipschitzGroup. Thus \(x=yz\) is Lipschitz. It is even and has reverse norm one, hence lies in Spin by Remark [fcap-0028][fcap-0028]. This dimension-sensitive argument is not asserted in dimension five or six.

For \(Q_{4,0}=x_0^2+x_1^2+x_2^2+x_3^2\), let \(I=e_0e_1e_2e_3\). Then \(I^2=1\), \(\operatorname {rev}(I)=I\), and \(I\) commutes with the even algebra CliffordAlgebra.prod_map_ι_sq_scalar CliffordAlgebra.prod_map_ι_mul_ι_of_even_length. Let \(H_0\) be the quaternion subalgebra with basis \(1,e_0e_1,e_0e_2,e_1e_2\), and choose \(\theta _0:H_0\simeq \mathbb H\) with the quaternion axes of Example [fcap-002H][fcap-002H]: \[e_0e_1\longmapsto -k,\qquad e_0e_2\longmapsto i,\qquad e_1e_2\longmapsto j.\] The eight even basis monomials show uniquely that every even value is \(u+Iv\) with \(u,v\in H_0\). Centrality and \(I^2=1\) make \[\Phi (u+Iv) =\bigl (\theta _0(u)+\theta _0(v),\theta _0(u)-\theta _0(v)\bigr )\] an algebra map. Its inverse is \[(q_+,q_-) \longmapsto \theta _0^{-1}\left (\frac {q_++q_-}{2}\right ) +I\theta _0^{-1}\left (\frac {q_+-q_-}{2}\right ).\] These formulas prove both multiplicativity and bijectivity.

Reversal becomes quaternion conjugation in each factor. If \(\mathbb H^1=\{q\in \mathbb H:\bar q q=1\}\) and \(\Phi (x)=(q_+,q_-)\), then \[\Phi (\operatorname {rev}(x)x) =(\bar q_+q_+,\bar q_-q_-),\qquad \operatorname {Spin}(Q_{4,0})\simeq \mathbb H^1\times \mathbb H^1.\] The forward restriction lands in the displayed product. Conversely, the written algebra inverse sends a pair of unit quaternions to an even unit of reverse norm one, and the dimension-four carrier lemma places it in the actual Spin group. No connectedness or covering-space argument is used.

Gallier computes the same \(u+Iv\mapsto (u+v,u-v)\) decomposition, norm equations, and compact group product using negative-square compact generators [gallier2014clifford, pp. 29--30]. Lawson--Michelsohn independently give the compact even-algebra reduction [lawson2016spin, I.3, Theorem 3.7, pp. 23--24] and the \(\mathbb H\oplus \mathbb H\) entry [lawson2016spin, I.4, Table I, p. 28]. Their relation \(v^2=-q(v)\) and the index translation of Convention [fcap-0011][fcap-0011] account for the sign change. The axis labels above are those fixed in Example [fcap-002H][fcap-002H], not labels imported from either source. Finally, \((1\pm I)/2\) are the two nonzero complementary central idempotents, so the even center is the split algebra \(\mathbb R\oplus \mathbb R\).

For \(Q_{4,0}=x_0^2+x_1^2+x_2^2+x_3^2\), keep the algebra map \(\Phi :\mathcal {C}\kern -2pt\ell ^+(Q_{4,0})\simeq \mathbb H\times \mathbb H\) of Example [fcap-002K][fcap-002K]. Write \(\Phi (s)=(q_+,q_-)\) for \(s\in \operatorname {Spin}(Q_{4,0})\). In the quaternion coordinates \[W(v_0e_0+v_1e_1+v_2e_2+v_3e_3)=-v_3-v_1i+v_0j-v_2k,\] the vector action is \[W(svs^{-1})=q_+W(v)\bar q_-.\] The signed permutation \(W\) identifies the Euclidean vector norm with the quaternion norm. Both factors are unit quaternions, so the right multiplier is the inverse of \(q_-\).

To prove the formula, let \(I=e_0e_1e_2e_3\) and use the quaternion subalgebra \(H_0\) from Example [fcap-002K][fcap-002K]. The vector \(e_3\) commutes with \(H_0\) and anticommutes with \(I\). Hence \(C(x)=e_3xe_3\) interchanges the two components of \(\Phi (x)\). The identities \[e_0e_3=-I e_1e_2,\qquad e_1e_3=I e_0e_2,\qquad e_2e_3=-I e_0e_1\] give \(\Phi _1(ve_3)=-W(v)\). Now \[(svs^{-1})e_3=s(ve_3)C(s^{-1}).\] Applying \(\Phi _1\) and negating proves the action formula. For the diagonal pair \((q,q)\), the vector \(e_3\) is fixed because \(W(e_3)=-1\); on its orthogonal complement \(W\) restricts to \(\eta _3\) of Example [fcap-003J][fcap-003J]. Thus the three-dimensional conjugation action is the diagonal case.

TauCeti chooses a different algebra equivalence, denoted here by \(\widehat \Phi \). Its bilinear-generator formula gives \[\begin {aligned} e_0e_1&\longmapsto (-k,-k),& e_0e_2&\longmapsto (j,-j),\\ e_0e_3&\longmapsto (i,i),& e_1e_2&\longmapsto (-i,i),\\ e_1e_3&\longmapsto (j,j),& e_2e_3&\longmapsto (k,-k) \end {aligned}\] TauCeti.realCliffordFourZeroEvenEquivQuaternionProd_ι. In particular, \(\widehat \Phi (I)=(1,-1)\). Define quaternion automorphisms \[\begin {aligned} A(a+bi+cj+dk)&=a-ci+bj+dk,\\ B(a+bi+cj+dk)&=a+ci-bj+dk. \end {aligned}\] They are conjugation by \((1+k)/\sqrt {2}\) and \((1-k)/\sqrt {2}\), respectively, and satisfy \(B(q)=kA(q)k^{-1}\). The rows for \(e_0e_1,e_0e_2,e_1e_2\) identify the restrictions to \(H_0\) as \(A\circ \theta _0\) and \(B\circ \theta _0\). Together with the image of \(I\), the decomposition \(x=u+Iu'\) therefore proves \[\widehat \Phi (x)=\bigl (A(\Phi _1(x)),B(\Phi _2(x))\bigr ).\]

TauCeti's vector coordinates are \[\eta _4(v)=-v_2+v_1i-v_0j+v_3k=A(W(v))k^{-1}\] TauCeti.realCliffordFourZeroQuaternionEquiv_apply. Since \(A,B\) commute with quaternion conjugation and \(A(\bar q)k^{-1}=k^{-1}\overline {B(q)}\), the formula for \(W\) gives \[\eta _4(svs^{-1})=A(q_+)\eta _4(v)\overline {B(q_-)}.\] This is precisely the action in the \(\widehat \Phi \) coordinates TauCeti.realSpinFourEquivQuaternionUnitaryProd_action. The displayed changes of coordinates derive its relation to the natural pair \(\Phi \) used in Example [fcap-002K][fcap-002K].

Gallier [gallier2014clifford, Section 1.4, pp. 29--30] gives the compact even-algebra decomposition into two quaternion factors with negative-square generators; Example [fcap-002K][fcap-002K] uses the positive-square convention. Porteous [porteous1995clifford, Chapter 8, Propositions 8.26--8.27, p. 65] describes the four-dimensional rotations \(z\mapsto qz\bar r\) for unit quaternions \(q,r\). The calculation with \(ve_3\) identifies these left and inverse-right factors for \(\Phi \); the explicit \(A,B,W,\eta _4\) formulas then give the coordinate translation to \(\widehat \Phi \).

For \(Q_{2,2}(v)=v_0^2+v_1^2-v_2^2-v_3^2\), the even Clifford algebra is a pair of real matrix algebras. We construct its coordinates to specify which Spin factor acts on each side of a vector. Set \(A=e_0e_1\), \(B=e_0e_2\), \(C=e_1e_2\), and \(I=e_0e_1e_2e_3\). The subalgebra \(H_0=\langle 1,A,B,C\rangle _{\mathbb R}\) has \(A^2=-1\), \(B^2=C^2=1\), and \(AB=-C\). Define \[J=\begin {pmatrix}0&1\\-1&0\end {pmatrix},\quad S=\begin {pmatrix}0&1\\1&0\end {pmatrix},\quad D=\begin {pmatrix}-1&0\\0&1\end {pmatrix}.\] The assignments \(\rho (A)=-J\), \(\rho (B)=D\), \(\rho (C)=S\) satisfy these relations and give a basis of \(M_2(\mathbb R)\) together with the identity. They define an algebra equivalence \(\rho \). The volume element \(I\) is central in the even algebra and \(I^2=1\). The eight even basis monomials give \(\mathcal {C}\kern -2pt\ell ^+(Q_{2,2})=H_0\oplus I H_0\). Hence the map \[\Phi (u+Iw)=\bigl (\rho (u)-\rho (w),\ S(\rho (u)+\rho (w))S\bigr )\] is an algebra equivalence to \(M_2(\mathbb R)\times M_2(\mathbb R)\). For a pair \((P,R)\), its inverse is recovered from \[\rho (u)=\tfrac 12(P+SRS),\qquad \rho (w)=\tfrac 12(SRS-P).\]

The reversion fixes \(I\) and negates \(A,B,C\). On \(H_0\), this is matrix adjugation, since \(\rho (A), \rho (B),\rho (C)\) are traceless. Conjugation by \(S\) commutes with adjugation, so \[\Phi (\operatorname {rev}(x))= \bigl (\operatorname {adj}(\Phi _1(x)), \operatorname {adj}(\Phi _2(x))\bigr ).\] Consequently \(\operatorname {rev}(x)x=1\) if and only if both component determinants are one. The carrier lemma Lemma [fcap-002J][fcap-002J] therefore restricts \(\Phi \), with the displayed inverse, to the actual group \[\operatorname {Spin}(Q_{2,2})\simeq SL_2(\mathbb R)\times SL_2(\mathbb R).\] Porteous's norm-one subgroup is denoted \(\operatorname {Spin}^+\); his split-four entry is a pair of \(Sp_2(\mathbb R)\) factors [porteous1995clifford, Chapter 17, Theorem 17.9 and Table 14, p. 159]. In degree two, \(M^{\mathsf T}JM=(\det M)J\), so these are precisely \(SL_2(\mathbb R)\). The norm-one restriction is essential to that comparison.

Our pair map has the following six bivector images: \[\begin {aligned} e_0e_1&\longmapsto (-J,J),& e_0e_2&\longmapsto (D,-D),\\ e_0e_3&\longmapsto (-S,S),& e_1e_2&\longmapsto (S,S),\\ e_1e_3&\longmapsto (D,D),& e_2e_3&\longmapsto (-J,-J). \end {aligned}\] In particular \(\Phi (I)=(-1,1)\). These are the specializations of TauCeti's bilinear-generator formula TauCeti.realCliffordTwoTwoEvenEquivMatrixProd_ι. Since the bivectors generate the even algebra, this identifies \(\Phi \) with its concrete even-algebra map and hence identifies the restricted group equivalence TauCeti.realSpinTwoTwoEquivSpecialLinearProd.

Now encode vectors by \[X(v)=\Phi _1(ve_3)S= \begin {pmatrix}-v_0-v_2&-v_1-v_3\\v_1-v_3&-v_0+v_2\end {pmatrix}.\] The inverse sends \(\begin {pmatrix}a&b\\c&d\end {pmatrix}\) to \((-(a+d)/2,(c-b)/2,(d-a)/2,-(b+c)/2)\). A determinant expansion gives \(\det X(v)=Q_{2,2}(v)\). Thus \(X\) identifies the whole vector space with the determinant quadratic space of real two-by-two matrices TauCeti.realCliffordTwoTwoVectorEquivMatrix_apply TauCeti.realCliffordTwoTwoVectorEquivMatrix_det. Writing \(\Phi (s)=(P,R)\) for a Spin element, the action is \[X(svs^{-1})=P X(v)R^{-1}.\]

For the proof, \(e_3^2=-1\), and conjugation \(\gamma (x)=-e_3xe_3\) fixes \(H_0\) and negates \(I\). Therefore \[\Phi (\gamma (x))= \bigl (S\Phi _2(x)S,\ S\Phi _1(x)S\bigr ).\] The identities \[e_0e_3=IC,\qquad e_1e_3=-IB,\qquad e_2e_3=-IA\] give the displayed formula for \(X\). Apply \(\Phi _1\) to \((svs^{-1})e_3=s(ve_3)\gamma (s^{-1})\), then multiply on the right by \(S\). Since \(S^2=1\), the result is \(P X(v)R^{-1}\). This proves TauCeti's exact coordinate action TauCeti.realSpinTwoTwoEquivSpecialLinearProd_action.

The diagram records the two ways to calculate the same action:

As in the compact action of Example [fcap-003K][fcap-003K], multiplication by a fixed vector makes an odd vector accessible to the even algebra, and conjugation by that vector interchanges its two factors. Here the factors are real matrices, with the explicit \(S\)-conjugations above. This is the even-algebra action transport of [porteous1995clifford, Chapter 16, Proposition 16.9, pp. 143--144] in the stated axes. The construction gives the group and its vector action; its orthogonal image retains the spinor-norm qualification of Theorem [fcap-0023][fcap-0023].

For \(Q_{1,3}=x_0^2-x_1^2-x_2^2-x_3^2\), put \(A_j=e_0e_j\) for \(1\le j\le 3\) and \(I=e_0e_1e_2e_3\). Then the \(A_j\) square to \(1\) and anticommute, while \[I^2=-1,\qquad A_1A_2A_3=-I.\] For the Pauli matrices \[\sigma _1=\begin {pmatrix}0&1\\1&0\end {pmatrix},\quad \sigma _2=\begin {pmatrix}0&-i\\i&0\end {pmatrix},\quad \sigma _3=\begin {pmatrix}1&0\\0&-1\end {pmatrix},\] the assignments \(\Psi (A_j)=\sigma _j\) define a real-algebra map from the even Clifford algebra to \(M_2(\mathbb C)\). Since \(\sigma _1\sigma _2\sigma _3=i1\), necessarily \(\Psi (I)=-i1\). The images of \(1,A_1,A_2,A_3,I,IA_1,IA_2,IA_3\) form a real basis, so \(\Psi \) is an algebra equivalence.

Write a matrix uniquely as \[M=z_0 1+z_1\sigma _1+z_2\sigma _2+z_3\sigma _3, \qquad z_j=a_j+i b_j,\] where \[\begin {aligned} z_0&=(m_{11}+m_{22})/2,&z_3&=(m_{11}-m_{22})/2,\\ z_1&=(m_{12}+m_{21})/2,&z_2&=(m_{21}-m_{12})/(2i). \end {aligned}\] Then an explicit inverse is \[\Psi ^{-1}(M) =a_0+\sum _{j=1}^3a_jA_j -I\left (b_0+\sum _{j=1}^3b_jA_j\right ).\] Reversal fixes \(I\) and negates every \(A_j\); under \(\Psi \) it is the complex-linear matrix adjugate. Hence \[\Psi (\operatorname {rev}(x))=\operatorname {adj}(\Psi (x)),\qquad \Psi (\operatorname {rev}(x)x)=\det (\Psi (x))1.\] For an arbitrary even \(x\), this norm is algebra-valued: the determinant may be complex, corresponding to the even center. It is not yet the real scalar-valued Lipschitz norm, and adjugation is not conjugate transpose.

Restriction therefore gives a homomorphism \(\operatorname {Spin}(Q_{1,3})\to SL_2(\mathbb C)\). Conversely, a determinant-one matrix has adjugate as a two-sided inverse. Its displayed Clifford preimage is an even unit with \(\operatorname {rev}(x)x=1\), so the dimension-four carrier lemma places it in Spin. The written inverse proves both compositions and multiplicativity: \[\operatorname {Spin}(Q_{1,3})\simeq SL_2(\mathbb C).\]

The source indices require translation. [lawson2016spin, I.3, Theorem 3.7, pp. 23--24] use \(v^2=-q(v)\) and give the even-algebra reduction \[\operatorname {Cl}^{0}_{3,1}\simeq \operatorname {Cl}_{2,1}.\] Their base entries and recurrence then give \[\operatorname {Cl}_{2,1}\simeq M_2(\mathbb C)\] [lawson2016spin, I.4, (4.0) and Theorem 4.1, p. 25].

Gallier uses the opposite indexing. The positive-square \(A_j\) exhibit \(\operatorname {Cl}_{3,0}\). [gallier2014clifford, Example 1.3, p. 33] records the matrix base entries, while [gallier2014clifford, Lemma 1.15, p. 34] supplies the recurrence. Together they give \[\operatorname {Cl}_{3,0} \simeq \operatorname {Cl}_{0,1}\otimes \operatorname {Cl}_{2,0} \simeq M_2(\mathbb C).\]

[porteous1995clifford, Chapter 17, Proposition 17.5, pp. 151--152] identifies his norm-one subgroup \(\operatorname {Spin}^{+}(1,3)\) with \(SL_2(\mathbb C)\). He computes reversal as adjugation. His broader mixed-sign carrier permits norm \(\pm 1\), and his displayed axes are not the Pauli axes fixed above.

Here the even center is \(\mathbb R[I]\simeq \mathbb C\), with no nonzero complementary central idempotents. This contrasts with the split compact center \(\mathbb R\oplus \mathbb R\), although both even algebras have real dimension eight. The full algebra \(\mathcal {C}\kern -2pt\ell _{1,3}\simeq M_2(\mathbb H)\) in Example [fcap-0026][fcap-0026] is a different algebra. The vector-action image remains the spinor-norm kernel from Theorem [fcap-0023][fcap-0023]; no topological component or concrete gamma-map claim is made.

Keep the Pauli convention of Example [fcap-002L][fcap-002L]: \(Q_{1,3}(v)=t^2-x_1^2-x_2^2-x_3^2\), \(A_j=e_0e_j\), and \(\Psi (A_j)=\sigma _j\). For \(Q_{3,1}(y)=y_0^2+y_1^2+y_2^2-y_3^2\), write \(f_0,\ldots ,f_3\) for the coordinate generators. The real linear bijection \[T(t,x_1,x_2,x_3)=(-x_2,x_1,-x_3,t)\] satisfies \(Q_{3,1}(Tv)=-Q_{1,3}(v)\). There is a real algebra equivalence \[E:\mathcal {C}\kern -2pt\ell ^+(Q_{1,3})\longrightarrow \mathcal {C}\kern -2pt\ell ^+(Q_{3,1}), \qquad E(vw)=-T(v)T(w).\] It preserves reversion and restricts to an equivalence of the actual Spin groups. Their vector actions satisfy \[T(svs^{-1})=E(s)T(v)E(s)^{-1}.\]

For the construction, complexify and send \(v\mapsto iT(v)\). Its square is \(Q_{1,3}(v)\), so the Clifford universal property gives an algebra map. On an even word of length \(2k\) its value is \((-1)^kT(v_1)\cdots T(v_{2k})\), which is real. This defines \(E\) by scalar extension as in Theorem [fcap-003V][fcap-003V]. The reverse construction sends \(w\mapsto iT^{-1}(w)\); the two composites negate generators and therefore fix every even word. Reversing an even word commutes with \(E\). The dimension-four carrier lemma Lemma [fcap-002J][fcap-002J] now identifies the reverse-norm-one even units on both sides, so \(E\) and its inverse restrict to the stated actual groups. Applying the complex map to \(svs^{-1}\) and cancelling \(i\) proves the action identity. This is the sign-transfer mechanism used for compact forms in Proposition [fcap-0039][fcap-0039], with the additional coordinate change \(T\).

The algebraic construction is also the composite of sign scaling and the isometry \(T:(-Q_{1,3})\to Q_{3,1}\). TauCeti's general scaling formula at the unit \(-1\) TauCeti.CliffordAlgebra.evenEquivEvenSMul_ι, its reversion compatibility TauCeti.CliffordAlgebra.evenEquivEvenSMul_reverseEven, and the isometry formula CliffordAlgebra.evenEquivOfIsometry_ι provide these three component statements. The displayed \(T\) and its Spin-action dictionary are the explicit specialization proved here.

Let \(\Phi :\mathcal {C}\kern -2pt\ell ^+(Q_{3,1})\to M_2(\mathbb C)\) be TauCeti's concrete matrix equivalence. Its bilinear-generator formula TauCeti.realCliffordThreeOneEvenEquivComplexMatrix_ι gives \[\begin {aligned} \Phi (f_0f_3)&=-\sigma _2,&\Phi (f_1f_3)&=\sigma _1,& \Phi (f_2f_3)&=-\sigma _3,\\ \Phi (f_0f_1)&=i\sigma _3,&\Phi (f_0f_2)&=i\sigma _1,& \Phi (f_1f_2)&=i\sigma _2. \end {aligned}\] Since \(T(e_0)=f_3\), \(T(e_1)=f_1\), \(T(e_2)=-f_0\), and \(T(e_3)=-f_2\), these formulas give \(\Phi (E(A_j))=\sigma _j\). The \(A_j\) generate the even algebra, hence \(\Phi \circ E=\Psi \). Also \(E(e_0e_1e_2e_3)=f_0f_1f_2f_3\), whose matrix is \(-i1\). Thus the Pauli group equivalence agrees, through \(E\), with TauCeti.realSpinThreeOneEquivSpecialLinear. This dictionary concerns the even algebras and their Spin actions; the full real Clifford algebras retain their different signature types.

In the Pauli model Example [fcap-002L][fcap-002L], an odd vector becomes an even element after multiplication by \(e_0\). Encode \(v=te_0+x_1e_1+x_2e_2+x_3e_3\) by \[X(v)=\Psi (ve_0)=t1-\sum _{j=1}^3x_j\sigma _j =\begin {pmatrix}t-x_3&-x_1+i x_2\\-x_1-i x_2&t+x_3\end {pmatrix}.\] A matrix is Hermitian when \(Z^*=Z\), where \(*\) denotes conjugate transpose. Every Hermitian two-by-two matrix has the form \(Z=\begin {pmatrix}a&z\\\overline z&d\end {pmatrix}\) with \(a,d\in \mathbb R\). The inverse coordinates are \[X^{-1}(Z)=\left (\frac {a+d}{2},-\operatorname {Re}z, \operatorname {Im}z,\frac {d-a}{2}\right ).\] Thus \(X\) is a real linear equivalence, and direct expansion gives \[\det X(v)=t^2-x_1^2-x_2^2-x_3^2=Q_{1,3}(v).\]

For \(s\in \operatorname {Spin}(Q_{1,3})\), put \(M=\Psi (s)\in SL_2(\mathbb C)\). Then the vector action is \[X(svs^{-1})=M X(v)M^*.\] To prove it, conjugation by \(e_0\) defines an automorphism \(\gamma (x)=e_0xe_0\) of the even algebra. It negates each \(A_j=e_0e_j\) and the volume element \(I=e_0e_1e_2e_3\). On the matrix side, \(M\mapsto \operatorname {adj}(M)^*\) has the same effect on \(\sigma _j\) and \(-i1\). It is a real algebra automorphism: both adjugation and conjugate transpose reverse products, and in size two adjugation is linear. Checking the even generators therefore gives \[\Psi (\gamma (x))=\operatorname {adj}(\Psi (x))^*.\] Now multiply the Clifford action by \(e_0\): \[(svs^{-1})e_0=s(ve_0)\gamma (s^{-1}).\] Since \(\det M=1\), we have \(\operatorname {adj}(M^{-1})=M\). Applying \(\Psi \) proves the congruence formula. It preserves Hermitian matrices, and its determinant is unchanged because \(\det M=\det M^*=1\).

The square makes the coordinate meaning of the action explicit:

For comparison with the formal opposite-signature model, use \(T\) and \(E\) from Lemma [fcap-003Z][fcap-003Z]. TauCeti's vector equivalence has coordinates \[H(y)=\begin {pmatrix}y_3+y_2&-y_1-i y_0\\ -y_1+i y_0&y_3-y_2\end {pmatrix},\qquad \det H(y)=-Q_{3,1}(y)\] TauCeti.coe_realCliffordThreeOneVectorEquivHermitian_apply TauCeti.realCliffordThreeOneVectorEquivHermitian_det. Substitution gives \(H(Tv)=X(v)\). In the even algebra this is the same identity as \(E(ve_0)=-T(v)f_3\), since \(H(y)=\Phi (-yf_3)\). The group coercion formula TauCeti.coe_realSpinThreeOneEquivSpecialLinear_apply identifies the matrix of \(E(s)\) with \(\Phi (E(s))=\Psi (s)=M\). Consequently the action dictionary in Lemma [fcap-003Z][fcap-003Z] translates TauCeti's exact Hermitian congruence theorem TauCeti.realSpinThreeOneEquivSpecialLinear_action into the displayed Pauli action. This checks both the signature sign and the matrix axes, not just the abstract group type.

Multiplication by a fixed nonisotropic vector is the even-algebra action mechanism of [porteous1995clifford, Chapter 16, Proposition 16.9, pp. 143--144]. His Lorentz group calculation uses adjugation and the norm-one carrier [porteous1995clifford, Chapter 17, Proposition 17.5, pp. 151--152]. The coordinates and conjugate-transpose action above are derived in our chosen axes. The orthogonal image retains the spinor-norm condition of Theorem [fcap-0023][fcap-0023]; a topological component identification is separate.

Let \(K\) be a field of characteristic different from two, and let \(q=\langle a,b,c,d\rangle \) with \(a,b,c,d\in K^\times \). Thus \(q(x)=ax_1^2+bx_2^2+cx_3^2+dx_4^2\). The center of its even Clifford algebra determines whether the quaternion description of its Spin group has two factors over \(K\) or one factor over a quadratic field. Put \[\begin {aligned} \delta &=abcd,\\ E&=K[t]/(t^2-\delta ),\\ D&=(-ab,-ac\mid K), \end {aligned}\] using the quaternion algebra notation. The class of \(\delta \) in \(K^\times /(K^\times )^2\) is the signed discriminant in dimension four; changing the diagonalizing basis changes the determinant by a square. Lam's center theorem identifies the corresponding quadratic algebra; the explicit quaternion and group identifications below follow by calculation [lam2005quadratic, V.2, thms. 2.2--2.5, pp. 109--111].

Extend quaternion conjugation \(\overline i=-i\), \(\overline j=-j\) \(E\)-linearly to \(D_E=D\otimes _K E\). Write \(SL_1(D_E)=\{x\in D_E:x\overline x=1\}\) for its norm-one group. Indeed, for \(x=x_0+x_1i+x_2j+x_3ij\), with \(x_r\in E\), \[x\overline x=\overline x x =x_0^2+abx_1^2+acx_2^2+a^2bcx_3^2\in E.\] This extends the reduced norm to the displayed quaternion algebra, and \(x^{-1}=\overline x\) when the norm is one. There are algebra and group isomorphisms \[\begin {aligned} \mathcal {C}\kern -2pt\ell ^+(q)&\simeq D_E,\\ Z(\mathcal {C}\kern -2pt\ell ^+(q))&\simeq E,\\ \operatorname {Spin}(q)&\simeq SL_1(D_E), \end {aligned}\] where the algebra isomorphism takes grade reversion to quaternion conjugation. If \(\delta \) is a square in \(K^\times \), this gives \[\operatorname {Spin}(q)\simeq SL_1(D)\times SL_1(D).\] If \(\delta \) is nonsquare, it gives \[\operatorname {Spin}(q)\simeq SL_1(D\otimes _K K(\sqrt \delta )).\] All groups here consist of points over the indicated fields.

For a concrete comparison, take \(q_d=\langle 1,-1,1,-d\rangle \). Then \(\delta =d\) and \(D=(1,-1\mid K)\). The matrices \[i\longmapsto \begin {pmatrix}1&0\\0&-1\end {pmatrix},\qquad j\longmapsto \begin {pmatrix}0&1\\-1&0\end {pmatrix}\] have squares \(1,-1\), anticommute, and, together with their product and the identity, form a basis of \(M_2(K)\). They therefore identify \(D\) with \(M_2(K)\). Conjugation becomes matrix adjugation and the norm becomes the determinant, giving \(\operatorname {Spin}(q_d)\simeq SL_2(E)\). In particular, over \(K=\mathbb Q\), the members \(q_1\) and \(q_2\) satisfy \[\begin {aligned} \operatorname {Spin}(q_1)(\mathbb Q) &\simeq SL_2(\mathbb Q)\times SL_2(\mathbb Q),\\ \operatorname {Spin}(q_2)(\mathbb Q) &\simeq SL_2(\mathbb Q(\sqrt 2)). \end {aligned}\] These identities apply the proposition to the two centers \(\mathbb Q\times \mathbb Q\) and \(\mathbb Q(\sqrt 2)\).

The split-center group equivalence has a formal counterpart in CliffordAlgebra.spinGroupEquivSplitCenterCorners, given a center isomorphism with \(K\times K\). The field-center existence theorem CliffordAlgebra.exists_spinGroupEquivQuaternionUnitaryOverCenter_of_finrank_eq_four gives a quaternion norm-one model over the actual even center. Both assume nondegeneracy and dimension four over a field with two invertible. The explicit parameters \(-ab,-ac\) and the matrices for \(q_d\) are supplied by the calculation above.

Let \(K\) be a field of characteristic different from two, and let \((V,Q)\) be a nondegenerate quadratic space of dimension five over \(K\). For \(x\in \mathcal {C}\kern -2pt\ell ^{+}(Q)\), \[x\text { is the Clifford value of a Spin element} \quad \Longleftrightarrow \quad \operatorname {rev}(x)x=1.\] The norm condition implies Lipschitz membership in this dimension CliffordAlgebra.evenUnitaryGroup_le_lipschitzGroup_of_finrank_eq_five. The point is to remove the possible degree-five term left by the dimension-four argument of Lemma [fcap-002J][fcap-002J].

Choose an orthogonal basis \(e_1,\ldots ,e_5\), suppress the generator map, and put \(\omega =e_1\cdots e_5\). Nondegeneracy gives \[\omega ^2=\delta 1,\qquad \delta =\prod _{i=1}^5 Q(e_i)\ne 0.\] The element \(\omega \) is central and invertible. Suppose \(\operatorname {rev}(x)x=1\). Finite dimensionality makes the left inverse a two-sided inverse. For any \(v\in V\), the element \(y=xvx^{-1}\) is odd and satisfies \(\operatorname {rev}(y)=y\). In the orthogonal monomial basis, reversal has signs \(+1,-1,+1\) on degrees one, three and five. Hence \[y=w+c\omega \qquad (w\in V,\ c\in K).\]

Conjugation preserves the scalar square of a vector. Since \(\omega \) is central, \[Q(v)1=y^2=Q(w)1+2c\omega w+c^2\delta 1.\] Each \(\omega e_i\) is a nonzero scalar multiple of the product of the other four basis vectors. Thus \(\omega w\) has pure degree four in this basis, whereas the other terms in the equation are scalar. Independence of the Clifford basis gives \(2c\omega w=0\). As two and \(\omega \) are invertible, either \(c=0\) or \(w=0\). In the latter case \(y=c\omega \) is central, so conjugating back gives \(v=x^{-1}yx=y=c\omega \). The degree-one and degree-five subspaces have zero intersection; therefore \(v=0\) and \(c=0\). In both cases \(y\in V\).

Thus \(x\) normalizes the vector space. The Clifford-group characterization makes it Lipschitz; together with evenness and reverse norm one, this is the Spin criterion of Remark [fcap-0028][fcap-0028]. The reverse implication is that same criterion. In fact the carrier equality holds in every dimension from one through five CliffordAlgebra.range_spinGroup_toUnits_eq_evenUnitaryGroup. The lower bound matters: in dimension zero the vector-generated Lipschitz group is trivial, whereas the even-unitary group contains both \(1\) and \(-1\). This carrier equality alone supplies no symplectic matrix model; the spinor pairing and matrix inverse for complex dimension five remain the separate argument of Proposition [fcap-0033][fcap-0033].

Porteous gives the real dimension-five proof by separating the vector, trivector and volume terms [porteous1995clifford, Chapter 16, Proposition 16.15, p. 147]. His relation is \(v^2=-q(v)\), so here \(Q=-q\); his conjugation is \(\operatorname {rev}\circ \alpha \), equal to reversal on even elements. His indefinite Spin carrier permits norm \(\pm 1\); we select norm \(+1\). The basis calculation above extends the norm-one argument from real spaces to the stated fields: orthogonality, nonzero basis squares and invertibility of two replace any need for real unit-length normalization. Gallier records the compact boundary at five and the failure at six [gallier2014clifford, Section 1.4, closing Remark, p. 31]; the next example computes that failure.

Let \(K\) be a field of characteristic different from two, and let \((V,Q)\) be a finite-dimensional nondegenerate quadratic space containing six orthogonal vectors \(e_1,\ldots ,e_6\) with \(Q(e_i)\ne 0\). Put \[\omega =e_1\cdots e_6,\qquad \delta =\prod _{i=1}^6 Q(e_i).\] Now \(\omega \) is even, \(\operatorname {rev}(\omega )=-\omega \), and \(\omega ^2=-\delta 1\). It anticommutes with each of the six displayed vectors. If \(a,b\in K\) satisfy \(a^2+\delta b^2=1\), then \[x=a+b\omega ,\qquad x^{-1}=\operatorname {rev}(x)=a-b\omega \] is an even unit of reverse norm one. Its action on a displayed basis vector is \[xe_i x^{-1}=(a^2-\delta b^2)e_i+2ab\omega e_i.\]

For \(ab\ne 0\), the last term is a nonzero degree-five monomial, up to a scalar. Extend the six vectors to an orthogonal basis; independence of the Clifford monomials shows that the displayed conjugate is not a vector. Since \(x\) is even, ordinary and twisted conjugation agree. Thus \(x\) is not Lipschitz and cannot belong to Spin, despite satisfying the norm equation CliffordAlgebra.notMem_lipschitzGroup_of_mem_evenUnitaryGroup_of_coe_eq. Only the selected six vectors are used: in higher dimension \(\omega \) commutes with an additional orthogonal vector, which does not affect this counterexample.

For a concrete compact example, take \(K=\mathbb R\) and \(Q(v)=v_1^2+\cdots +v_6^2\). With \(a=b=1/\sqrt 2\), one obtains \[x=\frac {1+\omega }{\sqrt 2},\qquad \operatorname {rev}(x)x=1,\qquad xe_1x^{-1}=\omega e_1=-e_2e_3e_4e_5e_6.\] Porteous [porteous1995clifford, Chapter 16, p. 146] exhibits the unnormalized element \(1+\omega \) of norm two.

Gallier [gallier2014clifford, Section 1.4, closing Remark, p. 31] uses the normalized element above.

Their compact generators square to \(-1\). With that choice the same six-vector product still squares to \(-1\), but \(\omega e_1=+e_2e_3e_4e_5e_6\). Both signs give the same obstruction. The calculation here uses the positive-square convention of Example [fcap-002H][fcap-002H].

Over any infinite \(K\) as above, the conic always supplies \(a,b\ne 0\). Indeed, choose \(t\ne 0\) with \(1+\delta t^2\ne 0\) and \(1-\delta t^2\ne 0\), and set \[a=\frac {1-\delta t^2}{1+\delta t^2},\qquad b=\frac {2t}{1+\delta t^2}.\] Only finitely many values of \(t\) are excluded, and substitution gives \(a^2+\delta b^2=1\). Consequently the Spin image is a proper subgroup of the even-unitary group for every nondegenerate form of dimension at least six over an infinite field of characteristic different from two CliffordAlgebra.range_spinGroup_toUnits_ne_evenUnitaryGroup_of_six_le_finrank. This field extension follows from the displayed calculation; the cited book passages concern real spaces. Over a finite field the conditional six-vector construction remains valid, but this infinitude argument makes no assertion that a suitable conic point exists.

The mixed \((1,1)\) recurrence removes matched axes but leaves a one-sided algebra \(\mathcal {C}\kern -2pt\ell _{r,0}\) or \(\mathcal {C}\kern -2pt\ell _{0,r}\), which it cannot classify. Together with the signature switch in Theorem [fcap-001X][fcap-001X] and initial entries in Example [fcap-0015][fcap-0015], the two recurrences below complete the calculation.

The two one-sided recurrences are \[\begin {aligned} \mathcal {C}\kern -2pt\ell _{p,q+2}&\simeq \mathcal {C}\kern -2pt\ell _{q,p}\otimes _{\mathbb R}\mathbb H,\\ \mathcal {C}\kern -2pt\ell _{p+8,q}&\simeq \mathcal {C}\kern -2pt\ell _{p,q}\otimes _{\mathbb R}M_{16}(\mathbb R). \end {aligned}\] The first line is the actual equivalence TauCeti.realCliffordQuaternionRecurrenceEquiv. For the second, the formal theorem supplies existence TauCeti.nonempty_realCliffordEightPeriodicityEquiv.

They yield the residue-indexed mod-eight classification TauCeti.realClifford_classification. The classical table is [lawson2016spin, I.4, Theorem 4.3 and Tables I--II, pp. 27--29].

Use the convention of Convention [fcap-0011][fcap-0011]: \(p\) counts positive squares, \(q\) counts negative squares, and a Clifford generator obeys \(v^2=Q(v)1\). Then the real algebra for one positive and three negative axes is \[\mathcal {C}\kern -2pt\ell _{1,3}\simeq M_2(\mathbb H).\] The Tau Ceti classification theorem states existence of an abstract real algebra equivalence. Here \(q-p=2\) is its residue modulo \(8\), and its matrix size is \(2^{(p+q-2)/2}=2\).

[chevalley1954algebraic, II.2.9, pp. 65--66] uses the same positive/negative index convention. Split off one hyperbolic plane of signature \((1,1)\); the orthogonal remainder is a negative plane of signature \((0,2)\). Chevalley's dimension-two definite calculation on p. 66 identifies its Clifford algebra with \(\mathbb H\). The hyperbolic-plane theorem [chevalley1954algebraic, II.2.1, pp. 42--43] gives \(\mathcal {C}\kern -2pt\ell _{1,1}\simeq M_2(\mathbb R)\).

[chevalley1954algebraic, II.2.5, pp. 45--46] gives an orthogonal-sum tensor-product formula for an even-dimensional nondegenerate first summand; the second quadratic form is twisted. Here normalized hyperbolic generators \(e^2=1\) and \(f^2=-1\) have volume \(J=ef\) with \(J^2=1\). For a vector \(v\) in the orthogonal remainder, \(Jv\) commutes with \(e,f\) and still squares to \(Q(v)\). Since \(v=J(Jv)\), these commuting factors generate the full algebra. Thus the special hyperbolic split leaves that remainder unchanged: \[\begin {aligned} \mathcal {C}\kern -2pt\ell _{1,3}&\simeq \mathcal {C}\kern -2pt\ell _{1,1}\otimes _{\mathbb R}\mathcal {C}\kern -2pt\ell _{0,2}\\ &\simeq M_2(\mathbb R)\otimes _{\mathbb R}\mathbb H \simeq M_2(\mathbb H). \end {aligned}\] Both sides have real dimension \(16=2^4=4\dim _{\mathbb R}\mathbb H\). By comparison, \(M_4(\mathbb C)\) has real dimension \(32\). This abstract classification alone does not identify any particular gamma-matrix map, its kernel, or its image; the concrete Dirac map is treated in Proposition [fcap-002U][fcap-002U].

On \(\mathbb R^4\), let \[q_\gamma (v)=v_0^2-v_1^2-v_2^2-v_3^2.\] Under the coordinate identification \(\operatorname {Fin}(4)=\operatorname {Fin}(1+3)\), the identity map is an isometry from \(q_\gamma \) to the signature form \(Q_{1,3}\) of Example [fcap-0026][fcap-0026]. This is equality of the displayed forms, rather than only equality of their signatures. Thus the Clifford transport of Proposition [fcap-0029][fcap-0029] and the classification in Example [fcap-0026][fcap-0026] give \[\mathcal {C}\kern -2pt\ell (q_\gamma )\simeq \mathcal {C}\kern -2pt\ell _{1,3}\simeq M_2(\mathbb H)\] as real algebras. The selected formal ingredients are the coordinate formula TauCeti.realCliffordForm_apply and the residue-two classification TauCeti.realClifford_classification_of_residue_eq_two; the latter supplies existence of an abstract equivalence, not a theorem about a particular gamma-matrix map.

Let \(\xi :\operatorname {Fin}(1)\sqcup \operatorname {Fin}(3) \simeq \operatorname {Fin}(4)\) be the standard index equivalence, and write \[\Gamma _i=\operatorname {endEquivMatrix} \bigl (\operatorname {gamma}(\xi ^{-1}i)\bigr ).\] These are the concrete matrices \(\gamma ^0,\gamma ^1,\gamma ^2,\gamma ^3\); their squares are \(+1,-1,-1,-1\), and distinct matrices anticommute. Put \[D_\gamma =\operatorname {Alg}_{\mathbb R} \langle \Gamma _0,\Gamma _1,\Gamma _2,\Gamma _3\rangle \subset M_4(\mathbb C).\] Physlib constructs the real unital algebra homomorphism \[\rho :\mathcal {C}\kern -2pt\ell (q_\gamma )\longrightarrow D_\gamma ,\qquad \rho \bigl (\iota _{q_\gamma }(v)\bigr )=\sum _{i=0}^3v_i\Gamma _i\] from the Clifford universal property and proves that it is surjective onto \(D_\gamma \); see the generator-map source and the surjectivity source. The codomain here is the generated real subalgebra, not all of \(M_4(\mathbb C)\).

It remains to prove that this actual map has zero kernel. First, \(M_2(\mathbb H)\) is simple. Let \(J\) be a nonzero two-sided ideal, choose a matrix \(A\in J\) with nonzero entry \(a=A_{ij}\), and let \(E_{kl}(b)\) denote the matrix whose only nonzero entry is \(b\) in position \((k,l)\). Since every nonzero quaternion is invertible, for all \(k,l\) one has \[E_{ki}(a^{-1})\,A\,E_{jl}(1)=E_{kl}(1)\in J.\] The order of the factors matters over \(\mathbb H\). Taking both diagonal matrix units and adding them gives \(1\in J\), so \(J=M_2(\mathbb H)\). Transport through the preceding equivalence makes \(\mathcal {C}\kern -2pt\ell (q_\gamma )\) simple. Hence \(\ker \rho \) is zero or the entire source. The second option is impossible because \(\rho \) is unital and the identity matrix in \(D_\gamma \subset M_4(\mathbb C)\) is nonzero. Therefore \(\rho \) is injective; together with the formal surjectivity, this proves that this same map is a real algebra equivalence \[\mathcal {C}\kern -2pt\ell (q_\gamma )\simeq _{\rho }D_\gamma .\]

Consequently \[\dim _{\mathbb R}D_\gamma =\dim _{\mathbb R}M_2(\mathbb H)=4\cdot 4=16.\] For the ambient algebra, \[\dim _{\mathbb R}M_4(\mathbb C)=16\cdot 2=32.\] Thus \(D_\gamma \) is a proper real subalgebra of the ambient complex matrix algebra. This conclusion uses the proved equivalence and does not assume the image dimension in order to deduce injectivity.

Lawson--Michelsohn invoke simplicity of \(M_n(K)\) for \(K=\mathbb R,\mathbb C,\mathbb H\) in their real representation theorem [lawson2016spin, I.5, Theorem 5.6, pp. 31--32]. The matrix-unit calculation above supplies that step for the quaternionic algebra and then applies it to Physlib's concrete homomorphism. Their convention is \(v^2=-q(v)1\), so our \(\mathcal {C}\kern -2pt\ell _{1,3}\) is their \(\mathcal {C}\kern -2pt\ell _{3,1}\). Their algebra in that convention is the quaternionic matrix algebra used in the simplicity argument. The abstract classification is formalized in Tau Ceti, and Physlib formalizes the concrete map and its surjectivity. The simplicity and kernel argument completing the equivalence here is informal; no whole-card formal badge is asserted.

Move a generator through the word using \[\iota (u)\iota (v)+\iota (v)\iota (u)=B_Q(u,v)1.\] The swapped word contributes the alternating sign, whereas the polar term has two fewer generators. Iterating separates the fully alternating word from terms in \(F_{n-2}\). Equivalently, changing from \(Q\) to the zero quadratic form changes a word only below its leading filtration degree.

The assignment \(v\mapsto \iota _{Q_L}(1\otimes v)\) has square \(Q(v)1\). The universal property extends it to a \(K\)-algebra map; extending scalars gives \(\beta _Q\). For the inverse, take the \(L\)-linear map \[j:V_L\longrightarrow L\otimes _K\mathcal {C}\kern -2pt\ell _K(Q),\qquad j(a\otimes v)=a\otimes \iota _Q(v).\] The Clifford anticommutator is \(\iota _Q(v)\iota _Q(w)+ \iota _Q(w)\iota _Q(v)=B_Q(v,w)1\). Thus, for \(x=\sum _i a_i\otimes v_i\), \[j(x)^2=\left (\sum _i a_i^2Q(v_i)+ \sum _{i<j}a_ia_jB_Q(v_i,v_j)\right )1=Q_L(x)1.\] The same universal property therefore extends \(j\) to an \(L\)-algebra map in the opposite direction. Both composites fix scalars and vector generators, so they are identities. For \(Q=0\), this argument gives \(\beta _\wedge \). The two maps and their inverses preserve word length and parity because they send generators to generators.

Parity changes the sign of each generator, so it fixes a product of two. Reversal exchanges the order of those generators. Applied to the half-commutator, the exchange negates it. Linearity then gives the same sign on the exterior-square image CliffordAlgebra.reverse_bivectorExterior. The bivector is even CliffordAlgebra.bivector_mem_evenOdd_zero; on any even element reversal also agrees with Clifford conjugation \(x\mapsto x^*\), since parity is the identity there CliffordAlgebra.reverse_eq_star_of_mem_even.

Pairwise orthogonality gives \(\iota _Q(v_i)\iota _Q(v_j)=-\iota _Q(v_j)\iota _Q(v_i)\) for \(i\ne j\). Move each factor of the second copy of \(\omega _\ell \) next to its matching factor in the first copy. This takes \((n-1)+(n-2)+\cdots +1=\binom n2\) swaps. Each adjacent pair then contracts to \(\iota _Q(v_i)^2=Q(v_i)1\), giving the formula.

The generator-square rule CliffordAlgebra.ι_sq_scalar and the anticommutator rule CliffordAlgebra.ι_mul_ι_add_swap give \[\iota (v)\iota (w)+\iota (w)\iota (v)=B_Q(v,w).\] Since \(\alpha (\iota (v))=-\iota (v)\) and \(\iota (v)^2=Q(v)\), substitution yields \[-\iota (v)\iota (w)\frac {\iota (v)}{Q(v)} =\iota (w)-\frac {B_Q(v,w)}{Q(v)}\iota (v) =\iota (\rho _v(w)).\] The ordinary adjoint differs by the leading minus sign; the twisted adjoint is the action that gives the reflection itself.

The displayed square identity gives \(Q(cv)Q(w)=c^2Q(v)Q(w)=1\). Each generator is a Clifford unit and lies in the Lipschitz group, while the star calculation above establishes the unitary condition. The twisted adjoint is multiplicative on Clifford units, and scalar rescaling does not change a reflection. Hence the action of \(x\) is \(\rho _{cv}\rho _w=\rho _v\rho _w\); its even degree supplies the remaining Spin condition.

Cartan proves reflection factorization by an induction that enlarges the fixed subspace. TauCeti formalizes the correction as a list of at most two anisotropic reflections whose product with \(g\) fixes \(W+Kx\) pointwise TauCeti.QuadraticMap.exists_reflectionOrthogonal_list_prod_mul_eqOn_sup_span_singleton. The statement below repackages that list-valued result: when \(H\) contains every reflection, closure under products places the correcting element in \(H\).

Let \(K\) be a field of characteristic different from \(2\), let \(Q\) be a quadratic form on a \(K\)-vector space \(V\), and let \(H\le O(V,Q)\) contain every reflection in a nonisotropic vector. Suppose \(g\in O(V,Q)\) fixes a subspace \(W\) pointwise and \(x\in W^{\perp }\) has \(Q(x)\ne 0\). Then there is an element \(r\in H\) such that \[rg\vert _{W+Kx}=\operatorname {id}.\] The correction leaves the previously fixed space untouched and fixes one additional nonisotropic direction. It is either one reflection or a product of two reflections.

Under the hypotheses of Lemma [fcap-000V][fcap-000V], suppose moreover that \(K\) is separably closed and take \(H\) to be the range of the Pin action. Over a separably closed field, TauCeti's fixed-sign square condition from Theorem [fcap-000X][fcap-000X] holds, so every reflection factor used by the correction has a square-normalized Pin lift by Lemma [fcap-000B][fcap-000B]. The correcting element \(r\) can therefore be chosen in \[\operatorname {range}(\operatorname {pinToOrthogonal}),\] and still satisfies \(rg\vert _{W+Kx}=\operatorname {id}\). The statement concerns the correcting element in the Pin-action range; in the exceptional case it is the image of a product of two Pin lifts, not the image of a single reflecting vector.

Let \(K\) be a field of characteristic different from \(2\), let \(V\) be finite-dimensional, and let \(Q\) be nondegenerate. Every orthogonal transformation is a product of reflections in nonisotropic vectors. Equivalently, if a subgroup \(H\le O(V,Q)\) contains every such reflection, then \[H=O(V,Q).\] This formulation asserts generation only; it records neither a sharp bound on the number of reflection factors nor a parity formula for such a factorization.

Let \(K\), \(V\), and \(Q\) be as in Theorem [fcap-000W][fcap-000W]. Suppose every scalar \(-Q(v)^{-1}\) attached to a nonisotropic vector is a square in \(K\). Then the twisted-adjoint homomorphism is surjective: \[\operatorname {pinToOrthogonal}:\operatorname {Pin}(V,Q)\twoheadrightarrow O(V,Q).\] Indeed, Lemma [fcap-000B][fcap-000B] puts every reflection in its range, and Theorem [fcap-000W][fcap-000W] says that those reflections generate the target. In particular the conclusion holds over a separably closed field.

Lawson and Michelsohn ask whether a nonzero vector can be rescaled to quadratic length either \(+1\) or \(-1\); see (2.26) and the discussion preceding Theorem 2.9. Under the convention \(Q=-q\), TauCeti's hypothesis asks for the particular scalar \(-Q(v)^{-1}\) to be a square, so every reflecting vector is normalized to one fixed sign. This is a sufficient and generally stronger condition, not an equivalent reformulation of Lawson--Michelsohn's condition.

In an oriented Euclidean plane, let \(u\) and \(v\) be unit normals whose directed angle is \(\frac {\theta }{2}\). Reflection in \(u^{\perp }\) followed by reflection in \(v^{\perp }\) is rotation through \(\theta \). With the convention \(Q=-\langle -,-\rangle \), both vectors have \(Q=-1\), and \[s=\iota (v)\iota (u)\in \operatorname {Spin}(V,Q)\] lifts that rotation. In an oriented orthonormal basis \(e_1,e_2\), the familiar rotor form is \[\pm s=\cos \left (\frac {\theta }{2}\right )+\sin \left (\frac {\theta }{2}\right )\,\iota (e_1)\iota (e_2),\] after choosing the central sign and the order convention for the two reflections. This is the two-dimensional specialization of the paired lift in Theorem [fcap-000C][fcap-000C]; the half-angle appears because the Spin element acts by conjugation on vectors.

Let \(R\) be a commutative ring in which \(2\) is invertible, let \(M\) be a finite free \(R\)-module, and let \(Q\) be a quadratic form on \(M\). A reflection in a vector of invertible quadratic value has determinant \(-1\). Therefore a product of \(r\) such reflections has determinant \[(-1)^r.\] In particular, every product of an even number of reflections belongs to \(SO(M,Q)\).

Lawson--Michelsohn state this parity argument for quadratic vector spaces over a field. The finite-free commutative-ring statement above is the formalized extension: its determinant calculation uses freeness and finiteness, while invertibility of \(2\) identifies the fixed part of the grading involution with the even subalgebra.

The Clifford lift remembers this parity. If \(p\in \operatorname {Pin}(M,Q)\) and its orthogonal action has determinant \(1\), then \(p\) lies in the even Clifford subalgebra. Hence \(p\) is a Spin element. Thus any Pin lift of a special orthogonal transformation is automatically even.

Let \(K\) be a field of characteristic different from \(2\), let \(V\) be finite-dimensional, and let \(Q\) be nondegenerate. Suppose that for every nonisotropic \(v\in V\), the scalar \(-Q(v)^{-1}\) is a square in \(K\). Then the twisted-adjoint action restricts to a surjection \[\operatorname {Spin}(V,Q)\twoheadrightarrow SO(V,Q).\] The underlying homomorphism is CliffordAlgebra.spinToSpecialOrthogonal, and its action on vectors is the usual Spin action by CliffordAlgebra.coe_spinToSpecialOrthogonal_apply.

Indeed, the square-normalization hypothesis and Cartan--Dieudonne generation give the Pin surjection of Theorem [fcap-000X][fcap-000X]. It lifts an element of \(SO(V,Q)\) to Pin; the lift has determinant \(1\), so Lemma [fcap-001A][fcap-001A] shows that it is even and therefore lies in Spin. The restriction square

The square condition is TauCeti's fixed-sign sufficient hypothesis, stronger in general than Lawson--Michelsohn's option to normalize each vector to either sign; see Theorem [fcap-000X][fcap-000X]. For a positive-definite real geometric form \(q\), the Clifford convention is \(Q=-q\); hence \(-Q(v)^{-1}>0\) for every nonzero \(v\), so the reflecting vectors can be normalized over \(\mathbb {R}\). This observation does not assert the square condition for arbitrary real signatures.

Let \(K\) be a field of characteristic different from two, let \(V\) be a positive-dimensional finite-dimensional \(K\)-space, and let \(Q\) be nondegenerate. Write \(\Gamma (Q)\) for the vector-generated Lipschitz group, and \(\tau _Q:\Gamma (Q)\to O(V,Q)\) for its twisted action. For \(x\in \Gamma (Q)\), let \(N_{\mathrm {rev}}(x)\in K^{\times }\) be the unique scalar unit satisfying \(\operatorname {rev}(x)x=N_{\mathrm {rev}}(x)\,1\). Set \(\mathcal {S}_K=K^{\times }/(K^{\times })^2\). The top row is exact, and the square commutes:

If \(Q(v)\) is nonzero, then \[N_{\mathrm {rev}}(\widehat v)=Q(v),\qquad \nu _Q^O(r_v)=[Q(v)]\] CliffordAlgebra.cliffordNorm_unitι CliffordAlgebra.orthogonalSpinorNorm_reflectionOrthogonal. Consequently, for an even product \(x=\widehat v_1\cdots \widehat v_{2k}\) of nonisotropic vector lifts, \[\tau _Q(x)=r_{v_1}\cdots r_{v_{2k}}\in SO(V,Q),\qquad \nu _Q(r_{v_1}\cdots r_{v_{2k}}) =\left [\prod _{i=1}^{2k}Q(v_i)\right ].\] Multiplying a lift by \(c\in K^\times \) changes its reverse norm by \(c^2\), so the square class is independent of the chosen lift. [chevalley1954algebraic, II.3.5--6, pp. 52--53] gives these vector and paired-product values. The scalar exact sequence, reflection factorization, and the same square-scaling law appear in [meinrenken2013clifford, Theorem 3.1, pp. 50--51]. Chevalley's quotient statement assumes positive dimension; Meinrenken works with a finite-dimensional characteristic-zero nondegenerate bilinear space.

If \(e:(V,Q)\simeq (V',Q')\) is an isometry equivalence, then conjugation transport preserves both norms: for \(g\in O(V,Q)\) and \(h\in SO(V,Q)\), \[\nu _{Q'}^O(ege^{-1})=\nu _Q^O(g),\qquad \nu _{Q'}(ehe^{-1})=\nu _Q(h).\] It therefore carries \(\ker \nu _Q\) onto \(\ker \nu _{Q'}\) QuadraticMap.IsometryEquiv.orthogonalSpinorNorm_orthogonalGroupCongr QuadraticMap.IsometryEquiv.spinorNorm_specialOrthogonalGroupCongr kernel-transport source. The induced kernel equivalence also commutes with Spin transport Spin-transport source. These are isometry-equivalence statements; they do not assert scalar-extension or orthogonal-product naturality. This is the norm-square companion to the vector-action square in Proposition [fcap-0029][fcap-0029].

Let \(K\) be a field in which \(2\) is invertible, \(V\) a finite-dimensional \(K\)-space, and \(Q\) a nondegenerate quadratic form. The Clifford norm of a Lipschitz lift, taken modulo squares, descends to \(\nu _Q^O:O(V,Q)\to K^{\times }/(K^\times )^2\) CliffordAlgebra.orthogonalSpinorNorm_lipschitzToOrthogonal. Its restriction to \(SO(V,Q)\) is the spinor norm \(\nu _Q:SO(V,Q)\to K^\times / (K^\times )^2\) CliffordAlgebra.spinorNorm. Then \[\operatorname {im}\bigl (\operatorname {Spin}(V,Q)\to SO(V,Q)\bigr ) =\ker \nu _Q.\] Thus a special orthogonal transformation has a Spin lift exactly when its spinor-norm class is trivial.

[chevalley1954algebraic, II.3.5--6, pp. 52--53] defines the reversal norm and describes the reduced orthogonal image by square classes of products \(Q(u)Q(v)\). His ordinary Clifford action and reversal norm compare with TauCeti's twisted action on even lifts: grading fixes such lifts, so the two actions agree, and reverse and star norms coincide Remark [fcap-0028][fcap-0028]. For a single nonisotropic reflection, the descended orthogonal spinor norm is \[\nu _Q^O(r_v)=[Q(v)]\] CliffordAlgebra.orthogonalSpinorNorm_reflectionOrthogonal. This agrees with Chevalley's reverse norm. TauCeti's star norm on the odd vector lift has class \([-Q(v)]\); it is a different norm. The extra minus sign cancels on an even product, where the reverse and star norms agree.

Let \(L/K\) be an extension of fields of characteristic different from two. Let \(V\) be a positive-dimensional finite-dimensional \(K\)-space, and let \(Q\) be nondegenerate. Set \(V_L=L\otimes _K V\), with extended form \(Q_L\), and write \[j:K^{\times }/(K^\times )^2\longrightarrow L^{\times }/(L^\times )^2, \qquad j([a]_K)=[a]_L.\] For \(g\in O(V,Q)\), scalar extension gives \(g_L(a\otimes v)=a\otimes g(v)\). Then \[\nu _{Q_L}^O(g_L)=j\bigl (\nu _Q^O(g)\bigr ).\] In particular, for \(g\in SO(V,Q)\), \[\nu _{Q_L}(g_L)=j\bigl (\nu _Q(g)\bigr ),\] and \(g_L\) has a Spin lift exactly when \(j(\nu _Q(g))=1\).

The Clifford map \(c:\mathcal {C}\kern -2pt\ell (Q)\to \mathcal {C}\kern -2pt\ell (Q_L)\) sends \(\iota _Q(v)\) to \(\iota _{Q_L}(1\otimes v)\). It preserves parity, reversal and products, and carries each nonisotropic vector unit to a nonisotropic vector unit. Thus it restricts to a map of the actual Spin carriers, and their vector actions satisfy \[q_L(c(s))=(q_K(s))_L\qquad (s\in \operatorname {Spin}(Q)),\] where \(q_K\) and \(q_L\) denote the Spin projections. Indeed, apply \(c\) to the conjugation identity on every vector generator. A lift defined over \(K\) therefore remains a lift over \(L\); the next proposition explains how additional lifts can appear when \(j\) kills a nontrivial square class.

[chevalley1954algebraic, Section 2.7, pp. 60--61] describes the Clifford extension, compatibility with the main antiautomorphism, and the group/vector-action inclusions in even dimension. His main antiautomorphism is reversal. The reflection proof above gives the stated naturality in every positive dimension, using the reverse-norm convention of Proposition [fcap-002D][fcap-002D].

TauCeti proves the orthogonal and special-orthogonal identities in CliffordAlgebra.orthogonalSpinorNorm_orthogonalGroupBaseChange and CliffordAlgebra.spinorNorm_specialOrthogonalGroupBaseChange under the field, finite-dimensionality, nondegeneracy and invertibility-of-two hypotheses. The commuting Spin-action square is CliffordAlgebra.spinToSpecialOrthogonal_baseChange; its more general input is a finite free module over a commutative ring with two invertible.

Keep the quadratic-space hypotheses of Theorem [fcap-003N][fcap-003N]. Let \(d\in K^\times \) be nonsquare, put \(L=K(\sqrt d)\), and let \(\sigma \) be its nontrivial \(K\)-automorphism. The square-class map has kernel \[\ker j=\{1,[d]_K\}.\] Consequently, for \(g\in SO(V,Q)\), \[g_L\text { has a Spin lift} \quad \Longleftrightarrow \quad \nu _Q(g)\in \{1,[d]_K\}.\] The trivial class already gives a lift over \(K\). If \(\nu _Q(g)=[d]_K\), the two lifts over \(L\) are exchanged by \(\sigma \); neither is the scalar extension of a \(K\)-defined Spin element.

For an explicit rational example, take \(K=\mathbb Q\) and \[Q(ae+bf)=a^2+2b^2,\qquad g=-\operatorname {Id}=r_e r_f.\] Here \(e^2=1\), \(f^2=2\), and \(ef=-fe\). Thus \(x=ef\) satisfies \[\operatorname {rev}(x)x=feef=2,\qquad x^2=efef=-2,\] and \(\nu _Q(g)=[2]_{\mathbb Q}\) is nontrivial. Over \(L=\mathbb Q(\sqrt 2)\), however, \[s=\frac {ef}{\sqrt 2},\qquad N_{\mathrm {rev}}(s)=1,\qquad s^2=-1.\] Its vector action is still \(-\operatorname {Id}\). The two Spin lifts \(s,-s\) are interchanged by conjugating \(\sqrt 2\); the rational orthogonal transformation acquires lifts without either lift becoming rational.

Let \(K\) be a field in which \(2\) is invertible, let \(V\) be a \(K\)-space, and let \(Q\) be nondegenerate. Write \(B_Q\) for the unhalved polar form and \(\widehat v=\iota _Q(v)\) for a Clifford generator. Suppose \[Q(u)=0,\qquad B_Q(u,w)=0.\] The Eichler transvection and its Clifford lift are \[\begin {aligned} E_{u,w}(x) &=x+B_Q(x,u)w-B_Q(x,w)u-Q(w)B_Q(x,u)u,\\ L_{u,w}&=1+\widehat w\widehat u. \end {aligned}\] Then \(L_{u,w}\in \operatorname {Spin}(Q)\), its Spin action is \(E_{u,w}\), and \[L_{u,w}^{-1}=\operatorname {rev}(L_{u,w})=1-\widehat w\widehat u.\] The formal transformation formula already makes sense over a commutative ring and module, without nondegeneracy or invertible \(2\) QuadraticMap.transvection_apply QuadraticMap.transvection_mem_specialOrthogonalGroup. The actual Spin lift uses the field, invertible-two, and nondegeneracy hypotheses stated above CliffordAlgebra.coe_spinTransvection CliffordAlgebra.coe_spinToSpecialOrthogonal_spinTransvection.

Indeed, put \(N=\widehat w\widehat u\). The Clifford relations give \[\begin {gathered} N^2=0,\qquad \operatorname {rev}(N)=-N,\\ N\widehat x-\widehat xN =B_Q(x,u)\widehat w-B_Q(x,w)\widehat u,\\ N\widehat xN=Q(w)B_Q(x,u)\widehat u. \end {gathered}\] Thus expansion of \((1+N)\widehat x(1-N)\) gives exactly the displayed formula, including its negative quadratic term, and proves reverse norm one. Actual membership in the vector-generated carrier is a separate point. If \(Q(w)\ne 0\), the explicit factorization is \[1+\widehat w\widehat u =\widehat {\frac {w}{Q(w)}}\, \widehat {\bigl (w+Q(w)u\bigr )},\] and the two quadratic values multiply to \(1\). If \(Q(w)=0\) and \(w\notin Ku\), nondegeneracy supplies \(x\perp u\) with \(b=B_Q(w,x)\ne 0\). For \[a=x+\frac {b-Q(x)}{b}w\] one has \(Q(a)=b\), \(Q(w+a)=2b\), and \(L_{u,w}=L_{u,w+a}L_{u,-a}\), reducing to the nonisotropic case. If \(w\in Ku\), the lift is \(1\). This is the algebraic carrier argument behind the linked formal construction; it needs no finite-dimensionality.

For \(w,w'\in u^\perp \), the cross term \((\widehat w\widehat u)(\widehat {w'}\widehat u)\) vanishes. Hence \[L_{u,w+w'}=L_{u,w}L_{u,w'},\qquad L_{u,-w}=L_{u,w}^{-1},\qquad L_{u,w+cu}=L_{u,w}.\] The same equations hold after projection to the Eichler transformations. Thus the lifts form a homomorphism \[u^{\perp }/Ku\longrightarrow \operatorname {Spin}(Q)\] which commutes with the projection to \(SO(Q)\); when \(u\ne 0\), it is injective CliffordAlgebra.spinTransvection_add CliffordAlgebra.spinTransvection_add_smul CliffordAlgebra.spinToSpecialOrthogonal_comp_spinTransvectionHom CliffordAlgebra.spinTransvectionHom_injective. The domain is \(u^{\perp }/Ku\), not all of \(V/Ku\); for \(u=0\) the family is trivial. If \(V\) is additionally finite-dimensional, these transformations have trivial spinor norm, as predicted by Theorem [fcap-0023][fcap-0023] CliffordAlgebra.spinorNorm_transvection.

Chevalley treats the common totally singular case \(Q(u)=Q(w)=B_Q(u,w)=0\): his finite exponential is \(1+\widehat w\widehat u\) and his conjugation formula is the displayed action with its quadratic term zero [chevalley1954algebraic, III.1.7, pp. 73--74]. This passage does not state the arbitrary-\(Q(w)\) formula. Meinrenken's quantization of the bivector \(w\wedge u\) is \(\widehat w\widehat u\); his commutator theorem and exponential Spin comparison recover the full formula over finite-dimensional nondegenerate real or complex spaces [meinrenken2013clifford, Section 2.2.10, Theorem 2.1 and Proposition 2.12, pp. 39--40] [meinrenken2013clifford, Proposition 3.2, pp. 53--54]. Here his symmetric form is the half-polar form \(B_M=b_Q=B_Q/2\). Since \(N^2=0\), both the Clifford and vector exponentials truncate, and the written polynomial calculation fixes the normalization and extends the formula to the stated general field. No claim that every Spin element is one exponential is made.

Let \(K\) be a field in which \(2\) is invertible and take the three-dimensional quadratic space \[Q(au+bv+cz)=ab+c^2.\] Thus \(u,v\) are null, \(B_Q(u,v)=1\), \(Q(z)=1\), and \(z\) is orthogonal to their hyperbolic plane. For \(w=tz\), the preceding lift and action become \[\begin {gathered} L_t=1+t\widehat z\widehat u =\widehat z\,\widehat {(z+tu)},\\ E_t(u)=u,\qquad E_t(z)=z-2tu,\qquad E_t(v)=v+tz-t^2u. \end {gathered}\] Both factors in the displayed product have quadratic value \(1\). Hence the pair criterion puts \(L_t\) directly in the actual Spin group, including at \(t=0\) CliffordAlgebra.ι_mul_ι_mem_spinGroup_of_norm_mul_norm_eq_one. In coordinates \((a,c,b)\) the transformation is \[E_t= \begin {pmatrix} 1&-2t&-t^2\\ 0&1&t\\ 0&0&1 \end {pmatrix}.\] Substitution gives \(Q(E_t x)=Q(x)\), while multiplication gives \(E_sE_t=E_{s+t}\) and \(L_sL_t=L_{s+t}\). At \(t=1/2\), \[z\longmapsto z-u,\qquad v\longmapsto v+\frac 12z-\frac 14u,\] and composing this map with itself gives \(z\mapsto z-2u\) and \(v\mapsto v+z-u\). For \(t\ne 0\), the vector action has \((E_t-1)^2v=-2t^2u\) and \((E_t-1)^3=0\), although the Clifford increment satisfies \((L_t-1)^2=0\). Over \(\mathbb R\), this is the null frame inside the split model of Example [fcap-002I][fcap-002I]; over every stated field it is a concrete element of the spinor-norm kernel in Theorem [fcap-0023][fcap-0023].

There is also a precise radical comparison. On the degenerate real form \[Q_{\mathrm {PGA}}(ar+xe+yf)=x^2+y^2\] the line \(\mathbb Rr\) is radical. With \(u=r\) and \(w=te\), the same ring-level transvection formula gives \[\begin {gathered} L_t=1+t\widehat e\widehat r =\widehat e\,\widehat {(e+tr)},\\ E_t(r)=r,\qquad E_t(e)=e-2tr,\qquad E_t(f)=f. \end {gathered}\] The nondegenerate packaged Spin-transvection theorem does not apply here. Nevertheless this particular lift still belongs to the vector-generated Spin carrier, because both displayed factors have quadratic value \(1\); the pair criterion itself needs no nondegeneracy. The quadratic action term vanishes because \(B_Q(r,-)=0\), and now \((E_t-1)^2=0\). This retains the original degenerate Clifford algebra rather than replacing it by the radical quotient of Remark [fcap-002C][fcap-002C]. It does not identify the shear with a particular PGA point translation, motor parameter, dual encoding, or orientation convention.

On \(\mathbb R^2\), let \(Q(a,b)=a^2-b^2\), \(e_+=(1,0)\), and \(e_-=(0,1)\). The corresponding reflections are \[r_{e_+}=\operatorname {diag}(-1,1),\qquad r_{e_-}=\operatorname {diag}(1,-1),\] so \(g=r_{e_+}r_{e_-}=-I\) lies in \(SO(Q)\). Its spinor norm is \[\nu _Q(g)=[Q(e_+)Q(e_-)]=[-1]\ne [1].\] With the two norm conventions of Remark [fcap-0028][fcap-0028], the even Clifford lift \(x=\widehat e_+\widehat e_-\) has \[N_{\mathrm {rev}}(x)=N_*(x)=-1.\] For every \(c\in \mathbb R^\times \), the scalar multiple \(cx\) has norm \(-c^2\), which cannot equal \(1\). More generally, any two Lipschitz lifts of \(g\) differ by a scalar by Proposition [fcap-002D][fcap-002D], so no lift can be normalized into the norm-one Spin carrier. Equivalently, the image theorem in Theorem [fcap-0023][fcap-0023] excludes a Spin lift because \(\nu _Q(g)\) is nontrivial.

This is the mixed-sign counterpart to the successful square normalizations in Lemma [fcap-000B][fcap-000B] and Theorem [fcap-000C][fcap-000C]. Meinrenken notes that over \(\mathbb R\) one sometimes uses the weaker carrier condition \(N(x)=\pm 1\); under that different convention this \(x\) passes the norm test [meinrenken2013clifford, Remark 3.2, p. 52]. TauCeti's Spin group uses the norm-one carrier, so the two conventions must not be identified.

Let \(Q\) be a positive-dimensional finite-dimensional nondegenerate real quadratic form. Distinguish the orthogonal norm \(\nu _Q^O\) on \(O(Q)\) from its restriction \(\nu _Q\) to \(SO(Q)\). Since \(\mathbb R^{\times }/(\mathbb R^\times )^2=\{[1],[-1]\}\), their images and the Spin image are: \[\begin {array}{c|c|c|c} \text {case}&\operatorname {im}\nu _Q^O& \operatorname {im}\nu _Q&\text {Spin image}\\ \hline \text {positive definite}&\{[1]\}&\{[1]\}&SO(Q)\\ \text {negative definite}&\{[1],[-1]\}&\{[1]\}&SO(Q)\\ \text {indefinite}&\{[1],[-1]\}&\{[1],[-1]\}&\ker \nu _Q \end {array}\] For a positive form, every reflected value is a square, so the orthogonal norm is trivial CliffordAlgebra.orthogonalSpinorNorm_eq_one_of_posDef. For a negative form, the orthogonal norm is the determinant square class and is therefore trivial on \(SO(Q)\) CliffordAlgebra.orthogonalSpinorNorm_eq_orthogonalDetSquareClass_of_negDef CliffordAlgebra.spinorNorm_eq_one_of_negDef. In the indefinite case, one positive and one negative reflection give a determinant-one element of norm \([-1]\), so \(\nu _Q\) is onto CliffordAlgebra.spinorNorm_surjective_of_indefinite. Thus the final kernel has index two. The Spin-image column follows from Theorem [fcap-0023][fcap-0023]; the table does not identify this kernel with a topological component.

Rank zero is separate: \(SO(Q)\) is trivial, and the image/kernel theorem uses its subsingleton branch rather than the positive-dimensional scalar row. In rank one, \(SO(Q)\) and its spinor norm are trivial. For any nonzero \(v\), the image of \(\nu _Q^O\) is generated by \([Q(v)]\), and it is trivial exactly when \(Q(v)\) is a square CliffordAlgebra.spinorNorm_eq_one_of_finrank_le_one CliffordAlgebra.orthogonalSpinorNorm_range_eq_zpowers_of_finrank_eq_one CliffordAlgebra.orthogonalSpinorNorm_eq_one_iff_isSquare_apply_of_finrank_eq_one. An indefinite real form has rank at least two. Degenerate or semidefinite PGA forms lie outside every row of this nondegenerate table.

Let \(V\) be a finite-dimensional real vector space with \(\dim V\geq 2\), and let \(Q\) be positive definite. If \(Q(x)=Q(y)=c>0\), then some \(s\in \operatorname {Spin}(Q)\) satisfies \[\operatorname {spinVectorAction}_Q(s,x)=y.\] In particular, Spin acts transitively on the unit level \(Q(v)=1\). This is a statement about the algebraic vector action; no topology or compactness is needed.

Cartan's anisotropic-normal reflection has determinant \(-1\) [cartan1981theory, Section 9, pp. 9--10]. His even-reflection correction appears in [cartan1981theory, Section 10, p. 10]. The following two-case calculation gives the sphere orbit explicitly.

The formal surjectivity theorem uses positive \(Q\) directly: every nonzero value \(Q(v)\) has a real square root, making the spinor norm trivial on \(SO(Q)\) CliffordAlgebra.orthogonalSpinorNorm_eq_one_of_posDef. This is a separate route from the fixed-sign sufficient hypothesis in Theorem [fcap-001B][fcap-001B].

For a real quadratic space of signature \((p,q)\) with \(p+q>0\), the kernel of the Spin action is the scalar pair: \[(\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \simeq \ker \bigl (\operatorname {Spin}(p,q)\longrightarrow SO(p,q)\bigr ).\] The nontrivial residue class maps to the scalar Clifford element \(-1\). Thus the two kernel elements are precisely \(1\) and \(-1\). This is the kernel used in Gallier's real double-cover theorem.

TauCeti proves the analogous algebraic statement over a field \(K\): \(V\) is nontrivial and finite-dimensional, \(Q\) is nondegenerate, and \(2\) is invertible in \(K\). Under exactly those hypotheses it constructs the displayed canonical multiplicative equivalence. This is a generalization of the cited real result, not an attribution of arbitrary-field kernel classification to Gallier.

Let \(K\) be a characteristic-zero field, let \(V\) be nonzero and finite-dimensional, and let its bilinear form be nondegenerate. Meinrenken defines Spin as the even part of the norm-one Clifford group. Its kernel is the scalar pair. If the Spin action is surjective, these data form the group extension \[1\longrightarrow (\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \longrightarrow \operatorname {Spin}(Q)\longrightarrow SO(Q)\longrightarrow 1.\] The left map sends the nontrivial class to \(-1\); the right map is the Spin action. TauCeti packages this generic construction from an explicit surjectivity proof. The group-extension constructor used in that package is GroupExtension.ofMulEquivKer.

Meinrenken warns that the map to \(SO(V)\) need not be surjective over a general field; it is surjective when every element of \(K\) has a square root, because lifts can then be rescaled to have norm one. TauCeti separates this issue explicitly. Its generic construction assumes a field, a nontrivial finite-dimensional module, invertible \(2\), a nondegenerate quadratic form, and a supplied surjectivity proof. Over a separably closed field, Theorem [fcap-001B][fcap-001B] supplies that proof and yields the specialized extension.

For a real quadratic space of signature \((p,q)\) with \(p+q>0\), the Pin action has the same two-element kernel: \[(\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \simeq \ker \bigl (\operatorname {Pin}(p,q)\longrightarrow O(p,q)\bigr ).\] Its nontrivial generator is the image in Pin of the scalar Spin element \(-1\). The identification is obtained by comparing the Pin kernel with the Spin kernel, not by adding a second pair of central elements. Gallier's real double-cover proof uses exactly the quotient by \(\{\pm 1\}\).

TauCeti transports the Spin-kernel equivalence to Pin over a field \(K\) when the module is nontrivial and finite-dimensional, \(Q\) is nondegenerate, and \(2\) is invertible. These are the formal theorem's exact assumptions; the cited scholarly claim is the real case.

In Meinrenken's characteristic-zero, nonzero, finite-dimensional, nondegenerate setting, Pin is the kernel of the norm on the Clifford group. Its scalar kernel and any proof that the Pin action is surjective determine the group extension \[1\longrightarrow (\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \longrightarrow \operatorname {Pin}(Q)\longrightarrow O(Q)\longrightarrow 1.\] The inclusion sends the nontrivial class to the scalar \(-1\), and the projection is the Pin action. Meinrenken notes that surjectivity can fail over a general field and that square roots for all field elements suffice to normalize lifts. TauCeti's generic theorem instead assumes a field, a nontrivial finite-dimensional module, invertible \(2\), a nondegenerate quadratic form, and an explicit surjectivity proof. Its separably closed specialization obtains that proof from the formal Cartan--Dieudonne route.

Let \(R\) be a commutative ring, let \(M_1,M_2\) be \(R\)-modules with quadratic forms \(Q_1,Q_2\), and let \(f:M_1\to M_2\) be an \(R\)-linear map satisfying \[Q_2(f(m))=Q_1(m).\] The Clifford universal property gives an algebra homomorphism \(\operatorname {Cl}(f):\mathcal {C}\kern -2pt\ell (Q_1)\to \mathcal {C}\kern -2pt\ell (Q_2)\) characterized on generators by \[\operatorname {Cl}(f)(\iota _{Q_1}(m))=\iota _{Q_2}(f(m))\] CliffordAlgebra.map_apply_ι. It preserves the Spin carrier and therefore restricts to a group homomorphism \(\operatorname {Spin}(f):\operatorname {Spin}(Q_1)\to \operatorname {Spin}(Q_2)\) QuadraticMap.Isometry.spinGroupMap. Concretely, the Clifford map preserves Lipschitz membership QuadraticMap.Isometry.map_mem_lipschitzGroup, evenness CliffordAlgebra.map_mem_even, and Clifford conjugation CliffordAlgebra.map_star; these are the carrier conditions separated in Remark [fcap-0028][fcap-0028]. Neither construction requires \(f\) to have an inverse.

Now suppose that \(2\) is invertible in \(R\). If \(a_i\) denotes the Spin vector action on \(M_i\), then \[a_2\bigl (\operatorname {Spin}(f)(s),f(m)\bigr ) =f\bigl (a_1(s,m)\bigr ).\] This identity says that the square with horizontal maps \(a_1,a_2\) and vertical maps \(\operatorname {Spin}(f)\times f,f\) commutes. It is the vector-action naturality equation, with no finite-dimensionality or nondegeneracy hypothesis. If \(f\) is instead an isometry equivalence, it induces a Spin equivalence QuadraticMap.IsometryEquiv.spinGroupEquiv, and the same square packages as naturality of the Spin-to-special-orthogonal homomorphism source theorem.

A changed Gram matrix shows why the target form is part of the data. Over \(\mathbb Q\), set \(Q_1(x,y)=x^2+y^2\) and \(T(x,y)=(2x,y)\). Keeping the same form on the target does not give an isometry: at \(e_1\), \[Q_1(Te_1)=4\ne 1=Q_1(e_1).\] Correspondingly, the source generator \(\iota _{Q_1}(e_1)\) squares to \(1\), while its proposed image \(\iota _{Q_1}(2e_1)\) squares to \(4\); that assignment cannot define the claimed Clifford map.

For the transported target form \(Q_2(x,y)=x^2/4+y^2\), one has \(Q_2(Tv)=Q_1(v)\). In column coordinates, \[G_1=I,\qquad G_2=(T^{-1})^\top G_1T^{-1} =\begin {pmatrix}1/4&0\\0&1\end {pmatrix},\qquad T^\top G_2T=G_1.\] Now \(\iota _{Q_2}(2e_1)^2=Q_2(2e_1)=1\), so the generator relation is preserved. Thus an arbitrary basis scaling is not a fixed-form isometry; it becomes an isometry only after the domain and target forms are related in the correct direction. This differs from the module equivalence \(T_Q:\mathcal {C}\kern -2pt\ell (Q)\simeq \bigwedge M\) in Lemma [fcap-0004][fcap-0004][fcap-0004], which is not an algebra map.

Meinrenken derives \(\operatorname {Cl}(f)\) from the same universal property for a bilinear-form-preserving linear map [meinrenken2013clifford, Section 2.2.2, Proposition 2.2, p. 29]. Chevalley's tensor-quotient construction gives the corresponding extension from generator images whose squares are \(Q(x)\) [chevalley1954algebraic, II.1.1, pp. 38--39]. In Meinrenken's convention \(Q(v)=B(v,v)\), so his \(B\) is the half-polar form \(b_Q\) of Convention [fcap-0027][fcap-0027]. These sources work over finite-dimensional vector spaces over fields; Meinrenken assumes characteristic different from two. The formal action square above has the commutative-ring hypotheses stated here. This card makes no claim about scalar extension, orthogonal sums, or composition of extension maps.

The extensions in Theorem [fcap-001D][fcap-001D] and Theorem [fcap-001F][fcap-001F] are exact sequences of abstract groups. They record a surjective homomorphism and its two-element kernel, but no topology. For the positive real form, the actual finite-dimensional carrier topology, compact double cover, and connectedness are established in Proposition [fcap-0039][fcap-0039]; the stabilizer argument and the universal-cover boundary are established in Proposition [fcap-003A][fcap-003A]. Those results do not extend the compact connectedness conclusion to arbitrary real signature.

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

For \(n\geq 3\), the covering in Proposition [fcap-0039][fcap-0039] is the universal covering of \(SO(n)\). The proof uses the action on the unit sphere from Theorem [fcap-0024][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][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][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][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][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][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.

Expand the half-commutator and move \(\iota (x)\) past \(\iota (u)\) and \(\iota (v)\) using the Clifford relation. The cubic terms cancel; the two polar terms combine to the displayed generator. Symmetry of \(B_Q\) then makes the skew-adjointness equation cancel in pairs.

For \(x\in V\), dual-basis reconstruction and skew-adjointness give the two contractions \[\begin {aligned} \sum _i B_Q(d_i,x)f(b_i)&=f(x),\\ \sum _i B_Q(f(b_i),x)d_i&=-f(x). \end {aligned}\] By Lemma [fcap-000P][fcap-000P], the commutator of the sum of bivectors with \(\iota (x)\) is the image of their difference, hence \(2\iota (f(x))\). Multiplication by \(1/2\) gives the action of \(z_f\) on every generator. The nondegenerate quadratic realization in Theorem [fcap-000R][fcap-000R] then identifies the two quadratic elements.

The invariance of \(\kappa \) makes \(\operatorname {ad}_x\) skew-adjoint. Applying Theorem [fcap-001Z][fcap-001Z] to \(f=\operatorname {ad}_x\) first gives a factor \(1/2\) with the dual basis for \(B_{Q_\kappa }\). Since \(B_{Q_\kappa }=2\kappa \), that polar-dual basis is \(d_i=\tfrac 12 b_i^\vee \). Bilinearity of the bivector gives the second factor \(1/2\), and \((1/2)(1/2)=1/4\). The equality \(B_{Q_\kappa }=2\kappa \) is the convention encoded by TauCeti.LieAlgebra.polarBilin_killingQuadraticForm.

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.