mathlib3 documentation

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 #

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

@[simp]
theorem clifford_algebra.contract_left_aux_apply_apply {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] (Q : quadratic_form R M) (d : module.dual R M) (ᾰ : M) (ᾰ_1 : clifford_algebra Q × clifford_algebra 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 contract_left (Q.associated v) x.

This includes [grinberg_clifford_2016][] Theorem 10.75

Equations

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

This is [grinberg_clifford_2016][] Theorem 6

This is [grinberg_clifford_2016][] Theorem 12

This is [grinberg_clifford_2016][] Theorem 7

This is [grinberg_clifford_2016][] Theorem 13

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

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} [add_comm_group M] [module R M] {Q Q' Q'' : quadratic_form R M} {B B' : bilin_form R 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} [add_comm_group M] [module R M] {Q Q' : quadratic_form R M} {B : bilin_form R M} (h : B.to_quadratic_form = Q' - Q) :

Auxiliary lemma used as an argument to clifford_algebra.change_form

@[simp]
theorem clifford_algebra.change_form_one {R : Type u1} [comm_ring R] {M : Type u2} [add_comm_group M] [module R M] {Q Q' : quadratic_form R M} {B : bilin_form R M} (h : B.to_quadratic_form = Q' - Q) :
@[simp]

This is [bourbaki2007][] $9 Lemma 3.

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]

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