English
The construction evenToNeg provides a canonical algebra homomorphism from the even subalgebra of Q to the even subalgebra of Q' when Q' = −Q, mapping generators to their negated counterparts.
Русский
Конструкция EvenToNeg задаёт каноническое алгебра-гомоморфное отображение от чётной подпалгебры Q к чётной подпалгебре Q' при Q' = −Q, переводя порождающие в их отрицательные аналоги.
LaTeX
$$$ evenToNeg Q Q' h: \\mathrm{even}(Q) \\to_A_R \\mathrm{even}(Q') $ with $Q' = -Q$$$
Lean4
/-- Fold a bilinear map along the generators of a term of the clifford algebra, with the rule
given by `foldr Q f hf n (ι Q m * x) = f m (foldr Q f hf n x)`.
For example, `foldr f hf n (r • ι R u + ι R v * ι R w) = r • f u n + f v (f w n)`. -/
def foldr (f : M →ₗ[R] N →ₗ[R] N) (hf : ∀ m x, f m (f m x) = Q m • x) : N →ₗ[R] CliffordAlgebra Q →ₗ[R] N :=
(CliffordAlgebra.lift Q ⟨f, fun v => LinearMap.ext <| hf v⟩).toLinearMap.flip
