# Contraction in Clifford Algebras #

This file contains some of the results from [grinberg_clifford_2016][]. The key result is CliffordAlgebra.equivExterior.

## Main definitions #

• CliffordAlgebra.contractLeft: contract a multivector by a Module.Dual R M on the left.
• CliffordAlgebra.contractRight: contract a multivector by a Module.Dual R M on 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, the CliffordAlgebra Q is 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 ⌊ d for contractRight x d
• d ⌋ x for contractLeft d x
@[simp]
theorem CliffordAlgebra.contractLeftAux_apply_apply {R : Type u1} [] {M : Type u2} [] [Module R M] (Q : ) (d : ) (a : M) (a : ) :
( a✝) a = d a✝ a.1 - a✝ * a.2
def CliffordAlgebra.contractLeftAux {R : Type u1} [] {M : Type u2} [] [Module R M] (Q : ) (d : ) :

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} [] {M : Type u2} [] [Module R M] (Q : ) (d : ) (v : M) (x : ) (fx : ) :
() ( v * x, () (x, fx)) = Q v fx
def CliffordAlgebra.contractLeft {R : Type u1} [] {M : Type u2} [] [Module R M] {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 [grinberg_clifford_2016][] Theorem 10.75

Equations
• CliffordAlgebra.contractLeft = { toFun := fun (d : ) => , map_add' := , map_smul' := }
Instances For
def CliffordAlgebra.contractRight {R : Type u1} [] {M : Type u2} [] [Module R M] {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 [grinberg_clifford_2016][] Theorem 16.75

Equations
• CliffordAlgebra.contractRight = ((CliffordAlgebra.contractLeft.compr₂ CliffordAlgebra.reverse).compl₂ CliffordAlgebra.reverse).flip
Instances For
theorem CliffordAlgebra.contractRight_eq {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } (d : ) (x : ) :
(CliffordAlgebra.contractRight x) d = CliffordAlgebra.reverse ((CliffordAlgebra.contractLeft d) (CliffordAlgebra.reverse x))
instance CliffordAlgebra.instSMul {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } :
SMul R ()
Equations
• CliffordAlgebra.instSMul = inferInstance
theorem CliffordAlgebra.contractLeft_ι_mul {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } (d : ) (a : M) (b : ) :
(CliffordAlgebra.contractLeft d) ( a * b) = d a b - a * (CliffordAlgebra.contractLeft d) b

This is [grinberg_clifford_2016][] Theorem 6

theorem CliffordAlgebra.contractRight_mul_ι {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } (d : ) (a : M) (b : ) :
(CliffordAlgebra.contractRight (b * a)) d = d a b - (CliffordAlgebra.contractRight b) d * a

This is [grinberg_clifford_2016][] Theorem 12

theorem CliffordAlgebra.contractLeft_algebraMap_mul {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } (d : ) (r : R) (b : ) :
(CliffordAlgebra.contractLeft d) (() r * b) = () r * (CliffordAlgebra.contractLeft d) b
theorem CliffordAlgebra.contractLeft_mul_algebraMap {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } (d : ) (a : ) (r : R) :
(CliffordAlgebra.contractLeft d) (a * () r) = (CliffordAlgebra.contractLeft d) a * () r
theorem CliffordAlgebra.contractRight_algebraMap_mul {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } (d : ) (r : R) (b : ) :
(CliffordAlgebra.contractRight (() r * b)) d = () r * (CliffordAlgebra.contractRight b) d
theorem CliffordAlgebra.contractRight_mul_algebraMap {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } (d : ) (a : ) (r : R) :
(CliffordAlgebra.contractRight (a * () r)) d = (CliffordAlgebra.contractRight a) d * () r
@[simp]
theorem CliffordAlgebra.contractLeft_ι {R : Type u1} [] {M : Type u2} [] [Module R M] (Q : ) (d : ) (x : M) :
(CliffordAlgebra.contractLeft d) ( x) = () (d x)
@[simp]
theorem CliffordAlgebra.contractRight_ι {R : Type u1} [] {M : Type u2} [] [Module R M] (Q : ) (d : ) (x : M) :
(CliffordAlgebra.contractRight ( x)) d = () (d x)
@[simp]
theorem CliffordAlgebra.contractLeft_algebraMap {R : Type u1} [] {M : Type u2} [] [Module R M] (Q : ) (d : ) (r : R) :
(CliffordAlgebra.contractLeft d) (() r) = 0
@[simp]
theorem CliffordAlgebra.contractRight_algebraMap {R : Type u1} [] {M : Type u2} [] [Module R M] (Q : ) (d : ) (r : R) :
(CliffordAlgebra.contractRight (() r)) d = 0
@[simp]
theorem CliffordAlgebra.contractLeft_one {R : Type u1} [] {M : Type u2} [] [Module R M] (Q : ) (d : ) :
(CliffordAlgebra.contractLeft d) 1 = 0
@[simp]
theorem CliffordAlgebra.contractRight_one {R : Type u1} [] {M : Type u2} [] [Module R M] (Q : ) (d : ) :
(CliffordAlgebra.contractRight 1) d = 0
theorem CliffordAlgebra.contractLeft_contractLeft {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } (d : ) (x : ) :
(CliffordAlgebra.contractLeft d) ((CliffordAlgebra.contractLeft d) x) = 0

This is [grinberg_clifford_2016][] Theorem 7

theorem CliffordAlgebra.contractRight_contractRight {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } (d : ) (x : ) :
(CliffordAlgebra.contractRight ((CliffordAlgebra.contractRight x) d)) d = 0

This is [grinberg_clifford_2016][] Theorem 13

theorem CliffordAlgebra.contractLeft_comm {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } (d : ) (d' : ) (x : ) :
(CliffordAlgebra.contractLeft d) ((CliffordAlgebra.contractLeft d') x) = -(CliffordAlgebra.contractLeft d') ((CliffordAlgebra.contractLeft d) x)

This is [grinberg_clifford_2016][] Theorem 8

theorem CliffordAlgebra.contractRight_comm {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } (d : ) (d' : ) (x : ) :
(CliffordAlgebra.contractRight ((CliffordAlgebra.contractRight x) d)) d' = -(CliffordAlgebra.contractRight ((CliffordAlgebra.contractRight x) d')) d

This is [grinberg_clifford_2016][] Theorem 14

@[simp]
theorem CliffordAlgebra.changeFormAux_apply_apply {R : Type u1} [] {M : Type u2} [] [Module R M] (Q : ) (B : ) (a : M) (a : ) :
( a✝) a = a✝ * a - (CliffordAlgebra.contractLeft (B a✝)) a
def CliffordAlgebra.changeFormAux {R : Type u1} [] {M : Type u2} [] [Module R M] (Q : ) (B : ) :

Auxiliary construction for CliffordAlgebra.changeForm

Equations
• = ().toLinearMap ∘ₗ - CliffordAlgebra.contractLeft ∘ₗ B
Instances For
theorem CliffordAlgebra.changeFormAux_changeFormAux {R : Type u1} [] {M : Type u2} [] [Module R M] (Q : ) (B : ) (v : M) (x : ) :
() (() x) = (Q v - (B v) v) x
def CliffordAlgebra.changeForm {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : B.toQuadraticForm = 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 Instances For theorem CliffordAlgebra.changeForm.zero_proof {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } : Auxiliary lemma used as an argument to CliffordAlgebra.changeForm theorem CliffordAlgebra.changeForm.add_proof {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {Q'' : } {B : } {B' : } (h : B.toQuadraticForm = Q' - Q) (h' : B'.toQuadraticForm = Q'' - Q') : (B + B').toQuadraticForm = Q'' - Q Auxiliary lemma used as an argument to CliffordAlgebra.changeForm theorem CliffordAlgebra.changeForm.neg_proof {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : B.toQuadraticForm = Q' - Q) : (-B).toQuadraticForm = Q - Q' Auxiliary lemma used as an argument to CliffordAlgebra.changeForm theorem CliffordAlgebra.changeForm.associated_neg_proof {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } [] : (QuadraticForm.associated (-Q)).toQuadraticForm = 0 - Q @[simp] theorem CliffordAlgebra.changeForm_algebraMap {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : B.toQuadraticForm = Q' - Q) (r : R) : (() r) = () r @[simp] theorem CliffordAlgebra.changeForm_one {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : B.toQuadraticForm = Q' - Q) : = 1 @[simp] theorem CliffordAlgebra.changeForm_ι {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : B.toQuadraticForm = Q' - Q) (m : M) : ( m) = () m theorem CliffordAlgebra.changeForm_ι_mul {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : B.toQuadraticForm = Q' - Q) (m : M) (x : ) : ( m * x) = () m * - (CliffordAlgebra.contractLeft (B m)) () theorem CliffordAlgebra.changeForm_ι_mul_ι {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : B.toQuadraticForm = Q' - Q) (m₁ : M) (m₂ : M) : ( m₁ * m₂) = () m₁ * () m₂ - () ((B m₁) m₂) theorem CliffordAlgebra.changeForm_contractLeft {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : B.toQuadraticForm = Q' - Q) (d : ) (x : ) : ((CliffordAlgebra.contractLeft d) x) = (CliffordAlgebra.contractLeft d) () Theorem 23 of [grinberg_clifford_2016][] theorem CliffordAlgebra.changeForm_self_apply {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } (x : ) : = x @[simp] theorem CliffordAlgebra.changeForm_self {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } : = LinearMap.id theorem CliffordAlgebra.changeForm_changeForm {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {Q'' : } {B : } {B' : } (h : B.toQuadraticForm = Q' - Q) (h' : B'.toQuadraticForm = Q'' - Q') (x : ) : () = This is [bourbaki2007][]$9 Lemma 3.

theorem CliffordAlgebra.changeForm_comp_changeForm {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {Q'' : } {B : } {B' : } (h : B.toQuadraticForm = Q' - Q) (h' : B'.toQuadraticForm = Q'' - Q') :
@[simp]
theorem CliffordAlgebra.changeFormEquiv_apply {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : B.toQuadraticForm = Q' - Q) (a : ) :
def CliffordAlgebra.changeFormEquiv {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : B.toQuadraticForm = 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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CliffordAlgebra.changeFormEquiv_symm {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : B.toQuadraticForm = Q' - Q) :
def CliffordAlgebra.equivExterior {R : Type u1} [] {M : Type u2} [] [Module R M] (Q : ) [] :

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.

Equations
Instances For
instance CliffordAlgebra.instNontrivialOfInvertibleOfNat {R : Type u1} [] {M : Type u2} [] [Module R M] (Q : ) [] [] :

A CliffordAlgebra over a nontrivial ring is nontrivial, in characteristic not two.

Equations
• =