mathlib documentation

linear_algebra.clifford_algebra.grading

Results about the grading structure of the clifford algebra #

The main result is clifford_algebra.graded_algebra, which says that the clifford algebra is a ℤ₂-graded algebra (or "superalgebra").

def clifford_algebra.even_odd {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (i : zmod 2) :

The even or odd submodule, defined as the supremum of the even or odd powers of (ι Q).range. even_odd 0 is the even submodule, and even_odd 1 is the odd submodule.

Equations
theorem clifford_algebra.one_le_even_odd_zero {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) :
@[protected, instance]
def clifford_algebra.graded_algebra.ι {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) :

A version of clifford_algebra.ι that maps directly into the graded structure. This is primarily an auxiliary construction used to provide clifford_algebra.graded_algebra.

Equations
@[protected, instance]

The clifford algebra is graded by the even and odd parts.

Equations
theorem clifford_algebra.supr_ι_range_eq_top {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) :
(⨆ (i : ), (clifford_algebra.ι Q).range ^ i) =