Contraction in Clifford Algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file contains some of the results from [grinberg_clifford_2016][].
The key result is clifford_algebra.equiv_exterior.
Main definitions #
clifford_algebra.contract_left: contract a multivector by amodule.dual R Mon the left.clifford_algebra.contract_right: contract a multivector by amodule.dual R Mon the right.clifford_algebra.change_form: convert between two algebras of different quadratic form, sending vectors to vectors. The difference of the quadratic forms must be a bilinear form.clifford_algebra.equiv_exterior: in characteristic not-two, theclifford_algebra Qis isomorphic as a module to the exterior algebra.
Implementation notes #
This file somewhat follows [grinberg_clifford_2016][], although we are missing some of the induction principles needed to prove many of the results. Here, we avoid the quotient-based approach described in [grinberg_clifford_2016][], instead directly constructing our objects using the universal property.
Note that [grinberg_clifford_2016][] concludes that its contents are not novel, and are in fact just a rehash of parts of [bourbaki2007][]; we should at some point consider swapping our references to refer to the latter.
Within this file, we use the local notation
x ⌊ dforcontract_right x dd ⌋ xforcontract_left d x
def
clifford_algebra.contract_left_aux
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(d : module.dual R M) :
M →ₗ[R] clifford_algebra Q × clifford_algebra Q →ₗ[R] clifford_algebra Q
Auxiliary construction for clifford_algebra.contract_left
Equations
- clifford_algebra.contract_left_aux Q d = linear_map.smul_right d (linear_map.fst R (clifford_algebra Q) (clifford_algebra Q)) - ((algebra.lmul R (clifford_algebra Q)).to_linear_map.comp (clifford_algebra.ι Q)).compl₂ (linear_map.snd R (clifford_algebra Q) (clifford_algebra Q))
@[simp]
theorem
clifford_algebra.contract_left_aux_apply_apply
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(d : module.dual R M)
(ᾰ : M)
(ᾰ_1 : clifford_algebra Q × clifford_algebra Q) :
theorem
clifford_algebra.contract_left_aux_contract_left_aux
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(d : module.dual R M)
(v : M)
(x fx : clifford_algebra Q) :
⇑(⇑(clifford_algebra.contract_left_aux Q d) v) (⇑(clifford_algebra.ι Q) v * x, ⇑(⇑(clifford_algebra.contract_left_aux Q d) v) (x, fx)) = ⇑Q v • fx
def
clifford_algebra.contract_left
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M} :
module.dual R M →ₗ[R] clifford_algebra Q →ₗ[R] clifford_algebra Q
Contract an element of the clifford algebra with an element d : module.dual R M from the left.
Note that $v ⌋ x$ is spelt contract_left (Q.associated v) x.
This includes [grinberg_clifford_2016][] Theorem 10.75
Equations
- clifford_algebra.contract_left = {to_fun := λ (d : module.dual R M), clifford_algebra.foldr' Q (clifford_algebra.contract_left_aux Q d) _ 0, map_add' := _, map_smul' := _}
def
clifford_algebra.contract_right
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M} :
clifford_algebra Q →ₗ[R] module.dual R M →ₗ[R] clifford_algebra Q
Contract an element of the clifford algebra with an element d : module.dual R M from the
right.
Note that $x ⌊ v$ is spelt contract_right x (Q.associated v).
This includes [grinberg_clifford_2016][] Theorem 16.75
theorem
clifford_algebra.contract_right_eq
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(d : module.dual R M)
(x : clifford_algebra Q) :
theorem
clifford_algebra.contract_left_ι_mul
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(d : module.dual R M)
(a : M)
(b : clifford_algebra Q) :
⇑(⇑clifford_algebra.contract_left d) (⇑(clifford_algebra.ι Q) a * b) = ⇑d a • b - ⇑(clifford_algebra.ι Q) a * ⇑(⇑clifford_algebra.contract_left d) b
This is [grinberg_clifford_2016][] Theorem 6
theorem
clifford_algebra.contract_right_mul_ι
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(d : module.dual R M)
(a : M)
(b : clifford_algebra Q) :
⇑(⇑clifford_algebra.contract_right (b * ⇑(clifford_algebra.ι Q) a)) d = ⇑d a • b - ⇑(⇑clifford_algebra.contract_right b) d * ⇑(clifford_algebra.ι Q) a
This is [grinberg_clifford_2016][] Theorem 12
theorem
clifford_algebra.contract_left_algebra_map_mul
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(d : module.dual R M)
(r : R)
(b : clifford_algebra Q) :
⇑(⇑clifford_algebra.contract_left d) (⇑(algebra_map R (clifford_algebra Q)) r * b) = ⇑(algebra_map R (clifford_algebra Q)) r * ⇑(⇑clifford_algebra.contract_left d) b
theorem
clifford_algebra.contract_left_mul_algebra_map
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(d : module.dual R M)
(a : clifford_algebra Q)
(r : R) :
⇑(⇑clifford_algebra.contract_left d) (a * ⇑(algebra_map R (clifford_algebra Q)) r) = ⇑(⇑clifford_algebra.contract_left d) a * ⇑(algebra_map R (clifford_algebra Q)) r
theorem
clifford_algebra.contract_right_algebra_map_mul
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(d : module.dual R M)
(r : R)
(b : clifford_algebra Q) :
⇑(⇑clifford_algebra.contract_right (⇑(algebra_map R (clifford_algebra Q)) r * b)) d = ⇑(algebra_map R (clifford_algebra Q)) r * ⇑(⇑clifford_algebra.contract_right b) d
theorem
clifford_algebra.contract_right_mul_algebra_map
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(d : module.dual R M)
(a : clifford_algebra Q)
(r : R) :
⇑(⇑clifford_algebra.contract_right (a * ⇑(algebra_map R (clifford_algebra Q)) r)) d = ⇑(⇑clifford_algebra.contract_right a) d * ⇑(algebra_map R (clifford_algebra Q)) r
@[simp]
theorem
clifford_algebra.contract_left_ι
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(d : module.dual R M)
(x : M) :
⇑(⇑clifford_algebra.contract_left d) (⇑(clifford_algebra.ι Q) x) = ⇑(algebra_map R (clifford_algebra Q)) (⇑d x)
@[simp]
theorem
clifford_algebra.contract_right_ι
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(d : module.dual R M)
(x : M) :
⇑(⇑clifford_algebra.contract_right (⇑(clifford_algebra.ι Q) x)) d = ⇑(algebra_map R (clifford_algebra Q)) (⇑d x)
@[simp]
theorem
clifford_algebra.contract_left_algebra_map
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(d : module.dual R M)
(r : R) :
⇑(⇑clifford_algebra.contract_left d) (⇑(algebra_map R (clifford_algebra Q)) r) = 0
@[simp]
theorem
clifford_algebra.contract_right_algebra_map
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(d : module.dual R M)
(r : R) :
⇑(⇑clifford_algebra.contract_right (⇑(algebra_map R (clifford_algebra Q)) r)) d = 0
@[simp]
theorem
clifford_algebra.contract_left_one
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(d : module.dual R M) :
⇑(⇑clifford_algebra.contract_left d) 1 = 0
@[simp]
theorem
clifford_algebra.contract_right_one
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(d : module.dual R M) :
⇑(⇑clifford_algebra.contract_right 1) d = 0
theorem
clifford_algebra.contract_left_contract_left
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(d : module.dual R M)
(x : clifford_algebra Q) :
This is [grinberg_clifford_2016][] Theorem 7
theorem
clifford_algebra.contract_right_contract_right
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(d : module.dual R M)
(x : clifford_algebra Q) :
This is [grinberg_clifford_2016][] Theorem 13
theorem
clifford_algebra.contract_left_comm
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(d d' : module.dual R M)
(x : clifford_algebra Q) :
This is [grinberg_clifford_2016][] Theorem 8
theorem
clifford_algebra.contract_right_comm
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(d d' : module.dual R M)
(x : clifford_algebra Q) :
This is [grinberg_clifford_2016][] Theorem 14
def
clifford_algebra.change_form_aux
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(B : bilin_form R M) :
M →ₗ[R] clifford_algebra Q →ₗ[R] clifford_algebra Q
Auxiliary construction for clifford_algebra.change_form
Equations
@[simp]
theorem
clifford_algebra.change_form_aux_apply_apply
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(B : bilin_form R M)
(ᾰ : M)
(ᾰ_1 : clifford_algebra Q) :
⇑(⇑(clifford_algebra.change_form_aux Q B) ᾰ) ᾰ_1 = ⇑(clifford_algebra.ι Q) ᾰ * ᾰ_1 - ⇑(⇑clifford_algebra.contract_left (⇑(⇑bilin_form.to_lin B) ᾰ)) ᾰ_1
theorem
clifford_algebra.change_form_aux_change_form_aux
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(B : bilin_form R M)
(v : M)
(x : clifford_algebra Q) :
def
clifford_algebra.change_form
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q Q' : quadratic_form R M}
{B : bilin_form R M}
(h : B.to_quadratic_form = Q' - Q) :
Convert between two algebras of different quadratic form, sending vector to vectors, scalars to scalars, and adjusting products by a contraction term.
This is $\lambda_B$ from [bourbaki2007][] $9 Lemma 2.
Equations
theorem
clifford_algebra.change_form.zero_proof
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M} :
0.to_quadratic_form = Q - Q
Auxiliary lemma used as an argument to clifford_algebra.change_form
theorem
clifford_algebra.change_form.add_proof
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q Q' Q'' : quadratic_form R M}
{B B' : bilin_form R M}
(h : B.to_quadratic_form = Q' - Q)
(h' : B'.to_quadratic_form = Q'' - Q') :
(B + B').to_quadratic_form = Q'' - Q
Auxiliary lemma used as an argument to clifford_algebra.change_form
theorem
clifford_algebra.change_form.neg_proof
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q Q' : quadratic_form R M}
{B : bilin_form R M}
(h : B.to_quadratic_form = Q' - Q) :
(-B).to_quadratic_form = Q - Q'
Auxiliary lemma used as an argument to clifford_algebra.change_form
theorem
clifford_algebra.change_form.associated_neg_proof
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
[invertible 2] :
(⇑quadratic_form.associated (-Q)).to_quadratic_form = 0 - Q
@[simp]
theorem
clifford_algebra.change_form_algebra_map
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q Q' : quadratic_form R M}
{B : bilin_form R M}
(h : B.to_quadratic_form = Q' - Q)
(r : R) :
⇑(clifford_algebra.change_form h) (⇑(algebra_map R (clifford_algebra Q)) r) = ⇑(algebra_map R (clifford_algebra Q')) r
@[simp]
theorem
clifford_algebra.change_form_one
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q Q' : quadratic_form R M}
{B : bilin_form R M}
(h : B.to_quadratic_form = Q' - Q) :
⇑(clifford_algebra.change_form h) 1 = 1
@[simp]
theorem
clifford_algebra.change_form_ι
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q Q' : quadratic_form R M}
{B : bilin_form R M}
(h : B.to_quadratic_form = Q' - Q)
(m : M) :
⇑(clifford_algebra.change_form h) (⇑(clifford_algebra.ι Q) m) = ⇑(clifford_algebra.ι Q') m
theorem
clifford_algebra.change_form_ι_mul
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q Q' : quadratic_form R M}
{B : bilin_form R M}
(h : B.to_quadratic_form = Q' - Q)
(m : M)
(x : clifford_algebra Q) :
⇑(clifford_algebra.change_form h) (⇑(clifford_algebra.ι Q) m * x) = ⇑(clifford_algebra.ι Q') m * ⇑(clifford_algebra.change_form h) x - ⇑(⇑clifford_algebra.contract_left (⇑(⇑bilin_form.to_lin B) m)) (⇑(clifford_algebra.change_form h) x)
theorem
clifford_algebra.change_form_ι_mul_ι
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q Q' : quadratic_form R M}
{B : bilin_form R M}
(h : B.to_quadratic_form = Q' - Q)
(m₁ m₂ : M) :
⇑(clifford_algebra.change_form h) (⇑(clifford_algebra.ι Q) m₁ * ⇑(clifford_algebra.ι Q) m₂) = ⇑(clifford_algebra.ι Q') m₁ * ⇑(clifford_algebra.ι Q') m₂ - ⇑(algebra_map R (clifford_algebra Q')) (⇑B m₁ m₂)
theorem
clifford_algebra.change_form_contract_left
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q Q' : quadratic_form R M}
{B : bilin_form R M}
(h : B.to_quadratic_form = Q' - Q)
(d : module.dual R M)
(x : clifford_algebra Q) :
Theorem 23 of [grinberg_clifford_2016][]
theorem
clifford_algebra.change_form_self_apply
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(x : clifford_algebra Q) :
@[simp]
theorem
clifford_algebra.change_form_self
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M} :
theorem
clifford_algebra.change_form_change_form
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q Q' Q'' : quadratic_form R M}
{B B' : bilin_form R M}
(h : B.to_quadratic_form = Q' - Q)
(h' : B'.to_quadratic_form = Q'' - Q')
(x : clifford_algebra Q) :
⇑(clifford_algebra.change_form h') (⇑(clifford_algebra.change_form h) x) = ⇑(clifford_algebra.change_form _) x
This is [bourbaki2007][] $9 Lemma 3.
theorem
clifford_algebra.change_form_comp_change_form
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q Q' Q'' : quadratic_form R M}
{B B' : bilin_form R M}
(h : B.to_quadratic_form = Q' - Q)
(h' : B'.to_quadratic_form = Q'' - Q') :
@[simp]
theorem
clifford_algebra.change_form_equiv_apply
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q Q' : quadratic_form R M}
{B : bilin_form R M}
(h : B.to_quadratic_form = Q' - Q)
(ᾰ : clifford_algebra Q) :
def
clifford_algebra.change_form_equiv
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q Q' : quadratic_form R M}
{B : bilin_form R M}
(h : B.to_quadratic_form = Q' - Q) :
Any two algebras whose quadratic forms differ by a bilinear form are isomorphic as modules.
This is $\bar \lambda_B$ from [bourbaki2007][] $9 Proposition 3.
Equations
- clifford_algebra.change_form_equiv h = {to_fun := ⇑(clifford_algebra.change_form h), map_add' := _, map_smul' := _, inv_fun := ⇑(clifford_algebra.change_form _), left_inv := _, right_inv := _}
@[simp]
theorem
clifford_algebra.change_form_equiv_symm
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
{Q Q' : quadratic_form R M}
{B : bilin_form R M}
(h : B.to_quadratic_form = Q' - Q) :
@[simp]
def
clifford_algebra.equiv_exterior
{R : Type u1}
[comm_ring R]
{M : Type u2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
[invertible 2] :
clifford_algebra Q ≃ₗ[R] exterior_algebra R M
The module isomorphism to the exterior algebra.
Note that this holds more generally when Q is divisible by two, rather than only when 1 is
divisible by two; but that would be more awkward to use.