# mathlibdocumentation

linear_algebra.clifford_algebra.basic

# 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 denoted as clifford_algebra 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 = algebra_map _ _ (Q m), there is a (unique) lift of f to an R-algebra morphism, which is denoted clifford_algebra.lift Q f cond.

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

## Theorems #

The main theorems proved ensure that clifford_algebra 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.

Additionally, when Q = 0 an alg_equiv to the exterior_algebra is provided as as_exterior.

## Implementation details #

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

1. We define a relation clifford_algebra.rel Q on tensor_algebra 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 linear_algebra/exterior_algebra.lean.

inductive clifford_algebra.rel {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] (Q : M) :
→ Prop
• of : ∀ {R : Type u_1} [_inst_1 : {M : Type u_2} [_inst_2 : [_inst_3 : M] (Q : M) (m : M), (( m) * m) ( M)) (Q m))

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

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

@[instance]
def clifford_algebra.inhabited {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] (Q : M) :
def clifford_algebra {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] (Q : M) :
Type (max u_1 u_2)

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

Equations
@[instance]
def clifford_algebra.algebra {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] (Q : M) :
@[instance]
def clifford_algebra.ring {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] (Q : M) :
def clifford_algebra.ι {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] (Q : M) :

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

Equations
@[simp]
theorem clifford_algebra.ι_sq_scalar {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] (Q : M) (m : M) :
( m) * m = (clifford_algebra Q)) (Q m)

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

@[simp]
theorem clifford_algebra.comp_ι_sq_scalar {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {Q : M} {A : Type u_3} [semiring A] [ A] (g : →ₐ[R] A) (m : M) :
(g ( m)) * g ( m) = A) (Q m)
def clifford_algebra.lift {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] (Q : M) {A : Type u_3} [semiring A] [ A] :
{f // ∀ (m : M), (f m) * f m = A) (Q m)} →ₐ[R] A)

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 clifford_algebra Q to A.

Equations
@[simp]
theorem clifford_algebra.lift_symm_apply {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] (Q : M) {A : Type u_3} [semiring A] [ A] (F : →ₐ[R] A) :
.symm) F = , _⟩
@[simp]
theorem clifford_algebra.ι_comp_lift {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {Q : M} {A : Type u_3} [semiring A] [ A] (f : M →ₗ[R] A) (cond : ∀ (m : M), (f m) * f m = A) (Q m)) :
f, cond⟩).to_linear_map.comp = f
@[simp]
theorem clifford_algebra.lift_ι_apply {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {Q : M} {A : Type u_3} [semiring A] [ A] (f : M →ₗ[R] A) (cond : ∀ (m : M), (f m) * f m = A) (Q m)) (x : M) :
f, cond⟩) ( x) = f x
@[simp]
theorem clifford_algebra.lift_unique {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {Q : M} {A : Type u_3} [semiring A] [ A] (f : M →ₗ[R] A) (cond : ∀ (m : M), (f m) * f m = A) (Q m)) (g : →ₐ[R] A) :
= f g = f, cond⟩
@[simp]
theorem clifford_algebra.lift_comp_ι {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {Q : M} {A : Type u_3} [semiring A] [ A] (g : →ₐ[R] A) :
, _⟩ = g
@[ext]
theorem clifford_algebra.hom_ext {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {Q : M} {A : Type u_3} [semiring A] [ A] {f g : →ₐ[R] A} :
f = g
theorem clifford_algebra.induction {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {Q : M} {C : → Prop} (h_grade0 : ∀ (r : R), C ( (clifford_algebra Q)) r)) (h_grade1 : ∀ (x : M), C ( x)) (h_mul : ∀ (a b : , C aC bC (a * b)) (h_add : ∀ (a b : , C aC bC (a + b)) (a : clifford_algebra Q) :
C a

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

def clifford_algebra.as_exterior {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] :

A Clifford algebra with a zero quadratic form is isomorphic to an exterior_algebra

Equations
theorem clifford_algebra.ι_mul_ι_add_swap {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {Q : M} (a b : M) :
( a) * b + ( b) * a = (clifford_algebra Q)) b)

The symmetric product of vectors is a scalar

def clifford_algebra.map {R : Type u_1} [comm_ring R] {M₁ : Type u_4} {M₂ : Type u_5} [add_comm_group M₁] [add_comm_group M₂] [ M₁] [ M₂] (Q₁ : M₁) (Q₂ : M₂) (f : M₁ →ₗ[R] M₂) (hf : ∀ (m : M₁), Q₂ (f m) = Q₁ m) :

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

See clifford_algebra.equiv_of_isometry for the case when f is a quadratic_form.isometry.

Equations
@[simp]
theorem clifford_algebra.map_comp_ι {R : Type u_1} [comm_ring R] {M₁ : Type u_4} {M₂ : Type u_5} [add_comm_group M₁] [add_comm_group M₂] [ M₁] [ M₂] (Q₁ : M₁) (Q₂ : M₂) (f : M₁ →ₗ[R] M₂) (hf : ∀ (m : M₁), Q₂ (f m) = Q₁ m) :
Q₂ f hf).to_linear_map.comp = .comp f
@[simp]
theorem clifford_algebra.map_apply_ι {R : Type u_1} [comm_ring R] {M₁ : Type u_4} {M₂ : Type u_5} [add_comm_group M₁] [add_comm_group M₂] [ M₁] [ M₂] (Q₁ : M₁) (Q₂ : M₂) (f : M₁ →ₗ[R] M₂) (hf : ∀ (m : M₁), Q₂ (f m) = Q₁ m) (m : M₁) :
Q₂ f hf) ( m) = (f m)
@[simp]
theorem clifford_algebra.map_id {R : Type u_1} [comm_ring R] {M₁ : Type u_4} [add_comm_group M₁] [ M₁] (Q₁ : M₁) :
@[simp]
theorem clifford_algebra.map_comp_map {R : Type u_1} [comm_ring R] {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [add_comm_group M₃] [ M₁] [ M₂] [ M₃] (Q₁ : M₁) (Q₂ : M₂) (Q₃ : M₃) (f : M₂ →ₗ[R] M₃) (hf : ∀ (m : M₂), Q₃ (f m) = Q₂ m) (g : M₁ →ₗ[R] M₂) (hg : ∀ (m : M₁), Q₂ (g m) = Q₁ m) :
Q₃ f hf).comp Q₂ g hg) = Q₃ (f.comp g) _
def clifford_algebra.equiv_of_isometry {R : Type u_1} [comm_ring R] {M₁ : Type u_4} {M₂ : Type u_5} [add_comm_group M₁] [add_comm_group M₂] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} (e : Q₁.isometry Q₂) :

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

Equations
@[simp]
theorem clifford_algebra.equiv_of_isometry_apply {R : Type u_1} [comm_ring R] {M₁ : Type u_4} {M₂ : Type u_5} [add_comm_group M₁] [add_comm_group M₂] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} (e : Q₁.isometry Q₂) (ᾰ : clifford_algebra Q₁) :
= Q₂ e _)
@[simp]
theorem clifford_algebra.equiv_of_isometry_symm {R : Type u_1} [comm_ring R] {M₁ : Type u_4} {M₂ : Type u_5} [add_comm_group M₁] [add_comm_group M₂] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} (e : Q₁.isometry Q₂) :
@[simp]
theorem clifford_algebra.equiv_of_isometry_trans {R : Type u_1} [comm_ring R] {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [add_comm_group M₃] [ M₁] [ M₂] [ M₃] {Q₁ : M₁} {Q₂ : M₂} {Q₃ : M₃} (e₁₂ : Q₁.isometry Q₂) (e₂₃ : Q₂.isometry Q₃) :
@[simp]
theorem clifford_algebra.equiv_of_isometry_refl {R : Type u_1} [comm_ring R] {M₁ : Type u_4} [add_comm_group M₁] [ M₁] {Q₁ : M₁} :
def tensor_algebra.to_clifford {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {Q : M} :

The canonical image of the tensor_algebra in the clifford_algebra, which maps tensor_algebra.ι R x to clifford_algebra.ι Q x.

Equations
@[simp]
theorem tensor_algebra.to_clifford_ι {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {Q : M} (m : M) :