Dependencies

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

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:

1. \(i_{f}(1) = 0\)

2. \(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

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

2. \(i_{f}\left( T^{p} M \right) \subset T^{p-1} M\)

3. \(i_{f}^{2} = 0\)

4. \(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

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:

satisfying:

1. \(\bar{i}_{f}(1) = 0\) for \(1 \in \mathop{\mathcal{C}\ell }(Q)\)

2. \(\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:

1. \(i_{m}^{F}(1) = 0\),

2. \( 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

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')\) :

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.

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 \(\mathop{\mathcal{C}\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 \mathop{\mathcal{C}\ell }(Q)\) in some literatures, or \(\pi _\Phi \)/\(\pi _Q\) to emphasize the bilinear form \(\Phi \) or the quadratic form \(Q\), respectively.

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:

for all \(x \in \mathop{\mathcal{C}\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):

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

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

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:

1. \(\alpha \circ \alpha = \operatorname {id}\)

2. \(\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) ] .

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

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

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 \(\mathop{\mathcal{C}\ell }(Q)\) to \(A\), denoted \(\operatorname {lift} f : \mathop{\mathcal{C}\ell }(Q) \to _{a}A\).

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:

1. \(\tau (m_1 m_2) = \tau (m_2) \tau (m_1)\)

2. \(\tau \circ \tau = \operatorname {id}\)

3. \(\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) ] .

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 : \mathop{\mathcal{C}\ell }(Q) \to _{a}A\), we have:

\( G \circ \iota = f \iff G = \operatorname {lift} f\)