Clifford Algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 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 from clifford_algebra Q to A, 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_liftis the fact that the composition ofι Qwithlift Q f condagrees withf.lift_uniqueensures the uniqueness oflift Q f condwith 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 Qontensor_algebra R M. This is the smallest relation which identifies squares of elements ofMwithQ 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.
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
- 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.
@[protected, 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) :
@[irreducible]
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
@[protected, 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)
@[protected, 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)
@[irreducible]
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
@[simp]
theorem
clifford_algebra.ι_sq_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
@[simp]
theorem
clifford_algebra.comp_ι_sq_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)
@[irreducible]
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] :
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 := _}
@[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), _⟩
@[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
@[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
@[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⟩
@[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
@[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
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.
See also the stronger clifford_algebra.left_induction and clifford_algebra.right_induction.
theorem
clifford_algebra.ι_mul_ι_add_swap
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(a b : M) :
⇑(clifford_algebra.ι Q) a * ⇑(clifford_algebra.ι Q) b + ⇑(clifford_algebra.ι Q) b * ⇑(clifford_algebra.ι Q) a = ⇑(algebra_map R (clifford_algebra Q)) (quadratic_form.polar ⇑Q a b)
The symmetric product of vectors is a scalar
theorem
clifford_algebra.ι_mul_comm
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(a b : M) :
⇑(clifford_algebra.ι Q) a * ⇑(clifford_algebra.ι Q) b = ⇑(algebra_map R (clifford_algebra Q)) (quadratic_form.polar ⇑Q a b) - ⇑(clifford_algebra.ι Q) b * ⇑(clifford_algebra.ι Q) a
theorem
clifford_algebra.ι_mul_ι_mul_ι
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(a b : M) :
⇑(clifford_algebra.ι Q) a * ⇑(clifford_algebra.ι Q) b * ⇑(clifford_algebra.ι Q) a = ⇑(clifford_algebra.ι Q) (quadratic_form.polar ⇑Q a b • a - ⇑Q a • b)
$aba$ is a vector.
@[simp]
theorem
clifford_algebra.ι_range_map_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)) :
submodule.map (⇑(clifford_algebra.lift Q) ⟨f, cond⟩).to_linear_map (linear_map.range (clifford_algebra.ι Q)) = linear_map.range f
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₂]
[module R M₁]
[module R M₂]
(Q₁ : quadratic_form R M₁)
(Q₂ : quadratic_form R M₂)
(f : M₁ →ₗ[R] M₂)
(hf : ∀ (m : M₁), ⇑Q₂ (⇑f m) = ⇑Q₁ m) :
clifford_algebra Q₁ →ₐ[R] clifford_algebra Q₂
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
- clifford_algebra.map Q₁ Q₂ f hf = ⇑(clifford_algebra.lift Q₁) ⟨(clifford_algebra.ι Q₂).comp f, _⟩
@[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₂]
[module R M₁]
[module R M₂]
(Q₁ : quadratic_form R M₁)
(Q₂ : quadratic_form R M₂)
(f : M₁ →ₗ[R] M₂)
(hf : ∀ (m : M₁), ⇑Q₂ (⇑f m) = ⇑Q₁ m) :
(clifford_algebra.map Q₁ Q₂ f hf).to_linear_map.comp (clifford_algebra.ι Q₁) = (clifford_algebra.ι Q₂).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₂]
[module R M₁]
[module R M₂]
(Q₁ : quadratic_form R M₁)
(Q₂ : quadratic_form R M₂)
(f : M₁ →ₗ[R] M₂)
(hf : ∀ (m : M₁), ⇑Q₂ (⇑f m) = ⇑Q₁ m)
(m : M₁) :
⇑(clifford_algebra.map Q₁ Q₂ f hf) (⇑(clifford_algebra.ι Q₁) m) = ⇑(clifford_algebra.ι Q₂) (⇑f m)
@[simp]
theorem
clifford_algebra.map_id
{R : Type u_1}
[comm_ring R]
{M₁ : Type u_4}
[add_comm_group M₁]
[module R M₁]
(Q₁ : quadratic_form R M₁) :
clifford_algebra.map Q₁ Q₁ linear_map.id _ = alg_hom.id R (clifford_algebra Q₁)
@[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₃]
[module R M₁]
[module R M₂]
[module R M₃]
(Q₁ : quadratic_form R M₁)
(Q₂ : quadratic_form R M₂)
(Q₃ : quadratic_form R 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) :
(clifford_algebra.map Q₂ Q₃ f hf).comp (clifford_algebra.map Q₁ Q₂ g hg) = clifford_algebra.map Q₁ Q₃ (f.comp g) _
@[simp]
theorem
clifford_algebra.ι_range_map_map
{R : Type u_1}
[comm_ring R]
{M₁ : Type u_4}
{M₂ : Type u_5}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(Q₁ : quadratic_form R M₁)
(Q₂ : quadratic_form R M₂)
(f : M₁ →ₗ[R] M₂)
(hf : ∀ (m : M₁), ⇑Q₂ (⇑f m) = ⇑Q₁ m) :
submodule.map (clifford_algebra.map Q₁ Q₂ f hf).to_linear_map (linear_map.range (clifford_algebra.ι Q₁)) = submodule.map (clifford_algebra.ι Q₂) (linear_map.range f)
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₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
(e : Q₁.isometry Q₂) :
clifford_algebra Q₁ ≃ₐ[R] clifford_algebra Q₂
Two clifford_algebras are equivalent as algebras if their quadratic forms are
equivalent.
Equations
- clifford_algebra.equiv_of_isometry e = alg_equiv.of_alg_hom (clifford_algebra.map Q₁ Q₂ ↑e _) (clifford_algebra.map Q₂ Q₁ ↑(e.symm) _) _ _
@[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₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
(e : Q₁.isometry Q₂)
(ᾰ : clifford_algebra Q₁) :
⇑(clifford_algebra.equiv_of_isometry e) ᾰ = ⇑(clifford_algebra.map 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₂]
[module R M₁]
[module R M₂]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R 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₃]
[module R M₁]
[module R M₂]
[module R M₃]
{Q₁ : quadratic_form R M₁}
{Q₂ : quadratic_form R M₂}
{Q₃ : quadratic_form R 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₁]
[module R M₁]
{Q₁ : quadratic_form R M₁} :
def
clifford_algebra.invertible_ι_of_invertible
{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)
[invertible (⇑Q m)] :
invertible (⇑(clifford_algebra.ι Q) m)
If the quadratic form of a vector is invertible, then so is that vector.
Equations
- clifford_algebra.invertible_ι_of_invertible Q m = {inv_of := ⇑(clifford_algebra.ι Q) (⅟ (⇑Q m) • m), inv_of_mul_self := _, mul_inv_of_self := _}
theorem
clifford_algebra.inv_of_ι
{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)
[invertible (⇑Q m)]
[invertible (⇑(clifford_algebra.ι Q) m)] :
⅟ (⇑(clifford_algebra.ι Q) m) = ⇑(clifford_algebra.ι Q) (⅟ (⇑Q m) • m)
For a vector with invertible quadratic form, $v^{-1} = \frac{v}{Q(v)}$
theorem
clifford_algebra.is_unit_ι_of_is_unit
{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}
(h : is_unit (⇑Q m)) :
is_unit (⇑(clifford_algebra.ι Q) m)
theorem
clifford_algebra.ι_mul_ι_mul_inv_of_ι
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(a b : M)
[invertible (⇑(clifford_algebra.ι Q) a)]
[invertible (⇑Q a)] :
⇑(clifford_algebra.ι Q) a * ⇑(clifford_algebra.ι Q) b * ⅟ (⇑(clifford_algebra.ι Q) a) = ⇑(clifford_algebra.ι Q) ((⅟ (⇑Q a) * quadratic_form.polar ⇑Q a b) • a - b)
$aba^{-1}$ is a vector.
theorem
clifford_algebra.inv_of_ι_mul_ι_mul_ι
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(a b : M)
[invertible (⇑(clifford_algebra.ι Q) a)]
[invertible (⇑Q a)] :
⅟ (⇑(clifford_algebra.ι Q) a) * ⇑(clifford_algebra.ι Q) b * ⇑(clifford_algebra.ι Q) a = ⇑(clifford_algebra.ι Q) ((⅟ (⇑Q a) * quadratic_form.polar ⇑Q a b) • a - b)
$a^{-1}ba$ is a vector.
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
@[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