# mathlib3documentation

linear_algebra.clifford_algebra.contraction

# Contraction in Clifford Algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main definitions #

• clifford_algebra.contract_left: contract a multivector by a module.dual R M on the left.
• clifford_algebra.contract_right: contract a multivector by a module.dual R M on the right.
• clifford_algebra.change_form: convert between two algebras of different quadratic form, sending vectors to vectors. The difference of the quadratic forms must be a bilinear form.
• clifford_algebra.equiv_exterior: in characteristic not-two, the clifford_algebra 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 contract_right x d
• d ⌋ x for contract_left d x
def clifford_algebra.contract_left_aux {R : Type u1} [comm_ring R] {M : Type u2} [ M] (Q : M) (d : M) :

Auxiliary construction for clifford_algebra.contract_left

Equations
@[simp]
theorem clifford_algebra.contract_left_aux_apply_apply {R : Type u1} [comm_ring R] {M : Type u2} [ M] (Q : M) (d : M) (ᾰ : M) (ᾰ_1 : × ) :
ᾰ) ᾰ_1 = d ᾰ ᾰ_1.fst - * ᾰ_1.snd
theorem clifford_algebra.contract_left_aux_contract_left_aux {R : Type u1} [comm_ring R] {M : Type u2} [ M] (Q : M) (d : M) (v : M) (x fx : clifford_algebra Q) :
v) ( v * x, v) (x, fx)) = Q v fx
def clifford_algebra.contract_left {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q : M} :

Contract an element of the clifford algebra with an element d : module.dual R M from the left.

Note that $v ⌋ x$ is spelt contract_left (Q.associated v) x.

This includes [grinberg_clifford_2016][] Theorem 10.75

Equations
def clifford_algebra.contract_right {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q : M} :

Contract an element of the clifford algebra with an element d : module.dual R M from the right.

Note that $x ⌊ v$ is spelt contract_right x (Q.associated v).

This includes [grinberg_clifford_2016][] Theorem 16.75

Equations
theorem clifford_algebra.contract_right_eq {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q : M} (d : M) (x : clifford_algebra Q) :
theorem clifford_algebra.contract_left_ι_mul {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q : M} (d : M) (a : M) (b : clifford_algebra Q) :
( a * b) = d a b -

This is [grinberg_clifford_2016][] Theorem 6

theorem clifford_algebra.contract_right_mul_ι {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q : M} (d : M) (a : M) (b : clifford_algebra Q) :

This is [grinberg_clifford_2016][] Theorem 12

theorem clifford_algebra.contract_left_algebra_map_mul {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q : M} (d : M) (r : R) (b : clifford_algebra Q) :
theorem clifford_algebra.contract_left_mul_algebra_map {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q : M} (d : M) (a : clifford_algebra Q) (r : R) :
@[simp]
theorem clifford_algebra.contract_left_ι {R : Type u1} [comm_ring R] {M : Type u2} [ M] (Q : M) (d : M) (x : M) :
@[simp]
theorem clifford_algebra.contract_right_ι {R : Type u1} [comm_ring R] {M : Type u2} [ M] (Q : M) (d : M) (x : M) :
@[simp]
theorem clifford_algebra.contract_left_algebra_map {R : Type u1} [comm_ring R] {M : Type u2} [ M] (Q : M) (d : M) (r : R) :
( (clifford_algebra Q)) r) = 0
@[simp]
theorem clifford_algebra.contract_right_algebra_map {R : Type u1} [comm_ring R] {M : Type u2} [ M] (Q : M) (d : M) (r : R) :
@[simp]
theorem clifford_algebra.contract_left_one {R : Type u1} [comm_ring R] {M : Type u2} [ M] (Q : M) (d : M) :
@[simp]
theorem clifford_algebra.contract_right_one {R : Type u1} [comm_ring R] {M : Type u2} [ M] (Q : M) (d : M) :
theorem clifford_algebra.contract_left_contract_left {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q : M} (d : M) (x : clifford_algebra Q) :

This is [grinberg_clifford_2016][] Theorem 7

theorem clifford_algebra.contract_right_contract_right {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q : M} (d : M) (x : clifford_algebra Q) :

This is [grinberg_clifford_2016][] Theorem 13

theorem clifford_algebra.contract_left_comm {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q : M} (d d' : M) (x : clifford_algebra Q) :

This is [grinberg_clifford_2016][] Theorem 8

theorem clifford_algebra.contract_right_comm {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q : M} (d d' : M) (x : clifford_algebra Q) :

This is [grinberg_clifford_2016][] Theorem 14

def clifford_algebra.change_form_aux {R : Type u1} [comm_ring R] {M : Type u2} [ M] (Q : M) (B : M) :

Auxiliary construction for clifford_algebra.change_form

Equations
@[simp]
theorem clifford_algebra.change_form_aux_apply_apply {R : Type u1} [comm_ring R] {M : Type u2} [ M] (Q : M) (B : M) (ᾰ : M) (ᾰ_1 : clifford_algebra Q) :
ᾰ) ᾰ_1 = * ᾰ_1 - ᾰ_1
theorem clifford_algebra.change_form_aux_change_form_aux {R : Type u1} [comm_ring R] {M : Type u2} [ M] (Q : M) (B : M) (v : M) (x : clifford_algebra Q) :
v) ( v) x) = (Q v - B v v) x
def clifford_algebra.change_form {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q Q' : M} {B : M} (h : B.to_quadratic_form = 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 theorem clifford_algebra.change_form.zero_proof {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q : M} : Auxiliary lemma used as an argument to clifford_algebra.change_form theorem clifford_algebra.change_form.add_proof {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q Q' Q'' : M} {B B' : M} (h : B.to_quadratic_form = Q' - Q) (h' : B'.to_quadratic_form = Q'' - Q') : (B + B').to_quadratic_form = Q'' - Q Auxiliary lemma used as an argument to clifford_algebra.change_form theorem clifford_algebra.change_form.neg_proof {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q Q' : M} {B : M} (h : B.to_quadratic_form = Q' - Q) : Auxiliary lemma used as an argument to clifford_algebra.change_form theorem clifford_algebra.change_form.associated_neg_proof {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q : M} [invertible 2] : @[simp] theorem clifford_algebra.change_form_algebra_map {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q Q' : M} {B : M} (h : B.to_quadratic_form = Q' - Q) (r : R) : @[simp] theorem clifford_algebra.change_form_one {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q Q' : M} {B : M} (h : B.to_quadratic_form = Q' - Q) : @[simp] theorem clifford_algebra.change_form_ι {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q Q' : M} {B : M} (h : B.to_quadratic_form = Q' - Q) (m : M) : ( m) = m theorem clifford_algebra.change_form_ι_mul {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q Q' : M} {B : M} (h : B.to_quadratic_form = Q' - Q) (m : M) (x : clifford_algebra Q) : ( m * x) = m * - theorem clifford_algebra.change_form_ι_mul_ι {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q Q' : M} {B : M} (h : B.to_quadratic_form = Q' - Q) (m₁ m₂ : M) : ( m₁ * m₂) = m₁ * m₂ - (clifford_algebra Q')) (B m₁ m₂) theorem clifford_algebra.change_form_contract_left {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q Q' : M} {B : M} (h : B.to_quadratic_form = Q' - Q) (d : M) (x : clifford_algebra Q) : Theorem 23 of [grinberg_clifford_2016][] theorem clifford_algebra.change_form_self_apply {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q : M} (x : clifford_algebra Q) : @[simp] theorem clifford_algebra.change_form_self {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q : M} : theorem clifford_algebra.change_form_change_form {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q Q' Q'' : M} {B B' : M} (h : B.to_quadratic_form = Q' - Q) (h' : B'.to_quadratic_form = Q'' - Q') (x : clifford_algebra Q) : This is [bourbaki2007][]$9 Lemma 3.

theorem clifford_algebra.change_form_comp_change_form {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q Q' Q'' : M} {B B' : M} (h : B.to_quadratic_form = Q' - Q) (h' : B'.to_quadratic_form = Q'' - Q') :
@[simp]
theorem clifford_algebra.change_form_equiv_apply {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q Q' : M} {B : M} (h : B.to_quadratic_form = Q' - Q) (ᾰ : clifford_algebra Q) :
def clifford_algebra.change_form_equiv {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q Q' : M} {B : M} (h : B.to_quadratic_form = 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
@[simp]
theorem clifford_algebra.change_form_equiv_symm {R : Type u1} [comm_ring R] {M : Type u2} [ M] {Q Q' : M} {B : M} (h : B.to_quadratic_form = Q' - Q) :
@[simp]
def clifford_algebra.equiv_exterior {R : Type u1} [comm_ring R] {M : Type u2} [ M] (Q : M) [invertible 2] :

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