Contraction in Clifford Algebras #
This file contains some of the results from [Gri16].
The key result is CliffordAlgebra.equivExterior.
Main definitions #
CliffordAlgebra.contractLeft: contract a multivector by aModule.Dual R Mon the left.CliffordAlgebra.contractRight: contract a multivector by aModule.Dual R Mon the right.CliffordAlgebra.changeForm: convert between two algebras of different quadratic form, sending vectors to vectors. The difference of the quadratic forms must be a bilinear form.CliffordAlgebra.equivExterior: in characteristic not-two, theCliffordAlgebra Qis isomorphic as a module to the exterior algebra.
Implementation notes #
This file somewhat follows [Gri16], 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 [Gri16], instead directly constructing our objects using the universal property.
Note that [Gri16] concludes that its contents are not novel, and are in fact just a rehash of parts of [Bou07]; we should at some point consider swapping our references to refer to the latter.
Within this file, we use the local notation
x ⌊ dforcontractRight x dd ⌋ xforcontractLeft d x
@[simp]
theorem
CliffordAlgebra.contractLeftAux_apply_apply
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
(d : Module.Dual R M)
(a : M)
(a : CliffordAlgebra Q × CliffordAlgebra Q)
:
((CliffordAlgebra.contractLeftAux Q d) a✝) a = d a✝ • a.1 - (CliffordAlgebra.ι Q) a✝ * a.2
def
CliffordAlgebra.contractLeftAux
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
(d : Module.Dual R M)
:
M →ₗ[R] CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q
Auxiliary construction for CliffordAlgebra.contractLeft
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CliffordAlgebra.contractLeftAux_contractLeftAux
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
(d : Module.Dual R M)
(v : M)
(x : CliffordAlgebra Q)
(fx : CliffordAlgebra Q)
:
((CliffordAlgebra.contractLeftAux Q d) v)
((CliffordAlgebra.ι Q) v * x, ((CliffordAlgebra.contractLeftAux Q d) v) (x, fx)) = Q v • fx
def
CliffordAlgebra.contractLeft
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
Module.Dual R M →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra 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 contractLeft (Q.associated v) x.
This includes [Gri16] Theorem 10.75
Equations
- CliffordAlgebra.contractLeft = { toFun := fun (d : Module.Dual R M) => CliffordAlgebra.foldr' Q (CliffordAlgebra.contractLeftAux Q d) ⋯ 0, map_add' := ⋯, map_smul' := ⋯ }
Instances For
def
CliffordAlgebra.contractRight
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
CliffordAlgebra Q →ₗ[R] Module.Dual R M →ₗ[R] CliffordAlgebra 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 contractRight x (Q.associated v).
This includes [Gri16] Theorem 16.75
Equations
- CliffordAlgebra.contractRight = ((CliffordAlgebra.contractLeft.compr₂ CliffordAlgebra.reverse).compl₂ CliffordAlgebra.reverse).flip
Instances For
theorem
CliffordAlgebra.contractRight_eq
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(d : Module.Dual R M)
(x : CliffordAlgebra Q)
:
(CliffordAlgebra.contractRight x) d = CliffordAlgebra.reverse ((CliffordAlgebra.contractLeft d) (CliffordAlgebra.reverse x))
instance
CliffordAlgebra.instSMul
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
SMul R (CliffordAlgebra Q)
Equations
- CliffordAlgebra.instSMul = inferInstance
theorem
CliffordAlgebra.contractLeft_ι_mul
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(d : Module.Dual R M)
(a : M)
(b : CliffordAlgebra Q)
:
(CliffordAlgebra.contractLeft d) ((CliffordAlgebra.ι Q) a * b) = d a • b - (CliffordAlgebra.ι Q) a * (CliffordAlgebra.contractLeft d) b
This is [Gri16] Theorem 6
theorem
CliffordAlgebra.contractRight_mul_ι
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(d : Module.Dual R M)
(a : M)
(b : CliffordAlgebra Q)
:
(CliffordAlgebra.contractRight (b * (CliffordAlgebra.ι Q) a)) d = d a • b - (CliffordAlgebra.contractRight b) d * (CliffordAlgebra.ι Q) a
This is [Gri16] Theorem 12
theorem
CliffordAlgebra.contractLeft_algebraMap_mul
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(d : Module.Dual R M)
(r : R)
(b : CliffordAlgebra Q)
:
(CliffordAlgebra.contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r * b) = (algebraMap R (CliffordAlgebra Q)) r * (CliffordAlgebra.contractLeft d) b
theorem
CliffordAlgebra.contractLeft_mul_algebraMap
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(d : Module.Dual R M)
(a : CliffordAlgebra Q)
(r : R)
:
(CliffordAlgebra.contractLeft d) (a * (algebraMap R (CliffordAlgebra Q)) r) = (CliffordAlgebra.contractLeft d) a * (algebraMap R (CliffordAlgebra Q)) r
theorem
CliffordAlgebra.contractRight_algebraMap_mul
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(d : Module.Dual R M)
(r : R)
(b : CliffordAlgebra Q)
:
(CliffordAlgebra.contractRight ((algebraMap R (CliffordAlgebra Q)) r * b)) d = (algebraMap R (CliffordAlgebra Q)) r * (CliffordAlgebra.contractRight b) d
theorem
CliffordAlgebra.contractRight_mul_algebraMap
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(d : Module.Dual R M)
(a : CliffordAlgebra Q)
(r : R)
:
(CliffordAlgebra.contractRight (a * (algebraMap R (CliffordAlgebra Q)) r)) d = (CliffordAlgebra.contractRight a) d * (algebraMap R (CliffordAlgebra Q)) r
@[simp]
theorem
CliffordAlgebra.contractLeft_ι
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
(d : Module.Dual R M)
(x : M)
:
(CliffordAlgebra.contractLeft d) ((CliffordAlgebra.ι Q) x) = (algebraMap R (CliffordAlgebra Q)) (d x)
@[simp]
theorem
CliffordAlgebra.contractRight_ι
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
(d : Module.Dual R M)
(x : M)
:
(CliffordAlgebra.contractRight ((CliffordAlgebra.ι Q) x)) d = (algebraMap R (CliffordAlgebra Q)) (d x)
@[simp]
theorem
CliffordAlgebra.contractLeft_algebraMap
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
(d : Module.Dual R M)
(r : R)
:
(CliffordAlgebra.contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r) = 0
@[simp]
theorem
CliffordAlgebra.contractRight_algebraMap
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
(d : Module.Dual R M)
(r : R)
:
(CliffordAlgebra.contractRight ((algebraMap R (CliffordAlgebra Q)) r)) d = 0
@[simp]
theorem
CliffordAlgebra.contractLeft_one
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
(d : Module.Dual R M)
:
(CliffordAlgebra.contractLeft d) 1 = 0
@[simp]
theorem
CliffordAlgebra.contractRight_one
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
(d : Module.Dual R M)
:
(CliffordAlgebra.contractRight 1) d = 0
theorem
CliffordAlgebra.contractLeft_contractLeft
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(d : Module.Dual R M)
(x : CliffordAlgebra Q)
:
(CliffordAlgebra.contractLeft d) ((CliffordAlgebra.contractLeft d) x) = 0
This is [Gri16] Theorem 7
theorem
CliffordAlgebra.contractRight_contractRight
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(d : Module.Dual R M)
(x : CliffordAlgebra Q)
:
(CliffordAlgebra.contractRight ((CliffordAlgebra.contractRight x) d)) d = 0
This is [Gri16] Theorem 13
theorem
CliffordAlgebra.contractLeft_comm
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(d : Module.Dual R M)
(d' : Module.Dual R M)
(x : CliffordAlgebra Q)
:
This is [Gri16] Theorem 8
theorem
CliffordAlgebra.contractRight_comm
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(d : Module.Dual R M)
(d' : Module.Dual R M)
(x : CliffordAlgebra Q)
:
This is [Gri16] Theorem 14
@[simp]
theorem
CliffordAlgebra.changeFormAux_apply_apply
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
(B : LinearMap.BilinForm R M)
(a : M)
(a : CliffordAlgebra Q)
:
((CliffordAlgebra.changeFormAux Q B) a✝) a = (CliffordAlgebra.ι Q) a✝ * a - (CliffordAlgebra.contractLeft (B a✝)) a
def
CliffordAlgebra.changeFormAux
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
(B : LinearMap.BilinForm R M)
:
M →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q
Auxiliary construction for CliffordAlgebra.changeForm
Equations
- CliffordAlgebra.changeFormAux Q B = (Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ CliffordAlgebra.ι Q - CliffordAlgebra.contractLeft ∘ₗ B
Instances For
theorem
CliffordAlgebra.changeFormAux_changeFormAux
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
(B : LinearMap.BilinForm R M)
(v : M)
(x : CliffordAlgebra Q)
:
((CliffordAlgebra.changeFormAux Q B) v) (((CliffordAlgebra.changeFormAux Q B) v) x) = (Q v - (B v) v) • x
def
CliffordAlgebra.changeForm
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{Q' : QuadraticForm R M}
{B : LinearMap.BilinForm R M}
(h : LinearMap.BilinMap.toQuadraticMap B = 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 [Bou07] $9 Lemma 2.
Equations
- CliffordAlgebra.changeForm h = (CliffordAlgebra.foldr Q (CliffordAlgebra.changeFormAux Q' B) ⋯) 1
Instances For
theorem
CliffordAlgebra.changeForm.zero_proof
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
Auxiliary lemma used as an argument to CliffordAlgebra.changeForm
theorem
CliffordAlgebra.changeForm.add_proof
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{Q' : QuadraticForm R M}
{Q'' : QuadraticForm R M}
{B : LinearMap.BilinForm R M}
{B' : LinearMap.BilinForm R M}
(h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q)
(h' : LinearMap.BilinMap.toQuadraticMap B' = Q'' - Q')
:
LinearMap.BilinMap.toQuadraticMap (B + B') = Q'' - Q
Auxiliary lemma used as an argument to CliffordAlgebra.changeForm
theorem
CliffordAlgebra.changeForm.neg_proof
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{Q' : QuadraticForm R M}
{B : LinearMap.BilinForm R M}
(h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q)
:
LinearMap.BilinMap.toQuadraticMap (-B) = Q - Q'
Auxiliary lemma used as an argument to CliffordAlgebra.changeForm
theorem
CliffordAlgebra.changeForm.associated_neg_proof
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
[Invertible 2]
:
@[simp]
theorem
CliffordAlgebra.changeForm_algebraMap
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{Q' : QuadraticForm R M}
{B : LinearMap.BilinForm R M}
(h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q)
(r : R)
:
(CliffordAlgebra.changeForm h) ((algebraMap R (CliffordAlgebra Q)) r) = (algebraMap R (CliffordAlgebra Q')) r
@[simp]
theorem
CliffordAlgebra.changeForm_one
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{Q' : QuadraticForm R M}
{B : LinearMap.BilinForm R M}
(h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q)
:
(CliffordAlgebra.changeForm h) 1 = 1
@[simp]
theorem
CliffordAlgebra.changeForm_ι
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{Q' : QuadraticForm R M}
{B : LinearMap.BilinForm R M}
(h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q)
(m : M)
:
(CliffordAlgebra.changeForm h) ((CliffordAlgebra.ι Q) m) = (CliffordAlgebra.ι Q') m
theorem
CliffordAlgebra.changeForm_ι_mul
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{Q' : QuadraticForm R M}
{B : LinearMap.BilinForm R M}
(h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q)
(m : M)
(x : CliffordAlgebra Q)
:
(CliffordAlgebra.changeForm h) ((CliffordAlgebra.ι Q) m * x) = (CliffordAlgebra.ι Q') m * (CliffordAlgebra.changeForm h) x - (CliffordAlgebra.contractLeft (B m)) ((CliffordAlgebra.changeForm h) x)
theorem
CliffordAlgebra.changeForm_ι_mul_ι
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{Q' : QuadraticForm R M}
{B : LinearMap.BilinForm R M}
(h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q)
(m₁ : M)
(m₂ : M)
:
(CliffordAlgebra.changeForm h) ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂) = (CliffordAlgebra.ι Q') m₁ * (CliffordAlgebra.ι Q') m₂ - (algebraMap R (CliffordAlgebra Q')) ((B m₁) m₂)
theorem
CliffordAlgebra.changeForm_contractLeft
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{Q' : QuadraticForm R M}
{B : LinearMap.BilinForm R M}
(h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q)
(d : Module.Dual R M)
(x : CliffordAlgebra Q)
:
(CliffordAlgebra.changeForm h) ((CliffordAlgebra.contractLeft d) x) = (CliffordAlgebra.contractLeft d) ((CliffordAlgebra.changeForm h) x)
Theorem 23 of [Gri16]
theorem
CliffordAlgebra.changeForm_self_apply
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
(x : CliffordAlgebra Q)
:
(CliffordAlgebra.changeForm ⋯) x = x
@[simp]
theorem
CliffordAlgebra.changeForm_self
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
CliffordAlgebra.changeForm ⋯ = LinearMap.id
theorem
CliffordAlgebra.changeForm_changeForm
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{Q' : QuadraticForm R M}
{Q'' : QuadraticForm R M}
{B : LinearMap.BilinForm R M}
{B' : LinearMap.BilinForm R M}
(h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q)
(h' : LinearMap.BilinMap.toQuadraticMap B' = Q'' - Q')
(x : CliffordAlgebra Q)
:
(CliffordAlgebra.changeForm h') ((CliffordAlgebra.changeForm h) x) = (CliffordAlgebra.changeForm ⋯) x
This is [Bou07] $9 Lemma 3.
theorem
CliffordAlgebra.changeForm_comp_changeForm
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{Q' : QuadraticForm R M}
{Q'' : QuadraticForm R M}
{B : LinearMap.BilinForm R M}
{B' : LinearMap.BilinForm R M}
(h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q)
(h' : LinearMap.BilinMap.toQuadraticMap B' = Q'' - Q')
:
@[simp]
theorem
CliffordAlgebra.changeFormEquiv_apply
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{Q' : QuadraticForm R M}
{B : LinearMap.BilinForm R M}
(h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q)
(a : CliffordAlgebra Q)
:
def
CliffordAlgebra.changeFormEquiv
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{Q' : QuadraticForm R M}
{B : LinearMap.BilinForm R M}
(h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q)
:
Any two algebras whose quadratic forms differ by a bilinear form are isomorphic as modules.
This is $\bar \lambda_B$ from [Bou07] $9 Proposition 3.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CliffordAlgebra.changeFormEquiv_symm
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
{Q' : QuadraticForm R M}
{B : LinearMap.BilinForm R M}
(h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q)
:
def
CliffordAlgebra.equivExterior
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
[Invertible 2]
:
CliffordAlgebra Q ≃ₗ[R] ExteriorAlgebra 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.
Instances For
instance
CliffordAlgebra.instNontrivialOfInvertibleOfNat
{R : Type u1}
[CommRing R]
{M : Type u2}
[AddCommGroup M]
[Module R M]
(Q : QuadraticForm R M)
[Nontrivial R]
[Invertible 2]
:
A CliffordAlgebra over a nontrivial ring is nontrivial, in characteristic not two.
Equations
- ⋯ = ⋯