The Blueprint For Formalizing Geometric Algebra in Lean: Operations

Definition 2.2.1 Grade involution

✓

#

Grade involution, intuitively, is negating each basis vector.

Formally, it’s an algebra homomorphism $\alpha : \mathop{\mathcal{C}\ell }(Q) \to _{a}\mathop{\mathcal{C}\ell }(Q)$, satisfying:

$\alpha \circ \alpha = \operatorname {id}$
$\alpha (\iota (m)) = - \iota (m)$

for all $m \in M$.

It’s called main involution $\alpha $ or main automorphism in [ Jadczyk(2019) ] , the canonical automorphism in [ Gallier(2008) ] .

It’s denoted $\hat{m}$ in [ Lounesto(2001) ] , $\alpha (m)$ in [ Jadczyk(2019) ] , $m^*$ in [ Chisolm(2012) ] .

$\begin{tikzcd} [column sep=huge, row sep=huge] \Cl(Q) \arrow[r, "\alpha"] & \Cl(Q) \\ V \arrow[ru, "-\iota"] \arrow[u, "\iota"] \end{tikzcd}$

Definition 2.2.2 Grade reversion

✓

#

Grade reversion, intuitively, is reversing the multiplication order of basis vectors.

Formally, it’s an algebra homomorphism $\tau : \mathop{\mathcal{C}\ell }(Q) \to _{a}\mathop{\mathcal{C}\ell }(Q)^{\mathtt{op}}$, satisfying:

$\tau (m_1 m_2) = \tau (m_2) \tau (m_1)$
$\tau \circ \tau = \operatorname {id}$
$\tau (\iota (m)) = \iota (m)$

It’s called anti-involution $\tau $ in [ Jadczyk(2019) ] , the canonical anti-automorphism in [ Gallier(2008) ] , also called transpose/ transposition in some literature, following tensor algebra or matrix.

It’s denoted $\tilde{m}$ in [ Lounesto(2001) ] , $m^\tau $ in [ Jadczyk(2019) ] (with variants like $m^t$ or $m^\top $ in other literatures), $m^\dagger $ in [ Chisolm(2012) ] .

$\begin{tikzcd} [column sep=huge, row sep=huge] \Cl(Q) \arrow[r, "\tau"] & \Cl(Q)^{\mathtt{op}} \\ V \arrow[ru, "\iota"] \arrow[u, "\iota"] \end{tikzcd}$

Definition 2.2.3 Clifford conjugate

✓

#

Clifford conjugate is an algebra homomorphism ${*} : \mathop{\mathcal{C}\ell }(Q) \to _{a}\mathop{\mathcal{C}\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 \mathop{\mathcal{C}\ell }(Q)$, satisfying (as a $*$-ring):

$(x + y)^{*} = (x)^{*} + (y)^{*}$
$(x y)^{*} = (y)^{*} (x)^{*}$
${*} \circ {*} = \operatorname {id}$
$1^{*} = 1$

and (as a $*$-algebra):

\[ (r x)^{*} = r' x^{*} \]

for all $r \in R$, $x, y \in \mathop{\mathcal{C}\ell }(Q)$ where $'$ is the involution of the commutative $*$-ring $R$.

Note: In our current formalization in 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 [ Lounesto(2001) ] and most literatures, $m^\ddagger $ in [ Chisolm(2012) ] .

Definition 2.2.4 $Z_2$-graded derivations $i_f$, anti-derivation

#

We denote by $\operatorname {End}(M)$ the algebra of all endomorphisms (linear maps) of $M$.

For $m \in M$, the linear operator $e_{m} \in \operatorname {End}(\mathrm{T}(M))$, $\mathrm{T}^{p}(M) \rightarrow \mathrm{T}^{p+1}(M)$ is of left multiplication by $m$ :

\[ e_{m}: x \mapsto e_{m}(x) = m \otimes x \]

for all $x \in \mathrm{T}(M)$.

Let $f$ be an element of the dual module $M^{*}$.

The anti-derivation $i_{f} : T(M) \to _{l[T]}(M)$ is a linear map from $T(M)$ to $T(M)$, satisfying:

$i_{f}(1) = 0$
$e_{m} \circ i_{f} + i_{f} \circ e_{m} = f(m) \cdot 1$ for all $m \in M$

The map $f \mapsto i_{f}$ from $M^{*}$ to linear transformations on $T(M)$ is linear. We have

$i_{f}(m \otimes x) = f(m) x - m \otimes i_{f}(x)$ for all $m \in M \subset T(M)$, $x \in T(M)$
$i_{f}\left( T^{p} M \right) \subset T^{p-1} M$
$i_{f}^{2} = 0$
$i_{f} i_{g} + i_{g} i_{f} = 0$, for all $f, g \in M^{*}$

For $m_{1}, \ldots , m_{p} \in M$ we have

\[ i_{f}\left(m_{1} \otimes \cdots \otimes m_{p}\right)=\sum _{i=1}^{p}(-1)^{i-1} f\left(m_{i}\right) m_{1} \otimes \cdots \otimes \check{m}_{i} \otimes \cdots \otimes m_{p} \]

where $\check{m}_{i}$ denotes deletion (of $m_i$ from the multiplication).

For a quadratic form $Q$ on $M$, $\bar{i}_{f}$ can be defined on the quotient Clifford algebra:

\[ \iota \circ i_{f} = \bar{i}_{f} \circ \iota , \]

satisfying:

$\bar{i}_{f}(1) = 0$ for $1 \in \mathop{\mathcal{C}\ell }(Q)$
$\bar{i}_{f}\left( \iota (m) x \right) = f(m) x - \iota (m) \bar{i}_{f}(x)$ for all $m \in M$, $x \in \mathop{\mathcal{C}\ell }(Q)$

Let $F$ be a bilinear form on $M$. Then every $m \in M$ determines a linear form $f_{m}$ on $M$ defined as $f_{m}(m') = F(m, m')$.

We will denote by $i_{m}^{F}$ the antiderivation $i_{f_{m}}$. We have:

$i_{m}^{F}(1) = 0$,
$ i_{m}^{F}(m' \otimes x) = F(m, m') x - m' \otimes i_{m}^{F}(x) $ for all $m' \in M, x \in T(M)$

For $x_{1}, \ldots , x_{n}$ in $T(M)$, we have

\[ i_{m}^{F}\left(x_{1} \otimes \cdots \otimes x_{n}\right) = \sum _{j=1}^{n}(-1)^{j-1} F\left(m, x_{j}\right) x_{1} \otimes \cdots \otimes \check{x}_{j} \otimes \cdots \otimes x_{n} \]

As it was in the case with $\bar{i}_{f}$, we will denote by $\bar{i}_{x}^{F}$ the antiderivation $\bar{i}_{f}$ for $f_m(m') = F(m, m')$ :

\[ \bar{i}_{m}^{F}=\bar{i}_{f} \]

for $f_m(m') = F(m, m'), (m, m' \in M)$

This is the approach used in [ Bourbaki(2007) ] , and re-introduced in [ Jadczyk(2019) , Jadczyk(2023) ] .

$\bar{i_f}$ is denoted $\partial _v$ for $v \in \mathop{\mathcal{C}\ell }(Q)_1$ in [ Lundholm and Svensson(2009) ] .

This is closely related to contraction (i.e. $\iota (m)\rfloor x = m \rfloor _{F} x \doteq \bar{i}_{m}^{F}(x)$ for $Q = 0$ ) and interior product.

2.2 Operations