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 forms, 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

@[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) : ((contractLeftAux Q d) a) a✝ = d a • a✝.1 - (ι 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 fx : CliffordAlgebra Q) : ((contractLeftAux Q d) v) ((ι Q) v * x, ((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) : (contractRight x) d = reverse ((contractLeft d) (reverse x))

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) : (contractLeft d) ((ι Q) a * b) = d a • b - (ι Q) a * (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) : (contractRight (b * (ι Q) a)) d = d a • b - (contractRight b) d * (ι 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) : (contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r * b) = (algebraMap R (CliffordAlgebra Q)) r * (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) : (contractLeft d) (a * (algebraMap R (CliffordAlgebra Q)) r) = (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) : (contractRight ((algebraMap R (CliffordAlgebra Q)) r * b)) d = (algebraMap R (CliffordAlgebra Q)) r * (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) : (contractRight (a * (algebraMap R (CliffordAlgebra Q)) r)) d = (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) : (contractLeft d) ((ι 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) : (contractRight ((ι 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) : (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) : (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) : (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) : (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) : (contractLeft d) ((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) : (contractRight ((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 d' : Module.Dual R M) (x : CliffordAlgebra Q) : (contractLeft d) ((contractLeft d') x) = -(contractLeft d') ((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 d' : Module.Dual R M) (x : CliffordAlgebra Q) : (contractRight ((contractRight x) d)) d' = -(contractRight ((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

@[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) : ((changeFormAux Q B) a) a✝ = (ι Q) a * a✝ - (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) : ((changeFormAux Q B) v) (((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 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 forms, sending vectors 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} : 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 Q' Q'' : QuadraticForm R M} {B 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 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 Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q) (r : R) : (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 Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q) : (changeForm h) 1 = 1

@[simp]

theorem CliffordAlgebra.changeForm_ι {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q) (m : M) : (changeForm h) ((ι Q) m) = (ι Q') m

theorem CliffordAlgebra.changeForm_ι_mul {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q) (m : M) (x : CliffordAlgebra Q) : (changeForm h) ((ι Q) m * x) = (ι Q') m * (changeForm h) x - (contractLeft (B m)) ((changeForm h) x)

theorem CliffordAlgebra.changeForm_ι_mul_ι {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q) (m₁ m₂ : M) : (changeForm h) ((ι Q) m₁ * (ι Q) m₂) = (ι Q') m₁ * (ι 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 Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q) (d : Module.Dual R M) (x : CliffordAlgebra Q) : (changeForm h) ((contractLeft d) x) = (contractLeft d) ((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) : (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} : changeForm ⋯ = LinearMap.id

theorem CliffordAlgebra.changeForm_changeForm {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q Q' Q'' : QuadraticForm R M} {B B' : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q) (h' : LinearMap.BilinMap.toQuadraticMap B' = Q'' - Q') (x : CliffordAlgebra Q) : (changeForm h') ((changeForm h) x) = (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 Q' Q'' : QuadraticForm R M} {B B' : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q) (h' : LinearMap.BilinMap.toQuadraticMap B' = Q'' - Q') : changeForm h' ∘ₗ changeForm h = changeForm ⋯

def CliffordAlgebra.changeFormEquiv {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q 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.

@[simp]

theorem CliffordAlgebra.changeFormEquiv_apply {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q) (a : CliffordAlgebra Q) : (changeFormEquiv h) a = (changeForm h) a

@[simp]

theorem CliffordAlgebra.changeFormEquiv_symm {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q) : (changeFormEquiv h).symm = 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.

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.