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

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.

@[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

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 [grinberg_clifford_2016][] 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' := ⋯ }

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 [grinberg_clifford_2016][] Theorem 16.75

Equations

• CliffordAlgebra.contractRight = ((CliffordAlgebra.contractLeft.compr₂ CliffordAlgebra.reverse).compl₂ CliffordAlgebra.reverse).flip

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 [grinberg_clifford_2016][] 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 [grinberg_clifford_2016][] 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 [grinberg_clifford_2016][] 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 [grinberg_clifford_2016][] 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) : (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} [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) : (CliffordAlgebra.contractRight ((CliffordAlgebra.contractRight x) d)) d' = -(CliffordAlgebra.contractRight ((CliffordAlgebra.contractRight x) d')) d

This is [grinberg_clifford_2016][] Theorem 14

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

@[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

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) : CliffordAlgebra Q →ₗ[R] CliffordAlgebra 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

• CliffordAlgebra.changeForm h = (CliffordAlgebra.foldr Q (CliffordAlgebra.changeFormAux Q' B) ⋯) 1

theorem CliffordAlgebra.changeForm.zero_proof {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} : LinearMap.BilinMap.toQuadraticMap 0 = Q - Q

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] : (QuadraticMap.associated (-Q)).toQuadraticMap = 0 - Q

@[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 [grinberg_clifford_2016][]

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 [bourbaki2007][] $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') : CliffordAlgebra.changeForm h' ∘ₗ CliffordAlgebra.changeForm h = CliffordAlgebra.changeForm ⋯

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) : CliffordAlgebra Q ≃ₗ[R] CliffordAlgebra 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

• CliffordAlgebra.changeFormEquiv h = { toFun := ⇑(CliffordAlgebra.changeForm h), map_add' := ⋯, map_smul' := ⋯, invFun := ⇑(CliffordAlgebra.changeForm ⋯), left_inv := ⋯, right_inv := ⋯ }

@[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) : (CliffordAlgebra.changeFormEquiv h) a = (CliffordAlgebra.changeForm h) a

@[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) : (CliffordAlgebra.changeFormEquiv h).symm = CliffordAlgebra.changeFormEquiv ⋯

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.

Equations

• CliffordAlgebra.equivExterior Q = CliffordAlgebra.changeFormEquiv ⋯

instance CliffordAlgebra.instNontrivialOfInvertibleOfNat {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Nontrivial R] [Invertible 2] : Nontrivial (CliffordAlgebra Q)

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

Equations

• ⋯ = ⋯