Operations [ca-000G]
✍️source

    Convention 1.  [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 2. 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 3. 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 4. 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].

            References

              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. Geometric algebra [chisolm2012geometric]

              @article{chisolm2012geometric,
 title = {Geometric Algebra},
 author = {Chisolm, Eric},
 year = {2012},
 url = {http://arxiv.org/abs/1205.5935},
 journaltitle = {arXiv preprint arXiv:1205.5935}
}

              Reference. Clifford algebras, clifford groups, and a generalization of the quaternions [gallier2008clifford]

              • 2008
              • Jean Gallier
              @article{gallier2008clifford,
 title = {Clifford algebras, clifford groups, and a generalization
of the quaternions},
 author = {Gallier, Jean},
 year = {2008},
 journal = {arXiv preprint arXiv:0805.0311}
}

              Reference. Clifford algebras and spinors [lounesto2001clifford]

              • 2001
              • Pertti Lounesto
              @book{lounesto2001clifford,
 title = {Clifford Algebras and Spinors},
 author = {Lounesto, Pertti},
 year = {2001},
 volume = {286},
 publisher = {{Cambridge university press}}
}

              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]

                    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]
                                      ✍️source

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