Grading by ℤ / 2ℤ #
This file defines the grading by zmod 2, as the function clifford_algebra.grades'.
Main results #
clifford_algebra.grades'_left_inverse,grades'has a left-inverse,add_monoid_algebra.sum_id.clifford_algebra.grades'.map_grades',grades'is idempotent
noncomputable
def
clifford_algebra.grades'
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M} :
clifford_algebra Q →ₐ[R] add_monoid_algebra (clifford_algebra Q) (zmod 2)
Separate an element of the clifford algebra into its zmod 2-graded components.
This is defined as an alg_hom to add_monoid_algebra so that algebra operators can be moved
before and after the mapping.
This is not the normal ℕ-graded definition that we usually use in GA. That definition is harder...
Equations
theorem
clifford_algebra.sum_id_comp_grades'
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M} :
Recombining the grades recovers the original element
theorem
clifford_algebra.grades'_left_inverse
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M} :
Stated another way, grades' has a left-inverse and is therefore injective (via function.left_inverse.injective).
@[protected, instance]
noncomputable
def
clifford_algebra.has_coe
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M} :
has_coe (add_monoid_algebra (clifford_algebra Q) (zmod 2)) (clifford_algebra Q)
Equations
@[simp, norm_cast]
theorem
clifford_algebra.coe_def
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(x : add_monoid_algebra (clifford_algebra Q) (zmod 2)) :
↑x = ⇑(add_monoid_algebra.sum_id R) x
theorem
clifford_algebra.grades'.map_algebra_map
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(r : R) :
⇑clifford_algebra.grades' (⇑(algebra_map R (clifford_algebra Q)) r) = finsupp.single 0 (⇑(algebra_map R (clifford_algebra Q)) r)
An element of R lifted with algebra_map has a single grade 0 element
theorem
clifford_algebra.grades'.map_ι
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(x : M) :
⇑clifford_algebra.grades' (⇑(clifford_algebra.ι Q) x) = finsupp.single 1 (⇑(clifford_algebra.ι Q) x)
An element of X lifted with the canonical ι R function has a single grade 1 element
@[simp]
theorem
clifford_algebra.grades'.map_grades'
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(x : clifford_algebra Q)
(i : zmod 2) :