Results about the grading structure of the clifford algebra

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} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (i : ZMod 2) : Submodule R (CliffordAlgebra Q)

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.

Equations

• CliffordAlgebra.evenOdd Q i = ⨆ (j : { n : ℕ // ↑n = i }), LinearMap.range (CliffordAlgebra.ι Q) ^ ↑j

theorem CliffordAlgebra.one_le_evenOdd_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : 1 ≤ CliffordAlgebra.evenOdd Q 0

theorem CliffordAlgebra.range_ι_le_evenOdd_one {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : LinearMap.range (CliffordAlgebra.ι Q) ≤ CliffordAlgebra.evenOdd Q 1

theorem CliffordAlgebra.ι_mem_evenOdd_one {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M) : (CliffordAlgebra.ι Q) m ∈ CliffordAlgebra.evenOdd Q 1

theorem CliffordAlgebra.ι_mul_ι_mem_evenOdd_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m₁ : M) (m₂ : M) : (CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ ∈ CliffordAlgebra.evenOdd Q 0

theorem CliffordAlgebra.evenOdd_mul_le {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (i : ZMod 2) (j : ZMod 2) : CliffordAlgebra.evenOdd Q i * CliffordAlgebra.evenOdd Q j ≤ CliffordAlgebra.evenOdd Q (i + j)

instance CliffordAlgebra.evenOdd.gradedMonoid {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : SetLike.GradedMonoid (CliffordAlgebra.evenOdd Q)

Equations

• (_ : SetLike.GradedMonoid (CliffordAlgebra.evenOdd Q)) = (_ : SetLike.GradedMonoid (CliffordAlgebra.evenOdd Q))

def CliffordAlgebra.GradedAlgebra.ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : M →ₗ[R] DirectSum (ZMod 2) fun (i : ZMod 2) => ↥(CliffordAlgebra.evenOdd Q i)

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

Equations

• One or more equations did not get rendered due to their size.

theorem CliffordAlgebra.GradedAlgebra.ι_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M) : (CliffordAlgebra.GradedAlgebra.ι Q) m = (DirectSum.of (fun (i : ZMod 2) => ↥(CliffordAlgebra.evenOdd Q i)) 1) { val := (CliffordAlgebra.ι Q) m, property := (_ : (CliffordAlgebra.ι Q) m ∈ CliffordAlgebra.evenOdd Q 1) }

theorem CliffordAlgebra.GradedAlgebra.ι_sq_scalar {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M) : (CliffordAlgebra.GradedAlgebra.ι Q) m * (CliffordAlgebra.GradedAlgebra.ι Q) m = (algebraMap R (DirectSum (ZMod 2) fun (i : ZMod 2) => ↥(CliffordAlgebra.evenOdd Q i))) (Q m)

theorem CliffordAlgebra.GradedAlgebra.lift_ι_eq {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (i' : ZMod 2) (x' : ↥(CliffordAlgebra.evenOdd Q i')) : ((CliffordAlgebra.lift Q) { val := CliffordAlgebra.GradedAlgebra.ι Q, property := (_ : ∀ (m : M), (CliffordAlgebra.GradedAlgebra.ι Q) m * (CliffordAlgebra.GradedAlgebra.ι Q) m = (algebraMap R (DirectSum (ZMod 2) fun (i : ZMod 2) => ↥(CliffordAlgebra.evenOdd Q i))) (Q m)) }) ↑x' = (DirectSum.of (fun (i : ZMod 2) => ↥(CliffordAlgebra.evenOdd Q i)) i') x'

instance CliffordAlgebra.gradedAlgebra {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : GradedAlgebra (CliffordAlgebra.evenOdd Q)

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

Equations

• One or more equations did not get rendered due to their size.

theorem CliffordAlgebra.iSup_ι_range_eq_top {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : ⨆ (i : ℕ), LinearMap.range (CliffordAlgebra.ι Q) ^ i = ⊤

theorem CliffordAlgebra.evenOdd_isCompl {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : IsCompl (CliffordAlgebra.evenOdd Q 0) (CliffordAlgebra.evenOdd Q 1)

theorem CliffordAlgebra.evenOdd_induction {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (n : ZMod 2) {P : (x : CliffordAlgebra Q) → x ∈ CliffordAlgebra.evenOdd Q n → Prop} (hr : ∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (CliffordAlgebra.ι Q) ^ ZMod.val n), P v (_ : v ∈ ⨆ (i : { n_1 : ℕ // ↑n_1 = n }), LinearMap.range (CliffordAlgebra.ι Q) ^ ↑i)) (hadd : ∀ {x y : CliffordAlgebra Q} {hx : x ∈ CliffordAlgebra.evenOdd Q n} {hy : y ∈ CliffordAlgebra.evenOdd Q n}, P x hx → P y hy → P (x + y) (_ : x + y ∈ CliffordAlgebra.evenOdd Q n)) (hιι_mul : ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ CliffordAlgebra.evenOdd Q n}, P x hx → P ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) (_ : (CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x ∈ CliffordAlgebra.evenOdd Q n)) (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd 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 CliffordAlgebra.even_induction {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {P : (x : CliffordAlgebra Q) → x ∈ CliffordAlgebra.evenOdd Q 0 → Prop} (hr : ∀ (r : R), P ((algebraMap R (CliffordAlgebra Q)) r) (_ : (algebraMap R (CliffordAlgebra Q)) r ∈ CliffordAlgebra.evenOdd Q 0)) (hadd : ∀ {x y : CliffordAlgebra Q} {hx : x ∈ CliffordAlgebra.evenOdd Q 0} {hy : y ∈ CliffordAlgebra.evenOdd Q 0}, P x hx → P y hy → P (x + y) (_ : x + y ∈ CliffordAlgebra.evenOdd Q 0)) (hιι_mul : ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ CliffordAlgebra.evenOdd Q 0}, P x hx → P ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) (_ : (CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x ∈ CliffordAlgebra.evenOdd Q 0)) (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd 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 CliffordAlgebra.odd_induction {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {P : (x : CliffordAlgebra Q) → x ∈ CliffordAlgebra.evenOdd Q 1 → Prop} (hι : ∀ (v : M), P ((CliffordAlgebra.ι Q) v) (_ : (CliffordAlgebra.ι Q) v ∈ CliffordAlgebra.evenOdd Q 1)) (hadd : ∀ {x y : CliffordAlgebra Q} {hx : x ∈ CliffordAlgebra.evenOdd Q 1} {hy : y ∈ CliffordAlgebra.evenOdd Q 1}, P x hx → P y hy → P (x + y) (_ : x + y ∈ CliffordAlgebra.evenOdd Q 1)) (hιι_mul : ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ CliffordAlgebra.evenOdd Q 1}, P x hx → P ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) (_ : (CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x ∈ CliffordAlgebra.evenOdd Q 1)) (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd 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.