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} [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.fst - ↑(CliffordAlgebra.ι Q) a * a.snd

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

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

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

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.instSMulCliffordAlgebra {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} : SMul R (CliffordAlgebra Q)

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

@[simp]

theorem CliffordAlgebra.changeFormAux_apply_apply {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (B : BilinForm R M) (a : M) (a : CliffordAlgebra Q) : ↑(↑(CliffordAlgebra.changeFormAux Q B) a) a = ↑(CliffordAlgebra.ι Q) a * a - ↑(↑CliffordAlgebra.contractLeft (↑(↑BilinForm.toLin B) a)) a

def CliffordAlgebra.changeFormAux {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (B : BilinForm R M) : M →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q

Auxiliary construction for CliffordAlgebra.changeForm

theorem CliffordAlgebra.changeFormAux_changeFormAux {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (B : BilinForm R M) (v : M) (x : CliffordAlgebra Q) : ↑(↑(CliffordAlgebra.changeFormAux Q B) v) (↑(↑(CliffordAlgebra.changeFormAux Q B) v) x) = (↑Q v - BilinForm.bilin 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 : BilinForm R M} (h : BilinForm.toQuadraticForm 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.

theorem CliffordAlgebra.changeForm.zero_proof {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} : BilinForm.toQuadraticForm 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 : BilinForm R M} {B' : BilinForm R M} (h : BilinForm.toQuadraticForm B = Q' - Q) (h' : BilinForm.toQuadraticForm B' = Q'' - Q') : BilinForm.toQuadraticForm (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 : BilinForm R M} (h : BilinForm.toQuadraticForm B = Q' - Q) : BilinForm.toQuadraticForm (-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] : BilinForm.toQuadraticForm (↑QuadraticForm.associated (-Q)) = 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 : BilinForm R M} (h : BilinForm.toQuadraticForm 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 : BilinForm R M} (h : BilinForm.toQuadraticForm 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 : BilinForm R M} (h : BilinForm.toQuadraticForm 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 : BilinForm R M} (h : BilinForm.toQuadraticForm B = Q' - Q) (m : M) (x : CliffordAlgebra Q) : ↑(CliffordAlgebra.changeForm h) (↑(CliffordAlgebra.ι Q) m * x) = ↑(CliffordAlgebra.ι Q') m * ↑(CliffordAlgebra.changeForm h) x - ↑(↑CliffordAlgebra.contractLeft (↑(↑BilinForm.toLin 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 : BilinForm R M} (h : BilinForm.toQuadraticForm 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')) (BilinForm.bilin 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 : BilinForm R M} (h : BilinForm.toQuadraticForm 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 (_ : BilinForm.toQuadraticForm 0 = Q - Q)) 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 (_ : BilinForm.toQuadraticForm 0 = Q - Q) = 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 : BilinForm R M} {B' : BilinForm R M} (h : BilinForm.toQuadraticForm B = Q' - Q) (h' : BilinForm.toQuadraticForm B' = Q'' - Q') (x : CliffordAlgebra Q) : ↑(CliffordAlgebra.changeForm h') (↑(CliffordAlgebra.changeForm h) x) = ↑(CliffordAlgebra.changeForm (_ : BilinForm.toQuadraticForm (B + B') = Q'' - Q)) 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 : BilinForm R M} {B' : BilinForm R M} (h : BilinForm.toQuadraticForm B = Q' - Q) (h' : BilinForm.toQuadraticForm B' = Q'' - Q') : LinearMap.comp (CliffordAlgebra.changeForm h') (CliffordAlgebra.changeForm h) = CliffordAlgebra.changeForm (_ : BilinForm.toQuadraticForm (B + 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 : BilinForm R M} (h : BilinForm.toQuadraticForm B = Q' - Q) (a : CliffordAlgebra Q) : ↑(CliffordAlgebra.changeFormEquiv h) a = ↑(CliffordAlgebra.changeForm h) a

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 : BilinForm R M} (h : BilinForm.toQuadraticForm 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.

@[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 : BilinForm R M} (h : BilinForm.toQuadraticForm B = Q' - Q) : LinearEquiv.symm (CliffordAlgebra.changeFormEquiv h) = CliffordAlgebra.changeFormEquiv (_ : BilinForm.toQuadraticForm (-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.