# Documentation

Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

# 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.fst - ↑() a * a.snd
def CliffordAlgebra.contractLeftAux {R : Type u1} [] {M : Type u2} [] [Module R M] (Q : ) (d : ) :

Auxiliary construction for CliffordAlgebra.contractLeft

Instances For
theorem CliffordAlgebra.contractLeftAux_contractLeftAux {R : Type u1} [] {M : Type u2} [] [Module R M] (Q : ) (d : ) (v : M) (x : ) (fx : ) :
↑(↑() v) (↑() v * x, ↑(↑() v) (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

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

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.instSMulCliffordAlgebra {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } :
SMul R ()
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 (↑(BilinForm.toLin B) a)) a
def CliffordAlgebra.changeFormAux {R : Type u1} [] {M : Type u2} [] [Module R M] (Q : ) (B : ) :

Auxiliary construction for CliffordAlgebra.changeForm

Instances For
theorem CliffordAlgebra.changeFormAux_changeFormAux {R : Type u1} [] {M : Type u2} [] [Module R M] (Q : ) (B : ) (v : M) (x : ) :
↑(↑() v) (↑(↑() v) x) = (Q v - ) x
def CliffordAlgebra.changeForm {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : = 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. 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 : = Q' - Q) (h' : = 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 : = Q' - Q) : = 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 : } [] : BilinForm.toQuadraticForm (QuadraticForm.associated (-Q)) = 0 - Q @[simp] theorem CliffordAlgebra.changeForm_algebraMap {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : = Q' - Q) (r : R) : ↑() (↑() r) = ↑() r @[simp] theorem CliffordAlgebra.changeForm_one {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : = Q' - Q) : = 1 @[simp] theorem CliffordAlgebra.changeForm_ι {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : = Q' - Q) (m : M) : ↑() (↑() m) = ↑() m theorem CliffordAlgebra.changeForm_ι_mul {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : = Q' - Q) (m : M) (x : ) : ↑() (↑() m * x) = ↑() m * - ↑(CliffordAlgebra.contractLeft (↑(BilinForm.toLin B) m)) () theorem CliffordAlgebra.changeForm_ι_mul_ι {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : = Q' - Q) (m₁ : M) (m₂ : M) : ↑() (↑() m₁ * ↑() m₂) = ↑() m₁ * ↑() m₂ - ↑() (BilinForm.bilin B m₁ m₂) theorem CliffordAlgebra.changeForm_contractLeft {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : = 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 : ) : @[simp] theorem CliffordAlgebra.changeForm_self {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } : CliffordAlgebra.changeForm (_ : ) = LinearMap.id theorem CliffordAlgebra.changeForm_changeForm {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {Q'' : } {B : } {B' : } (h : = Q' - Q) (h' : = Q'' - Q') (x : ) : ↑() () = ↑(CliffordAlgebra.changeForm (_ : BilinForm.toQuadraticForm (B + B') = 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 : = Q' - Q) (h' : = Q'' - Q') :
@[simp]
theorem CliffordAlgebra.changeFormEquiv_apply {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : = Q' - Q) (a : ) :
def CliffordAlgebra.changeFormEquiv {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : = 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.

Instances For
@[simp]
theorem CliffordAlgebra.changeFormEquiv_symm {R : Type u1} [] {M : Type u2} [] [Module R M] {Q : } {Q' : } {B : } (h : = 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.

Instances For