English
There is a left-fold operation foldl Q f hf that acts on an accumulator n and a Clifford algebra element x by iterating the bilinear map f along the left generator structure; it is defined as a function sending n to a linear map from CliffordAlgebra Q to N, built from the right-fold via a helper construct.
Русский
Существует операция левой свёртки foldl Q f hf, действующая на аккумулятор n и элемент CliffordAlgebra Q, которая строится через итерацию по левому генератору; определяется как функция, отправляющая n в линейный отображение CliffordAlgebra Q → N, полученное через вспомогательную конструкцию.
LaTeX
$$$\\text{foldl}_Q\\,f\\,hf : N \\to (CliffordAlgebra\\ Q \\to N)$$$
Lean4
/-- Fold a bilinear map along the generators of a term of the clifford algebra, with the rule
given by `foldl Q f hf n (ι Q m * x) = f m (foldl Q f hf n x)`.
For example, `foldl f hf n (r • ι R u + ι R v * ι R w) = r • f u n + f v (f w n)`. -/
def foldl (f : M →ₗ[R] N →ₗ[R] N) (hf : ∀ m x, f m (f m x) = Q m • x) : N →ₗ[R] CliffordAlgebra Q →ₗ[R] N :=
LinearMap.compl₂ (foldr Q f hf) reverse
