Results about the grading structure of the clifford algebra #
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}), (clifford_algebra.ι Q).range ^ ↑j
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.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] ⨁ (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 (⨁ (i : zmod 2), ↥(clifford_algebra.even_odd Q i))) (⇑Q m)
@[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) :