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.

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.

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

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.

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.

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

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

The universal property of the Clifford algebras is now proven, and should be used instead of the definition that is subject to change.

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

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

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

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

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

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