Results about the grading structure of the clifford algebra #
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]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(i : zmod 2) :
submodule R (clifford_algebra Q)
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
- clifford_algebra.even_odd Q i = ⨆ (j : {n // ↑n = i}), linear_map.range (clifford_algebra.ι Q) ^ ↑j
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) :
1 ≤ clifford_algebra.even_odd Q 0
theorem
clifford_algebra.range_ι_le_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) :
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) :
⇑(clifford_algebra.ι Q) m ∈ clifford_algebra.even_odd Q 1
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) :
⇑(clifford_algebra.ι Q) m₁ * ⇑(clifford_algebra.ι Q) m₂ ∈ clifford_algebra.even_odd Q 0
theorem
clifford_algebra.even_odd_mul_le
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(i j : zmod 2) :
clifford_algebra.even_odd Q i * clifford_algebra.even_odd Q j ≤ clifford_algebra.even_odd Q (i + j)
@[protected, instance]
def
clifford_algebra.even_odd.graded_monoid
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
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) :
M →ₗ[R] direct_sum (zmod 2) (λ (i : zmod 2), ↥(clifford_algebra.even_odd Q i))
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
- clifford_algebra.graded_algebra.ι Q = (direct_sum.lof R (zmod 2) (λ (i : zmod 2), ↥(clifford_algebra.even_odd Q i)) 1).comp (linear_map.cod_restrict (clifford_algebra.even_odd Q 1) (clifford_algebra.ι Q) _)
theorem
clifford_algebra.graded_algebra.ι_apply
{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) :
⇑(clifford_algebra.graded_algebra.ι Q) m = ⇑(direct_sum.of (λ (i : zmod 2), ↥(clifford_algebra.even_odd Q i)) 1) ⟨⇑(clifford_algebra.ι Q) m, _⟩
theorem
clifford_algebra.graded_algebra.ι_sq_scalar
{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) :
⇑(clifford_algebra.graded_algebra.ι Q) m * ⇑(clifford_algebra.graded_algebra.ι Q) m = ⇑(algebra_map R (direct_sum (zmod 2) (λ (i : zmod 2), ↥(clifford_algebra.even_odd Q i)))) (⇑Q m)
theorem
clifford_algebra.graded_algebra.lift_ι_eq
{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)
(x' : ↥(clifford_algebra.even_odd Q i')) :
⇑(⇑(clifford_algebra.lift Q) ⟨clifford_algebra.graded_algebra.ι Q, _⟩) ↑x' = ⇑(direct_sum.of (λ (i : zmod 2), ↥(clifford_algebra.even_odd Q i)) i') x'
@[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) :
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 : ℕ), linear_map.range (clifford_algebra.ι Q) ^ i) = ⊤
theorem
clifford_algebra.even_odd_is_compl
{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.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 ∈ linear_map.range (clifford_algebra.ι Q) ^ 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 hx → P y hy → P (x + y) _)
(hιι_mul : ∀ (m₁ m₂ : M) {x : clifford_algebra Q} {hx : x ∈ clifford_algebra.even_odd Q n}, P x hx → P (⇑(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 hx → P y hy → P (x + y) _)
(hιι_mul : ∀ (m₁ m₂ : M) {x : clifford_algebra Q} {hx : x ∈ clifford_algebra.even_odd Q 0}, P x hx → P (⇑(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 hx → P y hy → P (x + y) _)
(hιι_mul : ∀ (m₁ m₂ : M) {x : clifford_algebra Q} {hx : x ∈ clifford_algebra.even_odd Q 1}, P x hx → P (⇑(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.