English
Let Q be a quadratic form on M. For a bilinear map f: M → N → N that satisfies the defining Clifford relation f(m) ∘ f(m) = Q(m) · id on N for every m ∈ M, the fold operation along the Clifford algebra satisfies that applying the fold to the generator ι_Q(m) yields f(m, n) when evaluated at n ∈ N. In other words, folding along the generator ι_Q(m) acts as the given bilinear action on n.
Русский
Пусть Q – квадратичная форма на M. Для билинеарного отображения f: M → N → N, удовлетворяющего кла̀сическому соотношению Клиффорд: f(m) ∘ f(m) = Q(m) · id на N для каждого m ∈ M, свёртка по алгебре Clifford удовлетворяет: применение свёртки к генератору ι_Q(m) даёт f(m, n). Иными словами, свёртка по генератору ι_Q(m) действует как заданное билинейное действие на n.
LaTeX
$$$\\foldr_Q f hf n (\\iota_Q m) = f m n$$$
Lean4
@[simp]
theorem foldr_ι (f : M →ₗ[R] N →ₗ[R] N) (hf) (n : N) (m : M) : foldr Q f hf n (ι Q m) = f m n :=
LinearMap.congr_fun (lift_ι_apply _ _ _) n
