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

Notes on Clifford Algebras › 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].

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