« Home

Remark. [ca-000D]
✍️source

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

Context

Definition [ca-000F]

Definition. Clifford algebra [wieser2022formalizing] [ca-0006]
CliffordAlgebra TensorAlgebra.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_lift CliffordAlgebra.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:

\(F \circ \iota = f\), i.e. the following diagram commutes:
$\text{[math]}$
\(\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]
✍️source

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