Definition [ca-000F]
✍️source

    Definition 1. 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 2.  [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 3.  [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 4. 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 5. 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 6. 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 7. 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 8.  [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 9. 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\).

                      References

                        Reference. On the bundle of clifford algebras over the space of quadratic forms [jadczyk2023bundle]

                        • 2023
                        • Arkadiusz Jadczyk
                        @article{jadczyk2023bundle,
 title = {On the bundle of Clifford algebras over the space of
quadratic forms},
 author = {Jadczyk, Arkadiusz},
 year = {2023},
 journal = {Advances in Applied Clifford Algebras},
 volume = {33},
 number = {2},
 pages = {15},
 publisher = {Springer}
}

                        Reference. Formalizing geometric algebra in lean [wieser2022formalizing]

                        • 2022
                        • Eric Wieser, Utensil Song
                        @article{wieser2022formalizing,
 title = {Formalizing geometric algebra in lean},
 author = {Wieser, Eric and Song, Utensil},
 year = {2022},
 journal = {Advances in Applied Clifford Algebras},
 volume = {32},
 number = {3},
 pages = {28},
 publisher = {Springer}
}

                        Reference. Notes on clifford algebras [jadczyk2019notes]

                        • 2019
                        • Arkadiusz Jadczyk
                        @article{jadczyk2019notes,
 title = {Notes on Clifford Algebras},
 author = {Jadczyk, Arkadiusz},
 year = {2019}
}

                        Reference. The clifford algebra and the chevalley map - a computational approach [grinberg2016clifford]

                        @misc{grinberg2016clifford,
 title = {The Clifford algebra and the Chevalley map - a
computational approach},
 author = {Grinberg, Darij},
 year = {2016},
 url = {https://www.cip.ifi.lmu.de/~grinberg/algebra/chevalley.pdf}
}

                        Reference. Éléments de mathématique. Algèbre. Chapitre 9 [bourbaki2007algebra]

                        • 2007
                        • Nicolas Bourbaki
                        @book{bourbaki2007algebra,
 title = {{\'E}l{\'e}ments de math{\'e}matique. {Alg{\`e}bre}.
{Chapitre} 9},
 author = {Bourbaki, Nicolas},
 year = {2007},
 isbn = {3-540-35338-0},
 edition = {Reprint of the 1959 original},
 publisher = {Berlin: Springer},
 language = {French}
}

                        Context

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

                            Definition [ca-000F]
                            ✍️source

                              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\).

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