3.1. Clifford algebras🔗

To construct a Clifford algebra we must first give ourselves a quadratic form:

variable (R M : Type*)
  [CommRing R] [AddCommGroup M] [Module R M]
  (Q : QuadraticForm R M)

Given this data we may construct the associated Clifford algebra Cl(Q) as follows:

CliffordAlgebra Q : Type (max u_1 u_2)#check CliffordAlgebra Q

We can witness that this has the structure of an R-algebra as follows:

instAlgebraCliffordAlgebra Q#synth Algebra R (CliffordAlgebra Q)

The natural map from the module M into the Clifford algebra ι : M → Cl(Q) is written in Mathlib as CliffordAlgebra.ι Q. We may witness that this obeys the defining equation as follows:

open CliffordAlgebra in
example (m : M) :
    (ι Q m) ^ 2 = Q m • 1 := byR:Type u_1M:Type u_2inst✝²:CommRing Rinst✝¹:AddCommGroup Minst✝:Module R MQ:QuadraticForm R Mm:M⊢ (ι Q) m ^ 2 = Q m • 1
  rw [sq,R:Type u_1M:Type u_2inst✝²:CommRing Rinst✝¹:AddCommGroup Minst✝:Module R MQ:QuadraticForm R Mm:M⊢ (ι Q) m * (ι Q) m = Q m • 1 ι_sq_scalar,R:Type u_1M:Type u_2inst✝²:CommRing Rinst✝¹:AddCommGroup Minst✝:Module R MQ:QuadraticForm R Mm:M⊢ (algebraMap R (CliffordAlgebra Q)) (Q m) = Q m • 1 Algebra.smul_def,R:Type u_1M:Type u_2inst✝²:CommRing Rinst✝¹:AddCommGroup Minst✝:Module R MQ:QuadraticForm R Mm:M⊢ (algebraMap R (CliffordAlgebra Q)) (Q m) = (algebraMap R (CliffordAlgebra Q)) (Q m) * 1 mul_oneR:Type u_1M:Type u_2inst✝²:CommRing Rinst✝¹:AddCommGroup Minst✝:Module R MQ:QuadraticForm R Mm:M⊢ (algebraMap R (CliffordAlgebra Q)) (Q m) = (algebraMap R (CliffordAlgebra Q)) (Q m)]All goals completed! 🐙

This also shows that Mathlib's Clifford algebras adopt the positive sign convention.