Proposition. Complex Spin in dimension four is two copies of \(SL_2\) [fcap-0032]
✍️source

    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] 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] 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], while the Lorentzian real form \(SL_2(\mathbb C)\) is Example [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.