mathlib documentation

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

source
inductive clifford_algebra.rel {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (Q : quadratic_form R M) :
tensor_algebra R M → tensor_algebra R M → 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.

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

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

Equations
source
@[instance]
def clifford_algebra.algebra {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (Q : quadratic_form R M) :
algebra R (clifford_algebra Q)
source
@[instance]
def clifford_algebra.ring {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (Q : quadratic_form R M) :
ring (clifford_algebra Q)
source
def clifford_algebra.ι {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (Q : quadratic_form R M) :
M →ₗ[R] clifford_algebra Q

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

Equations
source
@[simp]
theorem clifford_algebra.ι_square_scalar {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (Q : quadratic_form R M) (m : M) :
(⇑(clifford_algebra.ι Q) m) * ⇑(clifford_algebra.ι Q) m = ⇑(algebra_map R (clifford_algebra Q)) (⇑Q m)

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

source
@[simp]
theorem clifford_algebra.comp_ι_square_scalar {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} {A : Type u_3} [semiring A] [algebra R A] (g : clifford_algebra Q →ₐ[R] A) (m : M) :
(⇑g (⇑(clifford_algebra.ι Q) m)) * ⇑g (⇑(clifford_algebra.ι Q) m) = ⇑(algebra_map R A) (⇑Q m)
source
def clifford_algebra.lift {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (Q : quadratic_form R M) {A : Type u_3} [semiring A] [algebra R A] :
{f // ∀ (m : M), (⇑f m) * ⇑f m = ⇑(algebra_map R A) (⇑Q m)} ≃ (clifford_algebra Q →ₐ[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
source
@[simp]
theorem clifford_algebra.lift_symm_apply {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (Q : quadratic_form R M) {A : Type u_3} [semiring A] [algebra R A] (F : clifford_algebra Q →ₐ[R] A) :
⇑((clifford_algebra.lift Q).symm) F = ⟨F.to_linear_map.comp (clifford_algebra.ι Q), _⟩
source
@[simp]
theorem clifford_algebra.ι_comp_lift {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} {A : Type u_3} [semiring A] [algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), (⇑f m) * ⇑f m = ⇑(algebra_map R A) (⇑Q m)) :
(⇑(clifford_algebra.lift Q) ⟨f, cond⟩).to_linear_map.comp (clifford_algebra.ι Q) = f
source
@[simp]
theorem clifford_algebra.lift_ι_apply {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} {A : Type u_3} [semiring A] [algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), (⇑f m) * ⇑f m = ⇑(algebra_map R A) (⇑Q m)) (x : M) :
⇑(⇑(clifford_algebra.lift Q) ⟨f, cond⟩) (⇑(clifford_algebra.ι Q) x) = ⇑f x
source
@[simp]
theorem clifford_algebra.lift_unique {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} {A : Type u_3} [semiring A] [algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), (⇑f m) * ⇑f m = ⇑(algebra_map R A) (⇑Q m)) (g : clifford_algebra Q →ₐ[R] A) :
g.to_linear_map.comp (clifford_algebra.ι Q) = f ↔ g = ⇑(clifford_algebra.lift Q) ⟨f, cond⟩
source
@[simp]
theorem clifford_algebra.lift_comp_ι {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} {A : Type u_3} [semiring A] [algebra R A] (g : clifford_algebra Q →ₐ[R] A) :
⇑(clifford_algebra.lift Q) ⟨g.to_linear_map.comp (clifford_algebra.ι Q), _⟩ = g
source
@[ext]
theorem clifford_algebra.hom_ext {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} {A : Type u_3} [semiring A] [algebra R A] {f g : clifford_algebra Q →ₐ[R] A} :
f.to_linear_map.comp (clifford_algebra.ι Q) = g.to_linear_map.comp (clifford_algebra.ι Q) → f = g

See note [partially-applied ext lemmas].

source
theorem clifford_algebra.induction {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} {C : clifford_algebra Q → Prop} (h_grade0 : ∀ (r : R), C (⇑(algebra_map R (clifford_algebra Q)) r)) (h_grade1 : ∀ (x : M), C (⇑(clifford_algebra.ι Q) x)) (h_mul : ∀ (a b : clifford_algebra Q), C a → C b → C (a * b)) (h_add : ∀ (a b : clifford_algebra Q), C a → C b → C (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.

source
def clifford_algebra.as_exterior {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] :
clifford_algebra 0 ≃ₐ[R] exterior_algebra R M

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

Equations
source
def tensor_algebra.to_clifford {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} :
tensor_algebra R M →ₐ[R] clifford_algebra Q

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

Equations
source
@[simp]
theorem tensor_algebra.to_clifford_ι {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (m : M) :
⇑tensor_algebra.to_clifford (⇑(tensor_algebra.ι R) m) = ⇑(clifford_algebra.ι Q) m