NOTE: This site has just upgraded to Forester 5.x and is still having some style and functionality issues, we will fix them ASAP.

Compendium on Spin groups [spin-0001]
✍️source 📄PDF

1. Motivation [spin-000R]

    This survey is built on my notes in the process of figuring out Eric Wieser's MathOverflow question Definition of a spin group for our PR to Lean 4's Mathlib about Spin groups.

    This is my first Forester experiment, also a spiritual successor to my writeup The Many Faces of Geometric Algebra.

    2. Our definition [spin-000X]

      definition 2.1. Clifford algebra [pr-spin] [ca-0002]

        Let \(M\) be a module over a commutative ring \(R\), equipped with a quadratic form \(Q: M \to R\).

        A Clifford algebra over \(Q\) is \[ \mathcal {C}\kern -2pt\ell (Q) \equiv T(M)/I_Q \] where \(T(M)\) is the tensor algebra of \(M\), \(I_Q\) is the two-sided ideal generated from the set \[ \{ m \otimes m - Q(m) \mid m \in M \}. \]

        We denote the canonical linear map \(M \to \mathcal {C}\kern -2pt\ell (Q)\) as \(\iota _Q\).

        definition 2.2. Lipschitz-Clifford group [pr-spin] [spin-000W]

          The Lipschitz-Clifford group is defined as the subgroup closure of all the invertible elements in the form of \(\iota _Q(m)\), \[ \Gamma \equiv \left \{ x_1 \ldots x_k \in \mathcal {C}\kern -2pt\ell ^{\times }(Q) \mid x_i \in V \right \} \] where \[ \mathcal {C}\kern -2pt\ell ^{\times }(Q) \equiv \left \{ x \in \mathcal {C}\kern -2pt\ell (Q) \mid \exists x^{-1} \in \mathcal {C}\kern -2pt\ell (Q), x^{-1} x = x x^{-1}=1\right \} \] is the group of units (i.e. invertible elements) of \(\mathcal {C}\kern -2pt\ell (Q)\), \[ V \equiv \left \{ \iota _Q(m) \in \mathcal {C}\kern -2pt\ell (Q) \mid m \in M \right \} \] is the subset \(V\) of \(\mathcal {C}\kern -2pt\ell (Q)\) in the form of \(\iota _Q(m)\).

          definition 2.3. Pin group [pr-spin] [spin-000Y]
          pinGroup
          L∃∀N

            The Pin group is defined as \[ \operatorname {Pin}(Q) \equiv \Gamma \sqcap \operatorname {U}(\mathcal {C}\kern -2pt\ell (Q)) \] where \(\sqcap \) is the infimum (or greatest lower bound, or meet), and the infimum of two submonoids is just their intersection \(\cap \), \[ \operatorname {U}(S) \equiv \left \{ x \in S \mid x^{*} * x = x * x^{*} = 1 \right \} \] are the unitary elements of the Clifford algebra as a \(*\)-monid, and we have defined the star operation of Clifford algebra as Clifford conjugate [wieser2022formalizing], denoted \(\bar {x}\).

            This definition is equivalent to the following: \[ \operatorname {Pin}(Q) \equiv \left \{ x \in \Gamma \mid \operatorname {N}(x) = 1 \right \} \] where \[ \operatorname {N}(x) \equiv x \bar {x}. \]

            definition 2.4. Spin group [pr-spin] [spin-0012]
            spinGroup
            L∃∀N

              The Spin group is defined as \[ \operatorname {Spin}(Q) \equiv \operatorname {Pin}(Q) \sqcap \mathcal {C}\kern -2pt\ell ^{+}(Q) \] where \(\mathcal {C}\kern -2pt\ell ^{+}(Q)\) is the even subalgebra of the Clifford algebra.

              3. Appendix: Many faces of Spin group [spin-000Z]

                Definitions coming from different sources are simply quoted here with minimal modifications, to include immediate prerequisites, and omit some discussions or theorems.

                They are not classified, ordered, or pruned by similarity.

                definition 3.1. Spin group [lawson2016spin] [spin-0002]

                  Let \(V\) be a vector space over the commutative field \(k\) and suppose \(q\) is a quadratic form on \(V\).

                  We now consider the multiplicative group of units in the Clifford algebra \(C \ell (V, q)\) associated to \(V\), which is defined to be the subset \[ C \ell ^{\times }(V, q) \equiv \left \{\varphi \in C \ell (V, q): \exists \varphi ^{-1} \text { with } \varphi ^{-1} \varphi =\varphi \varphi ^{-1}=1\right \} \]

                  This group contains all elements \(v \in V\) with \(q(v) \neq 0\).

                  The group of units always acts naturally as automorphisms of the algebra. That is, there is a homomorphism \[ \mathrm {Ad}: \mathrm {C} \ell ^{\times }(V, q) \longrightarrow \operatorname {Aut}(\mathrm {C} \ell (V, q)) \] called the adjoint representation, which is given by \[ \operatorname {Ad}_{\varphi }(x) \equiv \varphi \times \varphi ^{-1} \] The Pin group of \((V, q)\) is the subgroup \(\operatorname {Pin}(V, q)\) of \(\mathrm {P}(V, q)\) generated by the elements \(v \in V\) with \(q(v)= \pm 1\). The associated Spin group of \((V, q)\) is defined by \[ \operatorname {Spin}(V, q)=\operatorname {Pin}(V, q) \cap C \ell ^0(V, q) . \]

                  definition 3.2. Spin group [wiki2024clifford] [spin-0003]

                     The pin group \(\operatorname {Pin}_V(K)\) is the subgroup of the Lipschitz group \(\Gamma \) of elements of spinor norm 1, and similarly the spin group \(\operatorname {Spin}_V(K)\) is the subgroup of elements of Dickson invariant 0 in \(\operatorname {Pin}_V(K)\).

                    definition 3.3. Spin group [li2008invariant] [spin-0004]

                      A versor refers to a Clifford monomial composed of invertible vectors. It is called a rotor, or spinor, if the number of vectors is even. It is called a unit versor if its magnitude is 1.

                      All versors in \(\mathcal {C L}\left (\mathcal {V}^n\right )\) form a group under the geometric product, called the versor group, also known as the Clifford group, or Lipschitz group. All rotors form a subgroup, called the rotor group. All unit versors form a subgroup, called the pin group, and all unit rotors form a subgroup, called the spin group, denoted by \(\operatorname {Spin}\left (\mathcal {V}^n\right )\).

                      definition 3.4. Spin group [sommer2013geometric] [spin-0005]

                         The Clifford group \(\Gamma _{\mathrm {p}, \mathrm {q}}\) of a Clifford algebra \(\mathcal {C}_{p, q}\) is defined as \[ \Gamma _{\mathrm {p}, \mathrm {q}}:=\left \{s \in \mathcal {C}_{p, q} \mid \forall x \in \mathbb {R}_{p, q}: s x \hat {s}^{-1} \in \mathbb {R}_{p, q}\right \} . \] From that definition we get immediately \[ \Gamma _{\mathrm {p}, \mathrm {q}} \times \mathbb {R}_{p, q} \rightarrow \mathbb {R}_{p, q} ; \quad (s, x) \mapsto s x \hat {s}^{-1} \] as the operation of the Clifford group \(\Gamma _{\mathrm {p}, \mathrm {q}}\) on \(\mathbb {R}_{p, q}\). \(\Gamma _{\mathrm {p}, \mathrm {q}}\) is a multiple cover of the orthogonal group \(O(p, q)\). However, it is still unnecessarily large. Therefore, we first reduce \(\Gamma _{\mathrm {p}, \mathrm {q}}\) to a two-fold cover of \(O(p, q)\) by defining the so-called Pin group \[ \operatorname {Pin}(\mathrm {p}, \mathrm {q}):=\left \{s \in \Gamma _{\mathrm {p}, \mathrm {q}} \mid s \tilde {s}= \pm 1\right \} . \] The even elements of \(\operatorname {Pin}(p, q)\) form the spin group \[ \operatorname {Spin}(\mathrm {p}, \mathrm {q}):=\operatorname {Pin}(\mathrm {p}, \mathrm {q}) \cap \mathcal {C}_{p, q}^{+} \] which is a double cover of the special orthogonal group \(S O(p, q)\). Finally, those elements of \(\operatorname {Spin}(\mathrm {p}, \mathrm {q})\) with Clifford norm equal 1 form a further subgroup \[ \operatorname {Spin}_{+}(\mathrm {p}, \mathrm {q}):=\{s \in \operatorname {Spin}(\mathrm {p}, \mathrm {q}) \mid s \tilde {s}=1\} \] that covers \(\mathrm {SO}_{+}(p, q)\) twice. Thereby, \(\mathrm {SO}_{+}(p, q)\) is the connected component of the identity of \(O(p, q)\).

                        definition 3.5. Spin group [perwass2009geometric] [spin-0006]

                          A versor is a multivector that can be expressed as the geometric product of a number of non-null 1-vectors. That is, a versor \(\boldsymbol {V}\) can be written as \(\boldsymbol {V}=\prod _{i=1}^k \boldsymbol {n}_i\), where \(\left \{\boldsymbol {n}_1, \ldots , \boldsymbol {n}_k\right \} \subset \mathbb {G}_{p, q}^{\varnothing 1}\) with \(k \in \mathbb {N}^{+}\), is a set of not necessarily linearly independent vectors.

                          The subset of versors of \(\mathbb {G}_{p, q}\) together with the geometric product, forms a group, the Clifford group, denoted by \(\mathfrak {G}_{p, q}\).

                          A versor \(\boldsymbol {V} \in \mathfrak {G}_{p, q}\) is called unitary if \(\boldsymbol {V}^{-1}=\tilde {\boldsymbol {V}}\), i.e. \(\boldsymbol {V} \widetilde {\boldsymbol {V}}=+1\).

                          The set of unitary versors of \(\mathfrak {G}_{p, q}\) forms a subgroup \(\mathfrak {P}_{p, q}\) of the Clifford group \(\mathfrak {G}_{p, q}\), called the pin group.

                          A versor \(\boldsymbol {V} \in \mathfrak {G}_{p, q}\) is called a spinor if it is unitary \((\boldsymbol {V} \tilde {\boldsymbol {V}}=1)\) and can be expressed as the geometric product of an even number of 1-vectors. This implies that a spinor is a linear combination of blades of even grade.

                          The set of spinors of \(\mathfrak {G}_{p, q}\) forms a subgroup of the pin group \(\mathfrak {P}_{p, q}\), called the spin group, which is denoted by \(\mathfrak {S}_{p, q}\).

                          definition 3.6. Spin group [jadczyk2019notes] [spin-0007]

                            We define the Clifford group \(\Gamma =\Gamma (q)\) to be the group of all invertible elements \(u \in \mathrm {Cl}(q)\) which have the property that \(uyu^{-1}\) is in \(M\) whenever \(y\) is in \(M\). We define \(\Gamma (q)^{ \pm }\)as the intersection of \(\Gamma (q)\) and \(\mathrm {Cl}(q)_{ \pm }\).

                            For every element \(u \in \Gamma (q)\) we define the spinor norm \(N(u)\) by the formula \[ N(u)=\tau (u) u, \] where \(\tau \) is the main involution of the Clifford algebra \(\mathrm {Cl}(q)\). The following groups are called spin groups: \[ \begin {aligned} & \operatorname {Pin}(q):=\left \{s \in \Gamma (q)^{+} \cup \Gamma (q)^{-}: N(s)= \pm 1\right \} \\ & \operatorname {Spin}(q):=\left \{s \in \Gamma (q)^{+}: N(s)= \pm 1\right \} \\ & \operatorname {Spin}^{+}(q):=\left \{s \in \Gamma (q)^{+}: N(s)=+1\right \} . \end {aligned} \]

                            definition 3.7. Spin group [garling2011clifford] [spin-0008]

                               Suppose that \((E, q)\) is a regular quadratic space. We consider the action of \(\mathcal {G}(E, q)\) on \(\mathcal {A}(E, q)\) by adjoint conjugation. We set \[ A d_g^{\prime }(a)=g a g^{-1}, \] for \(g \in \mathcal {G}(E, q)\) and \(a \in \mathcal {A}(E, q)\). We restrict attention to those elements of \(\mathcal {G}(E, q)\) which stabilize \(E\). The Clifford group \(\Gamma =\Gamma (E, q)\) is defined as \[ \left \{g \in \mathcal {G}(E, q): A d_g^{\prime }(x) \in E \text { for } x \in E\right \} . \] If \(g \in \Gamma (E, q)\), we set \(\alpha (g)(x)=A d_g^{\prime }(x)\). Then \(\alpha (g) \in G L(E)\), and \(\alpha \) is a homomorphism of \(\Gamma \) into \(G L(E) . \alpha \) is called the graded vector representation of \(\Gamma \). It is customary to scale the elements of \(\Gamma (E, q)\); we set \[ \begin {aligned} \operatorname {Pin}(E, q) & =\{g \in \Gamma (E, q): \Delta (g)= \pm 1\}, \\ \Gamma _1(E, q) & =\{g \in \Gamma (E, q): \Delta (g)=1\} . \end {aligned} \] If \((E, q)\) is a Euclidean space, then \(\operatorname {Pin}(E, q)=\Gamma _1(E, q)\); otherwise, \(\Gamma _1(E, q)\) is a subgroup of \(\operatorname {Pin}(E, q)\) of index 2. We have a short exact sequence \[ 1 \longrightarrow D_2 \xrightarrow {\subseteq } \operatorname {Pin}(E, q) \xrightarrow {\alpha } O(E, q) \longrightarrow 1 ; \] \(\operatorname {Pin}(E, q)\) is a double cover of \(O(E, q)\). In fact there is more interest in the subgroup \(\operatorname {Spin}(E, q)\) of \(\operatorname {Pin}(E, q)\) consisting of products of an even number of unit vectors in \(E\). Thus \(\operatorname {Spin}(E, q)=\operatorname {Pin}(E, q) \cap \mathcal {A}^{+}(E, q)\) and \[ \operatorname {Spin}(E, q)=\left \{g \in \mathcal {A}^{+}(E, q): g E=E g \text { and } \Delta (g)= \pm 1\right \} . \] If \(x, y\) are unit vectors in \(E\) then \(\alpha (x y)=\alpha (x) \alpha (y) \in S O(E, q)\), so that \(\alpha (\operatorname {Spin}(E, q)) \subseteq S O(E, q)\). Conversely, every element of \(S O(E, q)\) is the product of an even number of simple reflections, and so \(S O(E, q) \subseteq \alpha \left (\operatorname {Spin}(E, q)\right )\). Thus \(\alpha \left (\operatorname {Spin}(E, q)\right )=S O(E, q)\), and we have a short exact sequence. \[ 1 \longrightarrow D_2 \xrightarrow {\subseteq } \operatorname {Spin}(E, q) \xrightarrow {\alpha } S O(E, q) \longrightarrow 1 ; \] \(\operatorname {Spin}(E, q)\) is a double cover of \(S O(E, q)\). Note also that if \(a \in \operatorname {Spin}(E, q)\) and \(x \in E\) then \(\alpha (a)(x)=a x a^{-1}\); conjugation and adjoint conjugation by elements of \(\operatorname {Spin}(E, q)\) are the same.

                              definition 3.8. Spin group [meinrenken2009lie] [spin-0009]

                                Recall that \(\Pi : \mathrm {Cl}(V) \rightarrow \) \(\mathrm {Cl}(V), x \mapsto (-1)^{|x|} x\) denotes the parity automorphism of the Clifford algebra. Let \(\mathrm {Cl}(V)^{\times }\)be the group of invertible elements in \(\mathrm {Cl}(V)\).

                                The Clifford group \(\Gamma (V)\) is the subgroup of \(\mathrm {Cl}(V)^{\times }\), consisting of all \(x \in \mathrm {Cl}(V)^{\times }\) such that \(A_x(v):=\Pi (x) v x^{-1} \in V\) for all \(v \in V \subset \mathrm {Cl}(V)\).

                                Hence, by definition the Clifford group comes with a natural representation, \(\Gamma (V) \rightarrow \mathrm {GL}(V), x \mapsto A_x\). Let \(S \Gamma (V)=\Gamma (V) \cap \mathrm {Cl}^{\overline {0}}(V)^{\times }\)denote the special Clifford group.

                                The canonical representation of the Clifford group takes values in \(\mathrm {O}(V)\), and defines an exact sequence, \[ 1 \longrightarrow \mathbb {K}^{\times } \longrightarrow \Gamma (V) \longrightarrow \mathrm {O}(V) \longrightarrow 1 . \] It restricts to a similar exact sequence for the special Clifford group, \[ 1 \longrightarrow \mathbb {K}^{\times } \longrightarrow S \Gamma (V) \longrightarrow \mathrm {SO}(V) \longrightarrow 1 . \] The elements of \(\Gamma (V)\) are all products \(x=v_1 \cdots v_k\) where \(v_1, \ldots , v_k \in V\) are non-isotropic. \(S \Gamma (V)\) consists of similar products, with \(k\) even. The corresponding element \(A_x\) is a product of reflections: \[ A_{v_1 \cdots v_k}=R_{v_1} \cdots R_{v_k} . \]

                                Suppose \(\mathbb {K}=\mathbb {R}\). The Pin group \(\operatorname {Pin}(V)\) is the preimage of \(\{1,-1\}\) under the norm homomorphism \(N: \Gamma (V) \rightarrow \mathbb {K}^{\times }\). Its intersection with \(S \Gamma (V)\) is called the Spin group, and is denoted \(\operatorname {Spin}(V)\).

                                Since \(N(\lambda )=\lambda ^2\) for \(\lambda \in \mathbb {K}^{\times }\), the only scalars in \(\operatorname {Pin}(V)\) are \(\pm 1\). Hence, the exact sequence for the Clifford group restricts to an exact sequence, \[ 1 \longrightarrow \mathbb {Z}_2 \longrightarrow \operatorname {Pin}(V) \longrightarrow \mathrm {O}(V) \longrightarrow 1, \] so that \(\operatorname {Pin}(V)\) is a double cover of \(\mathrm {O}(V)\). Similarly, \[ 1 \longrightarrow \mathbb {Z}_2 \longrightarrow \operatorname {Spin}(V) \longrightarrow \mathrm {SO}(V) \longrightarrow 1, \] defines a double cover of \(\mathrm {SO}(V)\). Elements in \(\operatorname {Pin}(V)\) are products \(x=\) \(v_1 \cdots v_k\) with \(B\left (v_i, v_i\right )= \pm 1\). The group \(\operatorname {Spin}(V)\) consists of similar products, with \(k\) even.

                                definition 3.9. Spin group [weber2013lie] [spin-000A]

                                  The "group of units" in \(C l_{p, q}\), denoted \(C l_{p, q}^{\times }\), is the group of all invertible elements.

                                  An important subgroup of \(C l^{\times }(V, q)\) is the group \(P(V, q)\) generated by elements \(v \in V\) with \(q(v) \neq 0\). Quotienting out by constants, we obtain the Pin group. Specifically, \(\operatorname {Pin}(V, q)\) (or \(\operatorname {Pin}_{p, q}\) ) is the group generated by elements \(v \in V\) with \(q(v)= \pm 1\). Further define the spin groups to be \[ \operatorname {Spin}(V, q)=\operatorname {Pin}(V, q) \cap C l^0(V, q) . \]

                                  definition 3.10. Spin group [bar2011spin] [spin-000B]

                                     We define the Pin \(\operatorname {group} \operatorname {Pin}(\boldsymbol {n})\) by \[ \operatorname {Pin}(n):=\left \{v_1 \cdot \ldots \cdot v_m \in \mathrm {Cl}_n \mid v_j \in S^{n-1} \subset \mathbb {R}^n, m \in \mathbb {N}_0\right \} \] We define the Spin group \(\operatorname {Spin}(\boldsymbol {n})\) by \[ \begin {aligned} \operatorname {Spin}(n) & :=\operatorname {Pin}(n) \cap \mathrm {Cl}_n^0 \\ & =\left \{v_1 \cdot \ldots \cdot v_m \in \mathrm {Cl}_n \mid v_j \in S^{n-1}, m \in 2 \mathbb {N}_0\right \} \end {aligned} \]

                                    definition 3.11. Spin group [woit2012lie] [spin-000C]

                                    • April 29, 2024

                                    There are several equivalent possible ways to go about defining the \(\operatorname {Spin}(n)\) groups as groups of invertible elements in the Clifford algebra.

                                    1. One can define \(\operatorname {Spin}(n)\) in terms of invertible elements \(\tilde {g}\) of \(C_{\text {even }}(n)\) that leave the space \(V=\mathbf {R}^n\) invariant under conjugation \[ \tilde {g} V \tilde {g}^{-1} \subset V \] 2. One can show that, for \(v, w \in V\), \[ v \rightarrow v-2 \frac {Q(v, w)}{Q(w, w)} w=-w v w / Q(w, w)=w v w^{-1} \] is reflection in the hyperplane perpendicular to \(w\). Then \(\operatorname {Pin}(n)\) is defined as the group generated by such reflections with \(||w||^2=1\) . \(\operatorname {Spin}(n)\) is the subgroup of \(\operatorname {Pin}(n)\) of even elements. Any rotation can be implemented as an even number of reflections (Cartan-Dieudonné) theorem.

                                    3. One can define the Lie algebra of \(\operatorname {Spin}(n)\) in terms of quadratic elements of the Clifford algebra.

                                    definition 3.12. Spin group [liu2016lie] [spin-000D]

                                       The space of quadratic vectors in \(\mathrm {Cl}\) is the Lie algebra of \(\mathrm {SO}(n)\). The corresponding Lie group, called the Spin group \(\operatorname {Spin}(Q)\), is the set of invertible elements \(x \in \mathrm {Cl}\) that preserve \(V\) under \(v \mapsto x v x^{-1}\). Clearly this map is in \(\mathrm {SO}(V, Q)\) since it preserves the quadratic form \(Q\), and is a two-fold cover with kernel \(\pm 1\).

                                      definition 3.13. Spin group [figueroa2010spin] [spin-000E]

                                        The Pin group Pin \((V)\) of \((V, Q)\) is the subgroup of (the group of units of) \(C \ell (V)\) generated by \(v \in \mathrm {V}\) with \(\mathrm {Q}(v)= \pm 1\). In other words, every element of \(\operatorname {Pin}(\mathrm {V})\) is of the form \(u_1 \cdots u_r\) where \(u_i \in \mathrm {V}\) and \(\mathrm {Q}\left (u_i\right )= \pm 1\). We will write \(\operatorname {Pin}(s, t)\) for \(\operatorname {Pin}\left (\mathbb {R}^{s, t}\right )\) and \(\operatorname {Pin}(n)\) for \(\operatorname {Pin}(n, 0)\).

                                        The spin group of \((V, Q)\) is the intersection \[ \operatorname {Spin}(V)=\operatorname {Pin}(V) \cap C \ell (V)_0 . \] Equivalently, it consists of elements \(u_1 \cdots u_{2 p}\), where \(u_i \in \mathrm {V}\) and \(\mathrm {Q}\left (u_i\right )= \pm 1\). We will write \(\operatorname {Spin}(s, t)\) for \(\operatorname {Spin}\left (\mathbb {R}^{s, t}\right )\) and \(\operatorname {Spin}(n)\) for \(\operatorname {Spin}(n, 0)\).

                                        definition 3.14. Spin group [lundholm2009clifford] [spin-000F]

                                           We identify the following groups embedded in \(\mathcal {G}\) : \[ \begin {aligned} \mathcal {G}^{\times } &:=\{x \in \mathcal {G}: \exists y \in \mathcal {G}: x y=y x=1\} & \text { the group of all invertible elements } \\ \tilde {\Gamma } &:=\left \{x \in \mathcal {G}^{\times }: x^{\star } V x^{-1} \subseteq V\right \} & \text { the Lipschitz group } \\ \Gamma &:=\left \{v_1 v_2 \ldots v_k \in \mathcal {G}: v_i \in V^{\times }\right \} & \text { the versor group } \\ \text { Pin } &:=\left \{x \in \Gamma : x x^{\dagger } \in \{-1,1\}\right \} & \text { the group of unit versors } \\ \text { Spin } &:=\operatorname {Pin} \cap \mathcal {G}^{+} & \text { the group of even unit versors } \\ \operatorname {Spin}^{+} &:=\left \{x \in \operatorname {Spin}: x x^{\dagger }=1\right \} & \text { the rotor group } \\ \end {aligned} \] In the above, \(V^{\times }:=\left \{v \in V: v^2 \neq 0\right \}\) denotes the set of all invertible vectors.

                                          definition 3.15. Spin group [renaud2020clifford] [spin-000G]

                                            The Clifford group \(\Gamma (p, q)\) is the (multiplicative) group generated by invertible 1-vectors in \(R^{p, q}\).

                                            The Pin group \(\operatorname {Pin}(p, q)\). \[ \operatorname {Pin}(p, q)=\{g \in \Gamma (p, q): g \widetilde {g}= \pm 1\} . \] So if \(g \in \operatorname {Pin}(p, q), \widetilde {g}\) is a scalar multiple of \(g^{-1}\). This is not true for arbitrary elements of \(\Gamma (p, q)\). The Spin group \(\operatorname {Spin}(p, q)\). This is the subgroup of \(\operatorname {Pin}(p, q)\) consisting of even elements only, i.e. \[ \operatorname {Spin}(p, q)=\operatorname {Pin}(p, q) \cap C l^{+}(p, q) . \] The \(\operatorname {Spin}\) group \(\operatorname {Spin}(p, q)\) has the further subgroup \[ \operatorname {Spin}^{\dagger }(p, q)=\{g \in \operatorname {Spin}(p, q): g \widetilde {g}=+1\} . \] \(\operatorname {Pin}(p, q)\), \(\operatorname {Spin}(p, q)\) and \(\operatorname {Spin}^{\dagger }(p, q)\) are respectively the two-fold covering groups of \(O(p, q), S O(p, q)\) and \(S O^{\dagger }(p, q)\) (where \(S O^{\dagger }(p, q)\) is the connected component of \(S O(p, q)\) ).

                                            definition 3.16. Spin group [dutailly2018clifford] [spin-000H]

                                              The Spin group \(\operatorname {Spin}(F, \rho )\) of \(C l(F, \rho )\) is the subset of \(C l(F, \rho )\) whose elements can be written as the product \(g=u_1 \cdot \ldots \cdot u_{2 p}\) of an even number of vectors of \(F\) of norm \(\left \langle u_k, u_k\right \rangle =1\).

                                              As a consequence : \(\langle g, g\rangle =1, g^t \cdot g=1\) and \(\operatorname {Spin}(F, \rho ) \subset O(C l)\).

                                              The scalars \(\pm 1\) belong to the Spin group. The identity is \(+1 . \operatorname {Spin}(F, \rho )\) is a connected Lie group.

                                              definition 3.17. Spin group [hitzer2012introduction] [spin-000I]

                                                A versor refers to a Clifford monomial (product expression) composed of invertible vectors. It is called a rotor, or spinor, if the number of vectors is even. It is called a unit versor if its magnitude is 1.

                                                Every versor \(A=a_1 \ldots a_r, \quad a_1, \ldots , a_r \in \mathbb {R}^2, r \in \mathbb {N}\) has an inverse \[ A^{-1}=a_r^{-1} \ldots a_1^{-1}=a_r \ldots a_1 /\left (a_1^2 \ldots a_r^2\right ), \] such that \[ A A^{-1}=A^{-1} A=1 . \]

                                                This makes the set of all versors in \(C l(2,0)\) a group, the so called Lipschitz group with symbol \(\Gamma (2,0)\), also called Clifford group or versor group. Versor transformations apply via outermorphisms to all elements of a Clifford algebra. It is the group of all reflections and rotations of \(\mathbb {R}^2\).

                                                The normalized subgroup of versors is called pin group \[ \operatorname {Pin}(2,0)=\{A \in \Gamma (2,0) \mid A \widetilde {A}= \pm 1\} . \] In the case of \(C l(2,0)\) we have \[ \begin {aligned} & \operatorname {Pin}(2,0) \\ & =\left \{a \in \mathbb {R}^2 \mid a^2=1\right \} \cup \left \{A \mid A=\cos \varphi +e_{12} \sin \varphi , \varphi \in \mathbb {R}\right \} . \end {aligned} \] The pin group has an even subgroup, called spin group \[ \operatorname {Spin}(2,0)=\operatorname {Pin}(2,0) \cap C l^{+}(2,0) . \] The spin group has in general a spin plus subgroup \[\operatorname {Spin}_{+}(2,0)=\{A \in \operatorname {Spin}(2,0) \mid A \widetilde {A}=+1\}.\]

                                                definition 3.18. Spin group [hahn2004clifford] [spin-000J]

                                                  We continue to let \(F\) be a field of characteristic not 2 and \(M\) a quadratic space over \(F\).

                                                  Recall that \(\gamma : M \rightarrow C(M)\) is injective and that there is a unique involution - on \(C(M)\) taking \(\gamma x\) to \(\gamma x\) for all \(x\). Consider \(M\) to be a subset of \(C(M)\) via \(\gamma \), and define the group \(\operatorname {Spin}(M)\) by \[ \operatorname {Spin}(M)=\left \{c \in C_0(M)^{\times } \mid c M c^{-1}=M, c \bar {c}=1_C\right \}, \] where \(C_0(M)^{\times }\)is the group of invertible elements of the \(\operatorname {ring} C_0(M)\). The isometries from \(M\) onto \(M\) constitute the orthogonal group \(O(M)\) and \(S O(M)\) is the subgroup of elements of determinant 1. For \(c\) in \(\operatorname {Spin}(M)\), define \[ \pi c: M \rightarrow M \] by \(\pi c(x)=c x c^{-1}\). This provides a homomorphism \[ \pi : \operatorname {Spin}(M) \rightarrow S O(M) . \] By a theorem of Cartan and Dieudonné, any element \(\sigma \) in \(O(M)\) is a product \(\sigma =\tau _{y_1} \cdots \tau _{y_k}\) of hyperplane reflections \(\tau _{y_i}\). The assignment \(\Theta (\sigma )=\) \(q\left (y_1\right ) \cdots q\left (y_k\right )\left (F^{\times }\right )^2\) defines the spinor norm homomorphism \[ \Theta : S O(M) \rightarrow F^{\times } /\left (F^{\times }\right )^2 . \]

                                                  definition 3.19. Spin group [porteous1995clifford] [spin-000K]

                                                     Let \(g\) be an invertible element of a universal Clifford algebra \(A\) such that, for each \(x \in X, g x \widehat {g}^{-1} \in X\). Then the map \[ \rho _{X, g}: x \mapsto g x \widehat {g}^{-1} \] is an orthogonal automorphism of \(X\).

                                                    The element \(g\) will be said to induce or represent the orthogonal transformation \(\rho _{X, g}\) and the set of all such elements \(g\) will be denoted by \(\Gamma (X)\) or simply by \(\Gamma \).

                                                    The subset \(\Gamma \) is a subgroup of \(A\).

                                                    The group \(\Gamma \) is called the Clifford group (or Lipschitz group) for \(X\) in the Clifford algebra \(A\). Since the universal algebra \(A\) is uniquely defined up to isomorphism, \(\Gamma \) is also uniquely defined up to isomorphism.

                                                    An element \(g\) of \(\Gamma (X)\) represents a rotation of \(X\) if and only if \(g\) is the product of an even number of elements of \(X\). The set of such elements will be denoted by \(\Gamma ^0=\Gamma ^0(X)\). An element \(g\) of \(\Gamma \) represents an anti-rotation of \(X\) if and only if \(g\) is the product of an odd number of elements of \(X\). The set of such elements will be denoted by \(\Gamma ^1=\Gamma ^1(X)\). Clearly, \(\Gamma ^0=\Gamma \cap A^0\) is a subgroup of \(\Gamma \), while \(\Gamma ^1=\Gamma \cap A^1\).

                                                    The Clifford group \(\Gamma (X)\) of a quadratic space \(X\) is larger than is necessary if our interest is in representing orthogonal transformations of \(X\). Use of a quadratic norm \(N\) on the Clifford algebra \(A\) leads to the definition of subgroups of \(\Gamma \) that are less redundant for this purpose. This quadratic norm \(N: A \rightarrow A\) is defined by the formula \[ N(a)=a^{-} a, \text { for any } a \in A, \] For \(X\) and \(\Gamma =\Gamma (X)\) as above we now define \[ \operatorname {Pin} X=\{g \in \Gamma :|N(g)|=1\} \text { and } \operatorname {Spin} X=\left \{g \in \Gamma ^0:|N(g)|=1\right \} \text {. } \]

                                                    definition 3.20. Spin group [rosen2019geometric] [spin-000L]

                                                      Let \(V\) be an inner product space. We denote by \(\Delta V\) the standard Clifford algebra \((\wedge V,+, \Delta )\) defined by the Clifford product \(\Delta \) on the space of multivectors in \(V\).

                                                      Let \(V\) be an inner product space. The Clifford cone of \(V\) is the multiplicative group \(\widehat {\triangle } V \subset \triangle V\) generated by nonsingular vectors, that is, vectors \(v\) such that \(\langle v\rangle ^2 \neq 0\). More precisely, \(q \in \widehat {\triangle } V\) if there are finitely many nonsingular vectors \(v_1, \ldots , v_k \in V\) such that \[ q=v_1 \Delta \cdots \Delta v_k . \]

                                                      Let \(w \in \triangle V\). Then \(w \in \widehat {\triangle } V\) if and only if \(w\) is invertible and \(\widehat {w} v w^{-1} \in V\) for all \(v \in V\).

                                                      In this case \(w\) can be written as a product of at most \(\operatorname {dim} V\) nonsingular vectors, and \(\bar {w} w=w \bar {w} \in \mathbf {R} \backslash \{0\}\).

                                                      Let \(V\) be an inner product space. Define the orthogonal, special orthogonal, pin, and spin groups \[ \begin {aligned} \mathrm {O}(V) & :=\{\text { isometries } T: V \rightarrow V\} \subset \mathcal {L}(V), \\ \mathrm {SO}(V) & :=\{T \in \mathrm {O}(V) ; \operatorname {det} T=+1\} \subset \mathcal {L}(V), \\ \operatorname {Pin}(V) & :=\left \{q \in \widehat {\triangle } V ;\langle q\rangle ^2= \pm 1\right \} \subset \triangle V, \\ \operatorname {Spin}(V) & :=\left \{q \in \operatorname {Pin}(V) ; q \in \triangle ^{\mathrm {ev}} V\right \} \subset \triangle ^{\mathrm {ev}} V . \end {aligned} \] We call \(T \in \operatorname {SO}(V)\) a rotation and we call \(q \in \operatorname {Spin}(V)\) a rotor.

                                                      definition 3.21. Spin group [ruhe2024clifford] [spin-000M]

                                                         Motivation E. 39 (The problem of generalizing the definition of the Spin group). For a positive definite quadratic form \(\mathfrak {q}\) on the real vector space \(V=\mathbb {R}^n\) with \(n \geq 3\) the \(\operatorname {Spin}\) group \(\operatorname {Spin}(n)\) is defined via the kernel of the Spinor norm (=extended quadratic form on \(\mathrm {Cl}(V, \mathfrak {q})\) ) restricted to the special Clifford group \(\Gamma ^{[0]}(V, \mathfrak {q})\) : \[ \operatorname {Spin}(n):=\operatorname {ker}\left (\overline {\mathfrak {q}}: \Gamma ^{[0]}(V, \mathfrak {q}) \rightarrow \mathbb {R}^{\times }\right )=\left \{w \in \Gamma ^{[0]}(V, \mathfrak {q}) \mid \overline {\mathfrak {q}}(w)=1\right \}=\left .\overline {\mathfrak {q}}\right |_{\Gamma ^{[0]}(V, \mathfrak {q})} ^{-1}(1) . \] \(\operatorname {Spin}(n)\) is thus a normal subgroup of the special Clifford group \(\Gamma ^{[0]}(V, \mathfrak {q})\), and, as it turns out, a double cover of the special orthogonal group \(\mathrm {SO}(n)\) via the twisted conjugation \(\rho \). The latter can be summarized by the short exact sequence: \[ 1 \longrightarrow \{ \pm 1\} \xrightarrow {\text { incl }} \operatorname {Spin}(n) \xrightarrow {\rho } \mathrm {SO}(n) \longrightarrow 1 . \]

                                                        We intend to generalize this in several directions: 1. from Spin to Pin group, 2. from \(\mathbb {R}^n\) to vector spaces \(V\) over general fields \(\mathbb {F}\) with \(\operatorname {ch}(\mathbb {F}) \neq 2\), 3. from non-degenerate to degenerate quadratic forms \(\mathfrak {q}\), 4. from positive (semi-)definite to non-definite quadratic forms \(\mathfrak {q}\). This comes with several challenges and ambiguities.

                                                        Definition E. 40 (The real Pin group and the real Spin group). Let \(V\) be a finite dimensional \(\mathbb {R}\)-vector space \(V, \operatorname {dim} V=n<\infty \), and \(\mathfrak {q} a\) (possibly degenerate) quadratic form on \(V\). We define the (real) Pin group and (real) Spin group, resp., of \((V, \mathfrak {q})\) as the following subquotients of the Clifford group. \(\Gamma (V, \mathfrak {q})\) and its even parity part \(\Gamma ^{[0]}(V, \mathfrak {q})\), resp.: \[ \begin {aligned} \operatorname {Pin}(V, \mathfrak {q}) & :=\{x \in \Gamma (V, \mathfrak {q}) \mid \overline {\mathfrak {q}}(x) \in \{ \pm 1\}\} / \bigwedge ^{[*]}(\mathcal {R}) \\ \operatorname {Spin}_{\infty }(V, \mathfrak {q}) & :=\left \{x \in \Gamma ^{[0]}(V, \mathfrak {q}) \mid \overline {\mathfrak {q}}(x) \in \{ \pm 1\}\right \} / \bigwedge ^{[*]}(\mathcal {R}) \end {aligned} \] Corollary E.41. Let \((V, \mathfrak {q})\) be a finite dimensional quadratic vector space over \(\mathbb {R}\). Then the twisted conjugation induces a well-defined and surjective group homomorphism onto the group of radical preserving orthogonal automorphisms of \((V, \mathfrak {q})\) : \[ \rho : \operatorname {Pin}(V, \mathfrak {q}) \rightarrow \mathrm {O}_{\mathcal {R}}(V, \mathfrak {q}), \] with kernel: \[ \operatorname {ker}\left (\rho : \underset {\sim \text { in }}{\operatorname {Pin}}(V, \mathfrak {q}) \rightarrow \mathrm {O}_{\mathcal {R}}(V, \mathfrak {q})\right )=\{ \pm 1\} . \] Correspondingly, for the \(\operatorname {Spin}(V, \mathfrak {q})\) group. In short, we have short exact sequences: \[ \begin {aligned} & 1 \longrightarrow \{ \pm 1\} \xrightarrow {\text { incl }} \operatorname {Pin}(V, \mathfrak {q}) \xrightarrow {\rho } \mathrm {O}_{\mathcal {R}}(V, \mathfrak {q}) \longrightarrow 1, \\ & 1 \longrightarrow \{ \pm 1\} \xrightarrow {\text { incl }} \operatorname {Spin}(V, \mathfrak {q}) \xrightarrow {\rho } \operatorname {SO}_{\mathcal {R}}(V, \mathfrak {q}) \longrightarrow 1 . \end {aligned} \]

                                                        definition 3.22. Spin group [gallier2014clifford] [spin-000N]

                                                           Every Clifford algebra \(\mathrm {Cl}(\Phi )\) possesses a canonical anti-automorphism \(t: \mathrm {Cl}(\Phi ) \rightarrow \mathrm {Cl}(\Phi )\) satisfying the properties \[ t(x y)=t(y) t(x), \quad t \circ t=\mathrm {id}, \quad \text { and } \quad t(i(v))=i(v), \] for all \(x, y \in \mathrm {Cl}(\Phi )\) and all \(v \in V\). Furthermore, such an anti-automorphism is unique. Every Clifford algebra \(\mathrm {Cl}(\Phi )\) has a unique canonical automorphism \(\alpha : \mathrm {Cl}(\Phi ) \rightarrow \mathrm {Cl}(\Phi )\) satisfying the properties \[ \alpha \circ \alpha =\mathrm {id}, \quad \text { and } \quad \alpha (i(v))=-i(v), \] for all \(v \in V\). First, we define conjugation on a Clifford algebra \(\mathrm {Cl}(\Phi )\) as the map \[ x \mapsto \bar {x}=t(\alpha (x)) \text { for all } x \in \mathrm {Cl}(\Phi ) . \] Given a finite dimensional vector space \(V\) and a quadratic form \(\Phi \) on \(V\), the Clifford group of \(\Phi \) is the group \[ \Gamma (\Phi )=\left \{x \in \mathrm {Cl}(\Phi )^* \mid \alpha (x) v x^{-1} \in V \quad \text { for all } v \in V\right \} . \] The map \(N: \mathrm {Cl}(Q) \rightarrow \mathrm {Cl}(Q)\) given by \[ N(x)=x \bar {x} \] is called the norm of \(\mathrm {Cl}(\Phi )\).

                                                          We also define the group \(\Gamma ^{+}(\Phi )\), called the special Clifford group, by \[ \Gamma ^{+}(\Phi )=\Gamma (\Phi ) \cap \mathrm {Cl}^0(\Phi ) . \]

                                                          We define the pinor group \(\operatorname {Pin}(p, q)\) as the group \[ \operatorname {Pin}(p, q)=\left \{x \in \Gamma _{p, q} \mid N(x)= \pm 1\right \}, \] and the spinor group \(\operatorname {Spin}(p, q)\) as \(\operatorname {Pin}(p, q) \cap \Gamma _{p, q}^{+}\).

                                                          The restriction of \(\rho : \Gamma _{p, q} \rightarrow \mathbf {G L}(n)\) to the pinor group \(\operatorname {Pin}(p, q)\) is a surjective homomorphism \(\rho : \mathbf {P i n}(p, q) \rightarrow \mathbf {O}(p, q)\) whose kernel is \(\{-1,1\}\), and the restriction of \(\rho \) to the spinor group \(\mathbf {S p i n}(p, q)\) is a surjective homomorphism \(\rho : \mathbf {S p i n}(p, q) \rightarrow \mathbf {S O}(p, q)\) whose kernel is \(\{-1,1\}\).

                                                          Remark: According to Atiyah, Bott and Shapiro, the use of the name \(\operatorname {Pin}(k)\) is a joke due to Jean-Pierre Serre (Atiyah, Bott and Shapiro Clifford modules, page 1).

                                                          definition 3.23. Spin group [fulton2013representation] [spin-000O]

                                                             Instead of defining the spin group as the set of products of certain elements of \(V\), it will be convenient to start with a more abstract definition. Set \[ \operatorname {Spin}(Q)=\left \{x \in C(Q)^{\text {even }}: x \cdot x^*=1 \text { and } x \cdot V \cdot x^* \subset V\right \} \text {. } \] We see from this definition that \(\operatorname {Spin}(Q)\) forms a closed subgroup of the group of units in the (even) Clifford algebra. Any \(x\) in \(\operatorname {Spin}(Q)\) determines an endomorphism \(\rho (x)\) of \(V\) by \[ \rho (x)(v)=x \cdot v \cdot x^*, \quad v \in V . \] Define a larger subgroup, this time of the multiplicative group of \(C(Q)\), by \[ \operatorname {Pin}(Q)=\left \{x \in C(Q): x \cdot x^*=1 \text { and } x \cdot V \cdot x^* \subset V\right \}, \] and define a homomorphism \[ \rho : \operatorname {Pin}(Q) \rightarrow \mathrm {O}(Q), \quad \rho (x)(v)=\alpha (x) \cdot v \cdot x^*, \] where \(\alpha : C(O) \rightarrow C(O)\) is the main involution.

                                                            definition 3.24. Spin group [wiki2023spin] [spin-000P]

                                                              The pin group \(\operatorname {Pin}(V)\) is a subgroup of \(\mathrm {Cl}(V)\) 's Clifford group of all elements of the form \[ v_1 v_2 \cdots v_k \] where each \(v_i \in V\) is of unit length: \(q\left (v_i\right )=1\).

                                                              The spin group is then defined as \[ \operatorname {Spin}(V)=\operatorname {Pin}(V) \cap \mathrm {Cl}^{\text {even }}, \] where \(\mathrm {Cl}^{\text {even }}=\mathrm {Cl}^0 \oplus \mathrm {Cl}^2 \oplus \mathrm {Cl}^4 \oplus \cdots \) is the subspace generated by elements that are the product of an even number of vectors. That is, \(\operatorname {Spin}(V)\) consists of all elements of \(\operatorname {Pin}(V)\), given above, with the restriction to \(k\) being an even number. The restriction to the even subspace is key to the formation of two-component (Weyl) spinors, constructed below.

                                                              definition 3.25. Spin group [nlab2023spin] [spin-000Q]

                                                                The Pin group \(\operatorname {Pin}(V ; q)\) of a quadratic vector space, is the subgroup of the group of units in the Clifford algebra \(\mathrm {Cl}(V, q)\) \[ \operatorname {Pin}(V, q) \hookrightarrow \operatorname {GL}_1(\mathrm {Cl}(V, q)) \] on those elements which are multiples \(v_1 \cdots v_n\) of elements \(v_i \in V\) with \(q\left (v_i\right )=1\).

                                                                The Spin group \(\operatorname {Spin}(V, q)\) is the further subgroup of \(\operatorname {Pin}(V ; q)\) on those elements which are even number multiples \(v_1 \cdots v_{2 k}\) of elements \(v_i \in V\) with \(q\left (v_i\right )=1\).

                                                                definition 3.26. Spin group [dereli2010degenerate] [spin-000T]

                                                                   The group \(\operatorname {Spin}(p, q)\) is defined by \[ \operatorname {Spin}(p, q)=\left \{v_1 \ldots v_m \in \mathcal {C} \ell _{p, q} \mid m \in 2 \mathbb {Z}^{+}, v_i=\sum _{j=1}^{p+q} a_{i j} e_j,\left \langle v_i, v_i\right \rangle =\mp 1,1 \leq i \leq m\right \} \]

                                                                  definition 3.27. Degenerate Spin group [dereli2010degenerate] [spin-000U]

                                                                     The subset of \(\mathcal {C} \ell _{p, q, r}\) defined by \[ S_{p, q, r}=\left \{s \gamma _1 \ldots \gamma _{p+q}(1+G) \mid s \in \operatorname {Spin}(p, q), \gamma _i=1+e_i \sum _{l=1}^r c_{i l} f_l, G \in \Lambda (f)\right \} \] is a group under the Clifford multiplication where \(\left \langle \cdot , \cdot \right \rangle \) is a symmetric bilinear form on \(\mathbb {R}^{p+q+r}\), \(\left \{e_1, \ldots , e_p, e_{p+1}, \ldots , e_{p+q}, f_1, \ldots , f_r\right \}\) is the algebra basis for the degenerate Clifford algebra \(\mathcal {C} \ell _{p, q, r}=\mathcal {C} \ell \left (\mathbb {R}^n,\langle \rangle \right )\), \(1 \leq i \leq p+q, c_{i l} \in \mathbb {R}\), and \(\Lambda (f)\) is defined by \[ \Lambda (f)=\operatorname {Span}\left \{f_{k_1} \ldots f_{k_j} \mid 1 \leq k_1<k_2<\ldots <k_j \leq r\right \} . \]

                                                                    Backlinks

                                                                      Notes on Clifford Algebras [ca-0001]
                                                                      📄PDF
                                                                      Readers may also check out Compendium on Spin groups.

                                                                      Preliminaries [ca-000N]

                                                                        This section introduces the algebraic environment of Clifford Algebra, covering vector spaces, groups, algebras, representations, modules, multilinear algebras, quadratic forms, filtrations and graded algebras.

                                                                        The material in this section should be familiar to the readers, but it is worth reading through it to become familiar with the notation and terminology that is used, as well as their counterparts in Lean, which usually require some additional treatment, both mathematically and technically (probably applicable to other formal proof verification systems).

                                                                        Details can be found in the references in corresponding section, or you may use the L∃∀N button to check the corresponding \(\textsf {Mathlib}\) document and Lean 4 source code.

                                                                        In this section, we follow [jadczyk2019notes], with supplements from [garling2011clifford][chen2016infinitely], and extensive modifications to match the counterparts in Lean's \(\textsf {Mathlib}\).

                                                                        basics: from groups to modules [ca-000P]

                                                                          [ca-000O]

                                                                            \card{convention}{definition style}{

                                                                            In this document, we unify the informal mathematical language for a definition to:

                                                                            \optional{Let \placeholder{\(X\)} be a \placeholder{\vocab{concept \(X\)}}. }

                                                                            A \newvocab{\placeholder{concept \(Z\)}} is a set/pair/triple/tuple \((Z, \mathtt {op}, ...)\), satisfying:

                                                                            1. \placeholder{\(Z\)} is a \placeholder{\vocab{concept \(Y\)}} \optional{ over \placeholder{\(X\)} under \placeholder{op} }.
                                                                            2. \placeholder{formula} for all \placeholder{elements in \(Z\)} \optional{(\vocab{ \placeholder{property} })}.
                                                                            3. \optional{for each \placeholder{element} in \placeholder{\vocab{concept \(X\)}}, } there exists \placeholder{element} such that \placeholder{formula} for all \placeholder{elements in concept \(Z\)}.
                                                                            4. \optional{\placeholder{op} is called \placeholder{\vocab{op name}}, }for all \placeholder{elements in \(Z\)}, we have
                                                                              1. \placeholder{formula}
                                                                              2. \placeholder{formula}
                                                                              \optional{(\vocab{ \placeholder{property} })}.

                                                                            By default, \placeholder{\(X\)} is a set, \placeholder{op} is a binary operation on \placeholder{\(X\)}.

                                                                            }

                                                                            definition. group [garling2011clifford, 1.1] [ca-000Q]
                                                                            GroupAddGroup
                                                                            L∃∀N

                                                                              A group is a pair \((G, *)\), satisfying:

                                                                              1. \((a * b) * c = a * (b * c)\) for all \(a, b, c \in G\) (associativity).
                                                                              2. there exists \(1 \in G\) such that \[1 * a = a * 1 = a\] for all \(a \in G\).
                                                                              3. for each \(a \in G\), there exists \(a^{-1} \in G\) such that \[a * a^{-1} = a^{-1} * a = 1\].

                                                                              remark.  [ca-000R]

                                                                                It then follows that \(1\), the identity element, is unique, and that for each \(g \in G\) the inverse \(g^{-1}\) is unique. A group G is abelian, or commutative, if \(g * h = h * g\) for all \(g, h \in G\).

                                                                                notation. product [ca-000S]

                                                                                  In literatures, the binary operation of a group is usually called a product. It's denoted by juxtaposition \(g h\), and is understood to be a mapping \((g, h) \mapsto g * h\) from \(G \times G\) to \(G\).

                                                                                  Here we use an explicit symbol for the operation. It can be denoted multiplicatively as \(*\) in Group or additively as \(+\) in AddGroup, where the identity element will be denoted by \(1\) or \(0\), respectively.

                                                                                  Sometimes we use notations with subscripts (e.g. \(*_G\), \(1_G\)) to indicate where they are.

                                                                                  \(\textsf {Mathlib}\) encodes the mapping \(G \times G \to G\) as \(G \to G \to G\), it is understood to be \(G \to (G \to G)\), that sends \(g \in G\) to a mapping that sends \(h \in G\) to \(g * h \in G\).

                                                                                  Furthermore, a mathematical construct, e.g. a group, is represented by a "type", as Lean has a dependent type theory foundation, see [carneiro2019type] and [ullrich2023extensible, sec. 3.2].

                                                                                  definition. monoid [ca-000T]
                                                                                  MonoidAddMonoid
                                                                                  L∃∀N

                                                                                    A monoid is a pair \((R, *)\), satisfying:

                                                                                    1. \((a * b) * c = a * (b * c)\) for all \(a, b, c \in R\) (associativity).
                                                                                    2. there exists an element \(1 \in R\) such that \(1 * a = a * 1 = a\) for all \(a \in R\)
                                                                                      3. i.e. \(1\) is the multiplicative identity (neutral element).

                                                                                    definition. ring [jadczyk2019notes, 1.1] [ca-000U]
                                                                                    RingCommRingCommSemiring
                                                                                    L∃∀N

                                                                                      A ring is a triple \((R, +, *)\), satisfying:

                                                                                      1. \(R\) is a commutative group under \(+\).
                                                                                      2. \(R\) is a monoid under \(*\).
                                                                                      3. for all \(a, b, c \in R\), we have
                                                                                        1. \(a * (b + c) = a * b + a * c\)
                                                                                        2. \((a + b) * c = a * c + b * c\)
                                                                                        (left and right distributivity over \(+\)).

                                                                                      remark.  [ca-000V]

                                                                                        In applications to Clifford algebras \(R\) will be always assumed to be commutative.

                                                                                        definition. division ring [ca-000W]
                                                                                        DivisionRing
                                                                                        L∃∀N

                                                                                          A division ring is a ring \((R, +, *)\), satisfying:

                                                                                          1. \(R\) contains at least 2 elements.
                                                                                          2. for all \(a \neq 0\) in \(R\), there exists a multiplicative inverse \(a^{-1} \in R\) such that
                                                                                            3. \[ a * a^{-1} = a^{-1} * a = 1 \]

                                                                                          definition. module [jadczyk2019notes, 1.3] [ca-000X]
                                                                                          Module
                                                                                          L∃∀N

                                                                                            Let \(R\) be a commutative ring. A module over \(R\), called an \(R\)-module, is a pair \((M, \bullet )\), satisfying:

                                                                                            1. M is a group under \(+\).
                                                                                            2. \(\bullet : R \to M \to M\) is called scalar multiplication, for every \(a, b \in R\), \(x, y \in M\), we have
                                                                                              1. \(a \bullet (x + y) = a \bullet x + b \bullet y\)
                                                                                              2. \((a + b) \bullet x = a \bullet x + b \bullet x\)
                                                                                              3. \(a * (b \bullet x)=(a * b) \bullet x\)
                                                                                              4. \(1_R \bullet x = x\)

                                                                                            remark.  [ca-000Y]

                                                                                              The notation of scalar multiplication is generalized as heterogeneous scalar multiplication HMul in \(\textsf {Mathlib}\): \[ \bullet : \alpha \to \beta \to \gamma \] where \(\alpha \), \(\beta \), \(\gamma \) are different types.

                                                                                              definition. vector space [jadczyk2019notes, 1.5] [ca-000Z]
                                                                                              Module
                                                                                              L∃∀N

                                                                                                If \(R\) is a division ring, then a module \(M\) over \(R\) is called a vector space.

                                                                                                remark.  [ca-0010]

                                                                                                  For generality, \(\textsf {Mathlib}\) uses Module throughout for vector spaces, particularly, for a vector space \(V\), it's usually declared as

                                                                                                  /-- Let $K$ be a division ring, a module $V$ over $K$ is a vector space where being a module requires $V$ to be a commutative group over $+$. -/ variable [DivisionRing K] [AddCommGroup V] [Module K V]

                                                                                                  For definitions/theorems about it, and most of them can be found under Mathlib.LinearAlgebra e.g. LinearIndependent.

                                                                                                  definition. submodule [ca-0011]

                                                                                                    A submodule \(N\) of \(M\) is a module \(N\) such that every element of \(N\) is also an element of \(M\). If \(M\) is a vector space then \(N\) is called a subspace.

                                                                                                    definition. dual module [ca-0012]
                                                                                                    Module.Dual
                                                                                                    L∃∀N

                                                                                                      The dual module \(M^* : M \to _{l[R]} R\) is the \(R\)-module of all linear maps from \(M\) to \(R\).

                                                                                                      algebras [ca-0013]

                                                                                                        definition. ring homomorphism [chen2016infinitely, 4.5.1] [ca-0014]
                                                                                                        RingHomRingHomClassalgebraMap
                                                                                                        L∃∀N

                                                                                                          Let \((\alpha , +_\alpha , *_\alpha )\) and \((\beta , +_\beta , *_\beta )\) be rings. A ring homomorphism from \(\alpha \) to \(\beta \) is a map \(\mathit {1} : \alpha \to _{+*} \beta \) such that

                                                                                                          1. \(\mathit {1}(x +_{\alpha } y) = \mathit {1}(x) +_{\beta } \mathit {1}(y)\) for each \(x,y \in \alpha \).
                                                                                                          2. \(\mathit {1}(x *_{\alpha } y) = \mathit {1}(x) *_{\beta } \mathit {1}(y)\) for each \(x,y \in \alpha \).
                                                                                                          3. \(\mathit {1}(1_{\alpha }) = 1_{\beta }\).

                                                                                                          definition. isomorphism, endomorphism, automorphism [ca-0015]

                                                                                                            Isomorphism \(A \cong B\) is a bijective homomorphism \(\phi : A \to B\) (it follows that \(\phi ^{-1} : B \to A\) is also a homomorphism).

                                                                                                            Endomorphism is a homomorphism from an object to itself, denoted \(\operatorname {End}(A)\).

                                                                                                            Automorphism is an endomorphism which is also an isomorphism, denoted \(\operatorname {Aut}(A)\).

                                                                                                            definition. algebra [ca-0016]
                                                                                                            Algebra
                                                                                                            L∃∀N

                                                                                                              Let \(R\) be a commutative ring. An algebra \(A\) over \(R\) is a pair \((A, \bullet )\), satisfying:

                                                                                                              1. \(A\) is a ring under \(*\).
                                                                                                              2. there exists a ring homomorphism from \(R\) to \(A\), denoted \(\mathit {1} : R \to _{+*} A\).
                                                                                                              3. \(\bullet : R \to M \to M\) is a scalar multiplication
                                                                                                              4. for every \(r \in R\), \(x \in A\), we have
                                                                                                                1. \(r * x = x * r\) (commutativity between \(R\) and \(A\))
                                                                                                                2. \(r \bullet x = r * x\) (definition of scalar multiplication)
                                                                                                                where we omitted that the ring homomorphism \(\mathit {1}\) is applied to \(r\) before each multiplication.

                                                                                                              notation.  [ca-0017]

                                                                                                                Following literatures, for \(r \in R\), usually we write \(\mathit {1}_A(r) : R \to _{+*} A\) as a product \(r \mathit {1}_A\) if not omitted, while they are written as a call to algebraMap _ _ r in \(\textsf {Mathlib}\), which is defined to be Algebra.toRingHom r.

                                                                                                                remark.  [ca-0018]

                                                                                                                  The definition above (adopted in \(\textsf {Mathlib}\)) is more general than the definition in literature (e.g. [jadczyk2019notes, 1.6]):

                                                                                                                  Let \(R\) be a commutative ring. An algebra \(A\) over \(R\) is a pair \((M, *)\), satisfying:

                                                                                                                  1. \(A\) is a module \(M\) over \(R\) under \(+\) and \(\bullet \).
                                                                                                                  2. \(A\) is a ring under \(*\).
                                                                                                                  3. For \(x, y \in A, a \in R\), we have
                                                                                                                    4. \[ a \bullet (x * y) = (a \bullet x) * y = x * (a \bullet y) \]

                                                                                                                  See Implementation notes in Algebra for details.

                                                                                                                  remark.  [ca-0019]

                                                                                                                    What's simply called algebra is actually associative algebra with identity, a.k.a. associative unital algebra. See the red herring principle for more about such phenomenon for naming, particularly the example of (possibly) nonassociative algebra.

                                                                                                                    definition. algebra homomorphism [ca-001A]
                                                                                                                    AlgHom
                                                                                                                    L∃∀N

                                                                                                                      Let \(A\) and \(B\) be \(R\)-algebras. \(\mathit {1}_A\) and \(\mathit {1}_B\) are ring homomorphisms from \(R\) to \(A\) and \(B\), respectively. A algebra homomorphism from \(A\) to \(B\) is a map \(f : \alpha \to _{a} \beta \) such that

                                                                                                                      1. \(f\) is a ring homomorphism
                                                                                                                      2. \(f(\mathit {1}_{A}(r)) = \mathit {1}_{B}(r)\) for each \(r \in R\)

                                                                                                                      definition. ring quotient [ca-001B]
                                                                                                                      RingQuot
                                                                                                                      L∃∀N

                                                                                                                        Let \(R\) be a non-commutative ring, \(r\) an arbitrary equivalence relation on \(R\). The ring quotient of \(R\) by \(r\) is the quotient of \(R\) by the strengthen equivalence relation of \(r\) such that for all \(a, b, c\) in \(R\):

                                                                                                                        1. \(a + c \sim b + c\) if \(a \sim b\)
                                                                                                                        2. \(a * c \sim b * c\) if \(a \sim b\)
                                                                                                                        3. \(a * b \sim a * c\) if \(b \sim c\)
                                                                                                                        i.e. the equivalence relation is compatible with the ring operations \(+\) and \(*\).

                                                                                                                        remark.  [ca-001C]

                                                                                                                          As ideals haven't been formalized for the non-commutative case, \(\textsf {Mathlib}\) uses RingQuot in places where the quotient of non-commutative rings by ideal is needed. The universal properties of the quotient are proven, and should be used instead of the definition that is subject to change.

                                                                                                                          definition. free algebra [ca-001D]
                                                                                                                          FreeAlgebra FreeAlgebra.Pre FreeAlgebra.Rel
                                                                                                                          L∃∀N

                                                                                                                            Let \(X\) be an arbitrary set. An free \(R\)-algebra on \(X\) (or "generated by \(X\)"), named \(A\), is the ring quotient of the following inductively constructed set \(A_{\mathtt {pre}}\)

                                                                                                                            1. for all \(x\) in \(X\), there exists a map \(X \to A_{\mathtt {pre}}\).
                                                                                                                            2. for all \(r\) in \(R\), there exists a map \(R \to A_{\mathtt {pre}}\).
                                                                                                                            3. for all \(a, b\) in \(A_{\mathtt {pre}}\), \(a + b\) is in \(A_{\mathtt {pre}}\).
                                                                                                                            4. for all \(a, b\) in \(A_{\mathtt {pre}}\), \(a * b\) is in \(A_{\mathtt {pre}}\).
                                                                                                                            by that equivalence relation that makes \(A\) an \(R\)-algebra, namely:
                                                                                                                            1. there exists a ring homomorphism from \(R\) to \(A_{\mathtt {pre}}\), denoted \(R \to _{+*} A_{\mathtt {pre}}\).
                                                                                                                            2. \(A\) is a commutative group under \(+\).
                                                                                                                            3. \(A\) is a monoid under \(*\).
                                                                                                                            4. left and right distributivity under \(*\) over \(+\).
                                                                                                                            5. \(0 * a \sim a * 0 \sim 0\).
                                                                                                                            6. for all \(a, b, c\) in \(A\), if \(a \sim b\), we have
                                                                                                                              1. \(a + c \sim b + c\)
                                                                                                                              2. \(c + a \sim c + b\)
                                                                                                                              3. \(a * c \sim b * c\)
                                                                                                                              4. \(c * a \sim c * b\)
                                                                                                                              (compatibility with the ring operations \(+\) and \(*\))

                                                                                                                            remark.  [ca-001E]

                                                                                                                              Similar to remark [ca-0019], what we defined here is the free (associative, unital) \(R\)-algebra on \(X\), it can be denoted \(R\langle X \rangle \), expressing that it's freely generated by \(R\) and \(X\), where \(X\) is the set of generators.

                                                                                                                              definition. linear map [ca-001F]
                                                                                                                              LinearMap
                                                                                                                              L∃∀N

                                                                                                                                Let \(R, S\) be rings, \(M\) an \(R\)-module, \(N\) an \(S\)-module. A linear map from \(M\) to \(N\) is a function \(f : M \to _{l} N\) over a ring homomorphism \(\sigma : R \to _{+*} S\), satisfying:

                                                                                                                                1. \(f(x + y) = f(x) + f(y)\) for all \(x, y \in M\).
                                                                                                                                2. \(f(r \bullet x) = \sigma (r) \bullet f(x)\) for all \(r \in R\), \(x \in M\).

                                                                                                                                remark. Lin [ca-001G]

                                                                                                                                  The set of all linear maps from \(M\) to \(M'\) is denoted \(\operatorname {Lin}(M, M')\), and \(\operatorname {Lin}(M)\) for mapping from \(M\) to itself. \(\operatorname {Lin}(M)\) is an endomorphism.

                                                                                                                                  definition. tensor algebra [ca-001H]
                                                                                                                                  TensorAlgebra
                                                                                                                                  L∃∀N

                                                                                                                                    Let \(A\) be a free \(R\)-algebra generated by module \(M\), let \(\iota : M \to A\) denote the map from \(M\) to \(A\). An tensor algebra over \(M\) (or "of \(M\)") \(T\) is the ring quotient of the free \(R\)-algebra generated by \(M\), by the equivalence relation satisfying:

                                                                                                                                    1. for all \(a, b\) in \(M\), \(\iota (a + b) \sim \iota (a) + \iota (b)\).
                                                                                                                                    2. for all \(r\) in \(R\), \(a\) in \(M\), \(\iota (r \bullet a) \sim r * \iota (a)\).
                                                                                                                                    i.e. making the inclusion of \(M\) into an \(R\)-linear map.

                                                                                                                                    remark.  [ca-001I]

                                                                                                                                      The definition above is equivalent to the following definition in literature (e.g. [jadczyk2019notes, 1.7]):

                                                                                                                                      Let \(M\) be a module over \(R\). An algebra \(T\) is called a tensor algebra over \(M\) (or "of \(M\)") if it satisfies the following universal properties:

                                                                                                                                      1. \(T\) is an algebra containing \(M\) as a submodule, and it is generated by \(M\),
                                                                                                                                      2. Every linear mapping \(\lambda \) of \(M\) into an algebra \(A\) over \(R\), can be extended to
                                                                                                                                        3. a homomorphism \(\theta \) of \(T\) into \(A\).

                                                                                                                                      Forms [ca-000L]

                                                                                                                                        definition. Bilinear form [ca-0003]
                                                                                                                                        BilinForm
                                                                                                                                        L∃∀N

                                                                                                                                          Let \(R\) be a ring, \(M\) an \(R\)-module.

                                                                                                                                          An bilinear form \(B\) over \(M\) is a map \(B : M \to M \to R\), satisfying:

                                                                                                                                          1. \( B(x + y, z) = B(x, z) +B(y, z) \)
                                                                                                                                          2. \( B(x, y + z) = B(x, y) +B(x, z) \)
                                                                                                                                          3. \( B(a \bullet x, y) = a * B(x, y)\)
                                                                                                                                          4. \( B(x, a \bullet y) = a * B(x, y)\)
                                                                                                                                          for all \(a \in R, x, y, z \in M\).

                                                                                                                                          definition. quadratic form [jadczyk2019notes, 1.9] [ca-0004]
                                                                                                                                          QuadraticFormQuadraticForm.polar
                                                                                                                                          L∃∀N

                                                                                                                                            Let \(R\) be a commutative ring, \(M\) a \(R\)-module.

                                                                                                                                            An quadratic form \(Q\) over \(M\) is a map \(Q : M \to R\), satisfying:

                                                                                                                                            1. \( Q(a \bullet x) = a * a * Q(x)\) for all \(a \in R, x \in M\).
                                                                                                                                            2. there exists a companion bilinear form \(B : M \to M \to R\), such that \(Q(x + y) = Q(x) + Q(y) + B(x, y)\)

                                                                                                                                            In [jadczyk2019notes], the bilinear form is denoted \(\Phi \), and called the polar form associated with the quadratic form \(Q\), or simply the polar form of \(Q\).

                                                                                                                                            remark.  [ca-0005]

                                                                                                                                              This notion generalizes to commutative semirings using the approach in [izhakian2016supertropical].

                                                                                                                                              Clifford Algebra [ca-000M]

                                                                                                                                                Here we provide a detailed account of the formalization of Clifford Algebra [hestenes2012clifford] in the Lean 4 theorem prover and programming language [moura2021lean][moura2015lean][ullrich2023extensible] and using its Mathematical Library \(\textsf {Mathlib}\) [mathlib2020lean].

                                                                                                                                                The primary references of the formalization are [wieser2022formalizing] and [wieser2024formalizing]. This section and the previous section are adapted from our [wieser2024blueprint].

                                                                                                                                                Notes on Clifford Algebras › Definition [ca-000F]

                                                                                                                                                  definition. Clifford algebra [wieser2022formalizing] [ca-0006]
                                                                                                                                                  CliffordAlgebraTensorAlgebra.toClifford
                                                                                                                                                  L∃∀N

                                                                                                                                                    Let \(M\) be a module over a commutative ring \(R\), equipped with a quadratic form \(Q: M \to R\).

                                                                                                                                                    Let \(\iota : M \to _{l[R]} T(M)\) be the canonical \(R\)-linear map for the tensor algebra \(T(M)\).

                                                                                                                                                    Let \(\mathit {1} : R \to _{+*} T(M)\) be the canonical map from \(R\) to \(T(M)\), as a ring homomorphism.

                                                                                                                                                    A Clifford algebra over \(Q\), denoted \(\mathcal {C}\kern -2pt\ell (Q)\), is the ring quotient of the tensor algebra \(T(M)\) by the equivalence relation satisfying \(\iota (m)^2 \sim \mathit {1}(Q(m))\) for all \(m \in M\).

                                                                                                                                                    The natural quotient map is denoted \(\pi : T(M) \to \mathcal {C}\kern -2pt\ell (Q)\) in some literatures, or \(\pi _\Phi \)/\(\pi _Q\) to emphasize the bilinear form \(\Phi \) or the quadratic form \(Q\), respectively.

                                                                                                                                                    remark.  [ca-0007]

                                                                                                                                                      In literatures, \(M\) is often written \(V\), and the quotient is taken by the two-sided ideal \(I_Q\) generated from the set \(\{ v \otimes v - Q(v) \vert v \in V \}\). See also Clifford algebra [pr-spin].

                                                                                                                                                      As of writing, \(\textsf {Mathlib}\) does not have direct support for two-sided ideals, but it does support the equivalent operation of taking the ring quotient by a suitable closure of a relation like \(v \otimes v \sim Q(v)\).

                                                                                                                                                      Hence the definition above.

                                                                                                                                                      remark.  [ca-0008]

                                                                                                                                                        This definition and what follows in \(\textsf {Mathlib}\) is initially presented in [wieser2022formalizing], some further developments are based on [grinberg2016clifford], and in turn based on [bourbaki2007algebra] which is in French and never translated to English.

                                                                                                                                                        The most informative English reference on [bourbaki2007algebra] is [jadczyk2019notes], which has an updated exposition in [jadczyk2023bundle].

                                                                                                                                                        example. Clifford algebra over a vector space [ca-0009]

                                                                                                                                                          Let \(V\) be a vector space \(\mathbb R^n\) over \(\mathbb R\), equipped with a quadratic form \(Q\).

                                                                                                                                                          Since \(\mathbb R\) is a commutative ring and \(V\) is a module, the definition above applies.

                                                                                                                                                          definition. Clifford map [wieser2022formalizing] [ca-000A]
                                                                                                                                                          CliffordAlgebra.ι
                                                                                                                                                          L∃∀N

                                                                                                                                                            We denote the canonical \(R\)-linear map to the Clifford algebra \(\mathcal {C}\kern -2pt\ell (M)\) by \(\iota : M \to _{l[R]} \mathcal {C}\kern -2pt\ell (M)\).

                                                                                                                                                            It's denoted \(i_\Phi \) or just \(i\) in some literatures.

                                                                                                                                                            definition. Clifford lift [wieser2022formalizing] [ca-000B]
                                                                                                                                                            CliffordAlgebra.lift
                                                                                                                                                            L∃∀N

                                                                                                                                                              Given a linear map \(f : M \to _{l[R]} A\) into an \(R\)-algebra \(A\), satisfying \(f(m)^2 = Q(m)\) for all \(m \in M\), called is Clifford, the canonical lift of \(f\) is defined to be a algebra homomorphism from \(\mathcal {C}\kern -2pt\ell (Q)\) to \(A\), denoted \(\operatorname {lift} f : \mathcal {C}\kern -2pt\ell (Q) \to _{a} A\).

                                                                                                                                                              theorem. Universal property [wieser2022formalizing] [ca-000C]
                                                                                                                                                              CliffordAlgebra.ι_comp_liftCliffordAlgebra.lift_unique
                                                                                                                                                              L∃∀N

                                                                                                                                                                Given \(f : M \to _{l[R]} A\), which is Clifford, \(F = \operatorname {lift} f\) (denoted \(\bar {f}\) in some literatures), we have:

                                                                                                                                                                1. \(F \circ \iota = f\), i.e. the following diagram commutes:

                                                                                                                                                                2. \(\operatorname {lift}\) is unique, i.e. given \(G : \mathcal {C}\kern -2pt\ell (Q) \to _{a} A\), we have: \[ G \circ \iota = f \iff G = \operatorname {lift} f\]

                                                                                                                                                                remark.  [ca-000D]

                                                                                                                                                                  The universal property of the Clifford algebras is now proven, and should be used instead of the definition that is subject to change.

                                                                                                                                                                  definition. Exterior algebra [wieser2022formalizing] [ca-000E]
                                                                                                                                                                  ExteriorAlgebra
                                                                                                                                                                  L∃∀N

                                                                                                                                                                    An Exterior algebra over \(M\) is the Clifford algebra \(\mathcal {C}\kern -2pt\ell (Q)\) where \(Q(m) = 0\) for all \(m \in M\).

                                                                                                                                                                    Notes on Clifford Algebras › Operations [ca-000G]

                                                                                                                                                                      convention.  [wieser2022formalizing] [ca-000H]

                                                                                                                                                                        Same as the previous section, let \(M\) be a module over a commutative ring \(R\), equipped with a quadratic form \(Q: M \to R\).

                                                                                                                                                                        We also use \(m\) or \(m_1, m_2, \dots \) to denote elements of \(M\), i.e. vectors, and \(x, y, z\) to denote elements of \(\mathcal {C}\kern -2pt\ell (Q)\).

                                                                                                                                                                        definition. Grade involution [wieser2022formalizing] [ca-000I]
                                                                                                                                                                        CliffordAlgebra.involute
                                                                                                                                                                        L∃∀N

                                                                                                                                                                          Grade involution, intuitively, is negating each basis vector.

                                                                                                                                                                          Formally, it's an algebra homomorphism \(\alpha : \mathcal {C}\kern -2pt\ell (Q) \to _{a} \mathcal {C}\kern -2pt\ell (Q)\), satisfying:

                                                                                                                                                                          1. \(\alpha \circ \alpha = \operatorname {id}\)
                                                                                                                                                                          2. \(\alpha (\iota (m)) = - \iota (m)\)

                                                                                                                                                                          for all \(m \in M\).

                                                                                                                                                                          That is, the following diagram commutes:

                                                                                                                                                                          It's called main involution \(\alpha \) or main automorphism in [jadczyk2019notes], the canonical automorphism in [gallier2008clifford].

                                                                                                                                                                          It's denoted \(\hat {m}\) in [lounesto2001clifford], \(\alpha (m)\) in [jadczyk2019notes], \(m^*\) in [chisolm2012geometric].

                                                                                                                                                                          definition. Grade reversion [wieser2022formalizing] [ca-000J]
                                                                                                                                                                          CliffordAlgebra.reverse
                                                                                                                                                                          L∃∀N

                                                                                                                                                                            Grade reversion, intuitively, is reversing the multiplication order of basis vectors. Formally, it's an algebra homomorphism \(\tau : \mathcal {C}\kern -2pt\ell (Q) \to _{a} \mathcal {C}\kern -2pt\ell (Q)^{\mathtt {op}}\), satisfying:

                                                                                                                                                                            1. \(\tau (m_1 m_2) = \tau (m_2) \tau (m_1)\)
                                                                                                                                                                            2. \(\tau \circ \tau = \operatorname {id}\)
                                                                                                                                                                            3. \(\tau (\iota (m)) = \iota (m)\)

                                                                                                                                                                            That is, the following diagram commutes:

                                                                                                                                                                            It's called anti-involution \(\tau \) in [jadczyk2019notes], the canonical anti-automorphism in [gallier2008clifford], also called transpose/transposition in some literature, following tensor algebra or matrix.

                                                                                                                                                                            It's denoted \(\tilde {m}\) in [lounesto2001clifford], \(m^\tau \) in [jadczyk2019notes] (with variants like \(m^t\) or \(m^\top \) in other literatures), \(m^\dagger \) in [chisolm2012geometric].

                                                                                                                                                                            definition. Clifford conjugate [wieser2022formalizing] [ca-000K]
                                                                                                                                                                            CliffordAlgebra.reverse
                                                                                                                                                                            L∃∀N

                                                                                                                                                                              Clifford conjugate is an algebra homomorphism \({*} : \mathcal {C}\kern -2pt\ell (Q) \to _{a} \mathcal {C}\kern -2pt\ell (Q)\), denoted \(x^{*}\) (or even \(x^\dagger \), \(x^v\) in some literatures), defined to be: \[ x^{*} = \operatorname {reverse}(\operatorname {involute}(x)) = \tau (\alpha (x)) \] for all \(x \in \mathcal {C}\kern -2pt\ell (Q)\), satisfying (as a \(*\)-ring):

                                                                                                                                                                              1. \((x + y)^{*} = (x)^{*} + (y)^{*}\)
                                                                                                                                                                              2. \((x y)^{*} = (y)^{*} (x)^{*}\)
                                                                                                                                                                              3. \({*} \circ {*} = \operatorname {id}\)
                                                                                                                                                                              4. \(1^{*} = 1\)
                                                                                                                                                                              and (as a \(*\)-algebra): \[ (r x)^{*} = r' x^{*} \] for all \(r \in R\), \(x, y \in \mathcal {C}\kern -2pt\ell (Q)\) where \('\) is the involution of the commutative \(*\)-ring \(R\).

                                                                                                                                                                              Note: In our current formalization in \(\textsf {Mathlib}\), the application of the involution on \(r\) is ignored, as there appears to be nothing in the literature that advocates doing this.

                                                                                                                                                                              Clifford conjugate is denoted \(\bar {m}\) in [lounesto2001clifford] and most literatures, \(m^\ddagger \) in [chisolm2012geometric].

                                                                                                                                                                              Learning diary › Year 2024 › January to August, 2024 › 2024-04-25 [2024-04-25]

                                                                                                                                                                                 
                                                                                                                                                                                The readings during this period are reflected in Compendium on Spin groups. Some are yet to be reflected in Notes on Hopf Algebras.