mathlib3documentation

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

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] [ M] (Q : 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] [ M] (Q : M) :
theorem clifford_algebra.range_ι_le_even_odd_one {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) :
theorem clifford_algebra.ι_mem_even_odd_one {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (m : M) :
theorem clifford_algebra.ι_mul_ι_mem_even_odd_zero {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (m₁ m₂ : M) :
m₁ * m₂
theorem clifford_algebra.even_odd_mul_le {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (i j : zmod 2) :
@[protected, instance]
def clifford_algebra.even_odd.graded_monoid {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) :
def clifford_algebra.graded_algebra.ι {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) :
M →ₗ[R] direct_sum (zmod 2) (λ (i : zmod 2),

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
theorem clifford_algebra.graded_algebra.ι_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (m : M) :
= (direct_sum.of (λ (i : zmod 2), 1) m, _⟩
theorem clifford_algebra.graded_algebra.ι_sq_scalar {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (m : M) :
= (direct_sum (zmod 2) (λ (i : zmod 2), i)))) (Q m)
theorem clifford_algebra.graded_algebra.lift_ι_eq {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (i' : zmod 2) (x' : ) :
x' = (direct_sum.of (λ (i : zmod 2), i') x'
@[protected, instance]
def clifford_algebra.graded_algebra {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) :

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] [ M] (Q : M) :
( (i : ), =
theorem clifford_algebra.even_odd_is_compl {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) :
theorem clifford_algebra.even_odd_induction {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (Q : M) (n : zmod 2) {P : Π (x : , Prop} (hr : (v : (h : v , P v _) (hadd : {x y : {hx : {hy : , P x hx P y hy P (x + y) _) (hιι_mul : (m₁ m₂ : M) {x : {hx : , P x hx P ( m₁ * m₂ * x) _) (x : clifford_algebra Q) (hx : x ) :
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] [ M] (Q : M) {P : Π (x : , Prop} (hr : (r : R), P ( (clifford_algebra Q)) r) _) (hadd : {x y : {hx : {hy : , P x hx P y hy P (x + y) _) (hιι_mul : (m₁ m₂ : M) {x : {hx : , P x hx P ( m₁ * m₂ * x) _) (x : clifford_algebra Q) (hx : x ) :
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] [ M] (Q : M) {P : Π (x : , Prop} (hι : (v : M), P ( v) _) (hadd : {x y : {hx : {hy : , P x hx P y hy P (x + y) _) (hιι_mul : (m₁ m₂ : M) {x : {hx : , P x hx P ( m₁ * m₂ * x) _) (x : clifford_algebra Q) (hx : x ) :
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.