English
The Clifford algebra is endowed with a grading by the even and odd parts, making it a graded algebra over the graded subspaces evenOdd(Q).
Русский
Клиффордова алгебра наделяется градацией по чётной и нечётной частям, образуя градуированную алгебру над подпространствами evenOdd(Q).
LaTeX
$$GradedAlgebra(CliffordAlgebra, evenOdd(Q))$$
Lean4
/-- The clifford algebra is graded by the even and odd parts. -/
instance gradedAlgebra : GradedAlgebra (evenOdd Q) :=
GradedAlgebra.ofAlgHom
(evenOdd Q)
-- while not necessary, the `by apply` makes this elaborate faster
(lift Q ⟨by apply GradedAlgebra.ι Q, by apply GradedAlgebra.ι_sq_scalar Q⟩)
-- the proof from here onward is mostly similar to the `TensorAlgebra` case, with some extra
-- handling for the `iSup` in `evenOdd`.
(by
ext m
dsimp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply, AlgHom.comp_apply, AlgHom.id_apply]
rw [lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.coeAlgHom_of, Subtype.coe_mk])
(by apply GradedAlgebra.lift_ι_eq Q)
