# Documentation

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

def CliffordAlgebra.evenOdd {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (i : ZMod 2) :

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

Instances For
theorem CliffordAlgebra.one_le_evenOdd_zero {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :
theorem CliffordAlgebra.range_ι_le_evenOdd_one {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :
theorem CliffordAlgebra.ι_mem_evenOdd_one {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (m : M) :
↑() m
theorem CliffordAlgebra.ι_mul_ι_mem_evenOdd_zero {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (m₁ : M) (m₂ : M) :
↑() m₁ * ↑() m₂
theorem CliffordAlgebra.evenOdd_mul_le {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (i : ZMod 2) (j : ZMod 2) :
instance CliffordAlgebra.evenOdd.gradedMonoid {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :
def CliffordAlgebra.GradedAlgebra.ι {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :
M →ₗ[R] ⨁ (i : ZMod 2), { x // }

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

Instances For
theorem CliffordAlgebra.GradedAlgebra.ι_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (m : M) :
= ↑(DirectSum.of (fun i => { x // }) 1) { val := ↑() m, property := (_ : ↑() m ) }
theorem CliffordAlgebra.GradedAlgebra.ι_sq_scalar {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (m : M) :
= ↑(algebraMap R (⨁ (i : ZMod 2), { x // })) (Q m)
theorem CliffordAlgebra.GradedAlgebra.lift_ι_eq {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (i' : ZMod 2) (x' : { x // x }) :
↑(↑() { val := , property := (_ : ∀ (m : M), = ↑(algebraMap R (⨁ (i : ZMod 2), { x // })) (Q m)) }) x' = ↑(DirectSum.of (fun i => { x // }) i') x'
instance CliffordAlgebra.gradedAlgebra {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :

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

theorem CliffordAlgebra.iSup_ι_range_eq_top {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :
⨆ (i : ), =
theorem CliffordAlgebra.evenOdd_isCompl {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) :
theorem CliffordAlgebra.evenOdd_induction {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) (n : ZMod 2) {P : (x : ) → Prop} (hr : (v : ) → (h : ) → P v (_ : v ⨆ (i : { n // n = n }), )) (hadd : {x y : } → {hx : } → {hy : } → P x hxP y hyP (x + y) (_ : x + y )) (hιι_mul : (m₁ m₂ : M) → {x : } → {hx : } → P x hxP (↑() m₁ * ↑() m₂ * x) (_ : ↑() m₁ * ↑() m₂ * x )) (x : ) (hx : ) :
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 CliffordAlgebra.even_induction {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) {P : (x : ) → Prop} (hr : (r : R) → P (↑() r) (_ : ↑() r )) (hadd : {x y : } → {hx : } → {hy : } → P x hxP y hyP (x + y) (_ : x + y )) (hιι_mul : (m₁ m₂ : M) → {x : } → {hx : } → P x hxP (↑() m₁ * ↑() m₂ * x) (_ : ↑() m₁ * ↑() m₂ * x )) (x : ) (hx : ) :
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 CliffordAlgebra.odd_induction {R : Type u_1} {M : Type u_2} [] [] [Module R M] (Q : ) {P : (x : ) → Prop} (hι : (v : M) → P (↑() v) (_ : ↑() v )) (hadd : {x y : } → {hx : } → {hy : } → P x hxP y hyP (x + y) (_ : x + y )) (hιι_mul : (m₁ m₂ : M) → {x : } → {hx : } → P x hxP (↑() m₁ * ↑() m₂ * x) (_ : ↑() m₁ * ↑() m₂ * x )) (x : ) (hx : ) :
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.