# Clifford Algebras #

We construct the Clifford algebra of a module M over a commutative ring R, equipped with a quadratic form Q.

## Notation #

The Clifford algebra of the R-module M equipped with a quadratic form Q is an R-algebra denoted CliffordAlgebra Q.

Given a linear morphism f : M → A from a module M to another R-algebra A, such that cond : ∀ m, f m * f m = algebraMap _ _ (Q m), there is a (unique) lift of f to an R-algebra morphism from CliffordAlgebra Q to A, which is denoted CliffordAlgebra.lift Q f cond.

The canonical linear map M → CliffordAlgebra Q is denoted CliffordAlgebra.ι Q.

## Theorems #

The main theorems proved ensure that CliffordAlgebra Q satisfies the universal property of the Clifford algebra.

1. ι_comp_lift is the fact that the composition of ι Q with lift Q f cond agrees with f.
2. lift_unique ensures the uniqueness of lift Q f cond with respect to 1.

## Implementation details #

The Clifford algebra of M is constructed as a quotient of the tensor algebra, as follows.

1. We define a relation CliffordAlgebra.Rel Q on TensorAlgebra R M. This is the smallest relation which identifies squares of elements of M with Q m.
2. The Clifford algebra is the quotient of the tensor algebra by this relation.

This file is almost identical to Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean.

inductive CliffordAlgebra.Rel {R : Type u_1} [] {M : Type u_2} [] [Module R M] (Q : ) :
Prop

Rel relates each ι m * ι m, for m : M, with Q m.

The Clifford algebra of M is defined as the quotient modulo this relation.

Instances For
def CliffordAlgebra {R : Type u_1} [] {M : Type u_2} [] [Module R M] (Q : ) :
Type (max u_2 u_1)

The Clifford algebra of an R-module M equipped with a quadratic_form Q.

Equations
Instances For
instance CliffordAlgebra.instInhabited {R : Type u_1} [] {M : Type u_2} [] [Module R M] (Q : ) :
Equations
instance CliffordAlgebra.instRing {R : Type u_1} [] {M : Type u_2} [] [Module R M] (Q : ) :
Equations
@[instance 900]
instance CliffordAlgebra.instAlgebra' {R : Type u_3} {A : Type u_4} {M : Type u_5} [] [] [] [Algebra R A] [Module R M] [Module A M] (Q : ) [] :
Equations
instance CliffordAlgebra.instAlgebra {R : Type u_1} [] {M : Type u_2} [] [Module R M] (Q : ) :
Equations
instance CliffordAlgebra.instSMulCommClass {R : Type u_3} {S : Type u_4} {A : Type u_5} {M : Type u_6} [] [] [] [] [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M] (Q : ) [] [] :
Equations
• =
instance CliffordAlgebra.instIsScalarTower {R : Type u_3} {S : Type u_4} {A : Type u_5} {M : Type u_6} [] [] [] [] [SMul R S] [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M] [] [] [] (Q : ) :
Equations
• =
def CliffordAlgebra.ι {R : Type u_1} [] {M : Type u_2} [] [Module R M] (Q : ) :

The canonical linear map M →ₗ[R] CliffordAlgebra Q.

Equations
• = ().toLinearMap ∘ₗ
Instances For
@[simp]
theorem CliffordAlgebra.ι_sq_scalar {R : Type u_1} [] {M : Type u_2} [] [Module R M] (Q : ) (m : M) :
m * m = () (Q m)

As well as being linear, ι Q squares to the quadratic form

@[simp]
theorem CliffordAlgebra.comp_ι_sq_scalar {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } {A : Type u_3} [] [Algebra R A] (g : ) (m : M) :
g ( m) * g ( m) = () (Q m)
@[simp]
theorem CliffordAlgebra.lift_symm_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] (Q : ) {A : Type u_3} [] [Algebra R A] (F : ) :
.symm F = F.toLinearMap ∘ₗ ,
def CliffordAlgebra.lift {R : Type u_1} [] {M : Type u_2} [] [Module R M] (Q : ) {A : Type u_3} [] [Algebra R A] :
{ f : M →ₗ[R] A // ∀ (m : M), f m * f m = () (Q m) } ()

Given a linear map f : M →ₗ[R] A into an R-algebra A, which satisfies the condition: cond : ∀ m : M, f m * f m = Q(m), this is the canonical lift of f to a morphism of R-algebras from CliffordAlgebra Q to A.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CliffordAlgebra.ι_comp_lift {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } {A : Type u_3} [] [Algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), f m * f m = () (Q m)) :
( f, cond).toLinearMap ∘ₗ = f
@[simp]
theorem CliffordAlgebra.lift_ι_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } {A : Type u_3} [] [Algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), f m * f m = () (Q m)) (x : M) :
( f, cond) ( x) = f x
@[simp]
theorem CliffordAlgebra.lift_unique {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } {A : Type u_3} [] [Algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), f m * f m = () (Q m)) (g : ) :
g.toLinearMap ∘ₗ = f g = f, cond
@[simp]
theorem CliffordAlgebra.lift_comp_ι {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } {A : Type u_3} [] [Algebra R A] (g : ) :
g.toLinearMap ∘ₗ , = g
theorem CliffordAlgebra.hom_ext {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } {A : Type u_4} [] [Algebra R A] {f : } {g : } :
f.toLinearMap ∘ₗ = g.toLinearMap ∘ₗ f = g

See note [partially-applied ext lemmas].

theorem CliffordAlgebra.induction {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } {C : } (algebraMap : ∀ (r : R), C (() r)) (ι : ∀ (x : M), C ( x)) (mul : ∀ (a b : ), C aC bC (a * b)) (add : ∀ (a b : ), C aC bC (a + b)) (a : ) :
C a

If C holds for the algebraMap of r : R into CliffordAlgebra Q, the ι of x : M, and is preserved under addition and muliplication, then it holds for all of CliffordAlgebra Q.

See also the stronger CliffordAlgebra.left_induction and CliffordAlgebra.right_induction.

theorem CliffordAlgebra.mul_add_swap_eq_polar_of_forall_mul_self_eq {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } {A : Type u_4} [Ring A] [Algebra R A] (f : M →ₗ[R] A) (hf : ∀ (x : M), f x * f x = () (Q x)) (a : M) (b : M) :
f a * f b + f b * f a = () (QuadraticMap.polar (Q) a b)
theorem CliffordAlgebra.forall_mul_self_eq_iff {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } {A : Type u_4} [Ring A] [Algebra R A] (h2 : ) (f : M →ₗ[R] A) :
(∀ (x : M), f x * f x = () (Q x)) ().compl₂ f ∘ₗ f + ().flip.compl₂ f ∘ₗ f =

An alternative way to provide the argument to CliffordAlgebra.lift when 2 is invertible.

To show a function squares to the quadratic form, it suffices to show that f x * f y + f y * f x = algebraMap _ _ (polar Q x y)

theorem CliffordAlgebra.ι_mul_ι_add_swap {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } (a : M) (b : M) :
a * b + b * a = () (QuadraticMap.polar (Q) a b)

The symmetric product of vectors is a scalar

theorem CliffordAlgebra.ι_mul_ι_comm {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } (a : M) (b : M) :
a * b = () (QuadraticMap.polar (Q) a b) - b * a
@[simp]
theorem CliffordAlgebra.ι_mul_ι_add_swap_of_isOrtho {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } {a : M} {b : M} (h : ) :
a * b + b * a = 0
theorem CliffordAlgebra.ι_mul_ι_comm_of_isOrtho {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } {a : M} {b : M} (h : ) :
a * b = -( b * a)
theorem CliffordAlgebra.mul_ι_mul_ι_of_isOrtho {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } (x : ) {a : M} {b : M} (h : ) :
x * a * b = -(x * b * a)
theorem CliffordAlgebra.ι_mul_ι_mul_of_isOrtho {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } (x : ) {a : M} {b : M} (h : ) :
a * ( b * x) = -( b * ( a * x))
theorem CliffordAlgebra.ι_mul_ι_mul_ι {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } (a : M) (b : M) :
a * b * a = (QuadraticMap.polar (Q) a b a - Q a b)

$aba$ is a vector.

@[simp]
theorem CliffordAlgebra.ι_range_map_lift {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } {A : Type u_3} [] [Algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), f m * f m = () (Q m)) :
Submodule.map ( f, cond).toLinearMap =
def CliffordAlgebra.map {R : Type u_1} [] {M₁ : Type u_4} {M₂ : Type u_5} [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (f : Q₁ →qᵢ Q₂) :

Any linear map that preserves the quadratic form lifts to an AlgHom between algebras.

See CliffordAlgebra.equivOfIsometry for the case when f is a QuadraticForm.IsometryEquiv.

Equations
• = () ∘ₗ f.toLinearMap,
Instances For
@[simp]
theorem CliffordAlgebra.map_comp_ι {R : Type u_1} [] {M₁ : Type u_4} {M₂ : Type u_5} [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (f : Q₁ →qᵢ Q₂) :
.toLinearMap ∘ₗ = ∘ₗ f.toLinearMap
@[simp]
theorem CliffordAlgebra.map_apply_ι {R : Type u_1} [] {M₁ : Type u_4} {M₂ : Type u_5} [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (f : Q₁ →qᵢ Q₂) (m : M₁) :
(() m) = () (f m)
@[simp]
theorem CliffordAlgebra.map_id {R : Type u_1} [] {M₁ : Type u_4} [] [Module R M₁] (Q₁ : ) :
@[simp]
theorem CliffordAlgebra.map_comp_map {R : Type u_1} [] {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [] [] [] [Module R M₁] [Module R M₂] [Module R M₃] {Q₁ : } {Q₂ : } {Q₃ : } (f : Q₂ →qᵢ Q₃) (g : Q₁ →qᵢ Q₂) :
.comp = CliffordAlgebra.map (f.comp g)
@[simp]
theorem CliffordAlgebra.ι_range_map_map {R : Type u_1} [] {M₁ : Type u_4} {M₂ : Type u_5} [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (f : Q₁ →qᵢ Q₂) :
Submodule.map .toLinearMap () = Submodule.map () (LinearMap.range f.toLinearMap)
theorem CliffordAlgebra.leftInverse_map_of_leftInverse {R : Type u_1} [] {M₁ : Type u_4} {M₂ : Type u_5} [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (f : Q₁ →qᵢ Q₂) (g : Q₂ →qᵢ Q₁) (h : ) :

If f is a linear map from M₁ to M₂ that preserves the quadratic forms, and if it has a linear retraction g that also preserves the quadratic forms, then CliffordAlgebra.map g is a retraction of CliffordAlgebra.map f.

theorem CliffordAlgebra.map_surjective {R : Type u_1} [] {M₁ : Type u_4} {M₂ : Type u_5} [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (f : Q₁ →qᵢ Q₂) (hf : ) :

If a linear map preserves the quadratic forms and is surjective, then the algebra maps it induces between Clifford algebras is also surjective.

@[simp]
theorem CliffordAlgebra.equivOfIsometry_apply {R : Type u_1} [] {M₁ : Type u_4} {M₂ : Type u_5} [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (e : Q₁.IsometryEquiv Q₂) (a : ) :
= (CliffordAlgebra.map e.toIsometry) a
def CliffordAlgebra.equivOfIsometry {R : Type u_1} [] {M₁ : Type u_4} {M₂ : Type u_5} [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (e : Q₁.IsometryEquiv Q₂) :

Two CliffordAlgebras are equivalent as algebras if their quadratic forms are equivalent.

Equations
Instances For
@[simp]
theorem CliffordAlgebra.equivOfIsometry_symm {R : Type u_1} [] {M₁ : Type u_4} {M₂ : Type u_5} [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (e : Q₁.IsometryEquiv Q₂) :
.symm =
@[simp]
theorem CliffordAlgebra.equivOfIsometry_trans {R : Type u_1} [] {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [] [] [] [Module R M₁] [Module R M₂] [Module R M₃] {Q₁ : } {Q₂ : } {Q₃ : } (e₁₂ : Q₁.IsometryEquiv Q₂) (e₂₃ : Q₂.IsometryEquiv Q₃) :
.trans = CliffordAlgebra.equivOfIsometry (e₁₂.trans e₂₃)
@[simp]
theorem CliffordAlgebra.equivOfIsometry_refl {R : Type u_1} [] {M₁ : Type u_4} [] [Module R M₁] {Q₁ : } :
= AlgEquiv.refl
def TensorAlgebra.toClifford {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } :

The canonical image of the TensorAlgebra in the CliffordAlgebra, which maps TensorAlgebra.ι R x to CliffordAlgebra.ι Q x.

Equations
• TensorAlgebra.toClifford =
Instances For
@[simp]
theorem TensorAlgebra.toClifford_ι {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } (m : M) :
TensorAlgebra.toClifford (() m) = m