Documentation

Mathlib.LinearAlgebra.CliffordAlgebra.Grading

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) :

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.ι_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) :
    def CliffordAlgebra.GradedAlgebra.ι {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :
    M →ₗ[R] ⨁ (i : ZMod 2), { x // x 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.

    Instances For
      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 => { x // x 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 (⨁ (i : ZMod 2), { x // x 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' : { x // 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 (⨁ (i : ZMod 2), { x // x CliffordAlgebra.evenOdd Q i })) (Q m)) }) x' = ↑(DirectSum.of (fun i => { x // x CliffordAlgebra.evenOdd Q i }) i') x'

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

      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 nProp} (hr : (v : CliffordAlgebra Q) → (h : v LinearMap.range (CliffordAlgebra.ι Q) ^ ZMod.val n) → P v (_ : v ⨆ (i : { n // n = 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 hxP y hyP (x + y) (_ : x + y CliffordAlgebra.evenOdd Q n)) (hιι_mul : (m₁ m₂ : M) → {x : CliffordAlgebra Q} → {hx : x CliffordAlgebra.evenOdd Q n} → P x hxP (↑(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 0Prop} (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 hxP y hyP (x + y) (_ : x + y CliffordAlgebra.evenOdd Q 0)) (hιι_mul : (m₁ m₂ : M) → {x : CliffordAlgebra Q} → {hx : x CliffordAlgebra.evenOdd Q 0} → P x hxP (↑(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 1Prop} (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 hxP y hyP (x + y) (_ : x + y CliffordAlgebra.evenOdd Q 1)) (hιι_mul : (m₁ m₂ : M) → {x : CliffordAlgebra Q} → {hx : x CliffordAlgebra.evenOdd Q 1} → P x hxP (↑(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.