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.
ι_comp_lift
is the fact that the composition ofι Q
withlift Q f cond
agrees withf
.lift_unique
ensures the uniqueness oflift 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.
- We define a relation
clifford_algebra.rel Q
ontensor_algebra R M
. This is the smallest relation which identifies squares of elements ofM
withQ m
. - The Clifford algebra is the quotient of the tensor algebra by this relation.
This file is almost identical to linear_algebra/exterior_algebra.lean
.
- of : ∀ {R : Type u_1} [_inst_1 : comm_ring R] {M : Type u_2} [_inst_2 : add_comm_group M] [_inst_3 : module R M] (Q : quadratic_form R M) (m : M), clifford_algebra.rel Q ((⇑(tensor_algebra.ι R) m) * ⇑(tensor_algebra.ι R) m) (⇑(algebra_map R (tensor_algebra R 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.
The Clifford algebra of an R
-module M
equipped with a quadratic_form Q
.
Equations
The canonical linear map M →ₗ[R] clifford_algebra Q
.
Equations
As well as being linear, ι Q
squares to the quadratic form
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
- clifford_algebra.lift Q = {to_fun := λ (f : {f // ∀ (m : M), (⇑f m) * ⇑f m = ⇑(algebra_map R A) (⇑Q m)}), ⇑(ring_quot.lift_alg_hom R) ⟨⇑(tensor_algebra.lift R) ↑f, _⟩, inv_fun := λ (F : clifford_algebra Q →ₐ[R] A), ⟨F.to_linear_map.comp (clifford_algebra.ι Q), _⟩, left_inv := _, right_inv := _}
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
.
A Clifford algebra with a zero quadratic form is isomorphic to an exterior_algebra
Equations
- clifford_algebra.as_exterior = alg_equiv.of_alg_hom (⇑(clifford_algebra.lift 0) ⟨exterior_algebra.ι R _inst_3, _⟩) (⇑(exterior_algebra.lift R) ⟨clifford_algebra.ι 0, _⟩) clifford_algebra.as_exterior._proof_3 clifford_algebra.as_exterior._proof_4
The canonical image of the tensor_algebra
in the clifford_algebra
, which maps
tensor_algebra.ι R x
to clifford_algebra.ι Q x
.