Proposition. The real algebra generated by the Dirac gamma matrices [fcap-002U]
Proposition. The real algebra generated by the Dirac gamma matrices [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]. This is equality of the displayed forms, rather than only
equality of their signatures. Thus the Clifford transport of
Proposition [fcap-0029] and the classification in Example [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.