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
Instances for clifford_algebra.even_odd
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) :
theorem clifford_algebra.ι_mem_even_odd_one {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (m : M) :
theorem clifford_algebra.ι_mul_ι_mem_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) (m₁ m₂ : 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) =
theorem clifford_algebra.even_odd_induction {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) (n : zmod 2) {P : Π (x : clifford_algebra Q), x clifford_algebra.even_odd Q n → Prop} (hr : ∀ (v : clifford_algebra Q) (h : v (clifford_algebra.ι Q).range ^ n.val), P v _) (hadd : ∀ {x y : clifford_algebra Q} {hx : x clifford_algebra.even_odd Q n} {hy : y clifford_algebra.even_odd Q n}, P x hxP y hyP (x + y) _) (hιι_mul : ∀ (m₁ m₂ : M) {x : clifford_algebra Q} {hx : x clifford_algebra.even_odd Q n}, P x hxP ((clifford_algebra.ι Q) m₁ * (clifford_algebra.ι Q) m₂ * x) _) (x : clifford_algebra Q) (hx : x clifford_algebra.even_odd Q n) :
P x hx

To show a property is true on the even or odd part, it suffices to show it is true on the scalars or vectors (respectively), closed under addition, and under left-multiplication by a pair of vectors.

theorem clifford_algebra.even_induction {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) {P : Π (x : clifford_algebra Q), x clifford_algebra.even_odd Q 0 → Prop} (hr : ∀ (r : R), P ((algebra_map R (clifford_algebra Q)) r) _) (hadd : ∀ {x y : clifford_algebra Q} {hx : x clifford_algebra.even_odd Q 0} {hy : y clifford_algebra.even_odd Q 0}, P x hxP y hyP (x + y) _) (hιι_mul : ∀ (m₁ m₂ : M) {x : clifford_algebra Q} {hx : x clifford_algebra.even_odd Q 0}, P x hxP ((clifford_algebra.ι Q) m₁ * (clifford_algebra.ι Q) m₂ * x) _) (x : clifford_algebra Q) (hx : x clifford_algebra.even_odd Q 0) :
P x hx

To show a property is true on the even parts, it suffices to show it is true on the scalars, closed under addition, and under left-multiplication by a pair of vectors.

theorem clifford_algebra.odd_induction {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (Q : quadratic_form R M) {P : Π (x : clifford_algebra Q), x clifford_algebra.even_odd Q 1 → Prop} (hι : ∀ (v : M), P ((clifford_algebra.ι Q) v) _) (hadd : ∀ {x y : clifford_algebra Q} {hx : x clifford_algebra.even_odd Q 1} {hy : y clifford_algebra.even_odd Q 1}, P x hxP y hyP (x + y) _) (hιι_mul : ∀ (m₁ m₂ : M) {x : clifford_algebra Q} {hx : x clifford_algebra.even_odd Q 1}, P x hxP ((clifford_algebra.ι Q) m₁ * (clifford_algebra.ι Q) m₂ * x) _) (x : clifford_algebra Q) (hx : x clifford_algebra.even_odd Q 1) :
P x hx

To show a property is true on the odd parts, it suffices to show it is true on the vectors, closed under addition, and under left-multiplication by a pair of vectors.