CliffordAlgebra.foldr_prod_map_ι
theorem CliffordAlgebra.foldr_prod_map_ι :
∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M]
[inst_2 : AddCommGroup N] [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (l : List M)
(f : M →ₗ[R] N →ₗ[R] N) (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) (n : N),
((CliffordAlgebra.foldr Q f hf) n) (List.map (⇑(CliffordAlgebra.ι Q)) l).prod =
List.foldr (fun m n => (f m) n) n l
This theorem, named `CliffordAlgebra.foldr_prod_map_ι`, states that for any commutative ring `R`, additive commutative groups `M` and `N`, and modules `M` and `N` over `R`, given a quadratic form `Q` on `M`, a list `l` of elements of `M`, a linear map `f` from `M` to another linear map from `N` to `N` that satisfies a certain property, and an element `n` of `N`, the application of the `foldr` function of the Clifford Algebra on `n` and the product of mapping the list `l` through the canonical linear map of the Clifford Algebra equals the result of folding the list `l` with the function that applies the linear map `f` on its elements, starting with the element `n`. The property that the linear map `f` needs to satisfy is that for any element `m` of `M` and `x` of `N`, applying `f m` twice on `x` results in scaling `x` by the value of the quadratic form `Q` at `m`.
More concisely: Given a commutative ring `R`, additive commutative groups `M` and `N`, modules `M` and `N` over `R`, a quadratic form `Q` on `M`, a list `l` of elements of `M`, a linear map `f : M -> (N -> N)` satisfying `f m x * f m x = Q m * x` for all `m in M` and `x in N`, and an element `n in N`, we have `(foldr (λ x, f x) n l) = foldr (λ x, (f x).map) n (list.map f l)`.
|
CliffordAlgebra.foldl_prod_map_ι
theorem CliffordAlgebra.foldl_prod_map_ι :
∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M]
[inst_2 : AddCommGroup N] [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (l : List M)
(f : M →ₗ[R] N →ₗ[R] N) (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) (n : N),
((CliffordAlgebra.foldl Q f hf) n) (List.map (⇑(CliffordAlgebra.ι Q)) l).prod =
List.foldl (fun m n => (f n) m) n l
This theorem, named `CliffordAlgebra.foldl_prod_map_ι`, states that for any commutative ring `R`, any additive commutative groups `M` and `N`, any modules `M` and `N` over `R`, any quadratic form `Q` over `M`, any list `l` of elements from `M`, any linear map `f` from `M` to the endomorphism ring of `N`, and any element `n` from `N` that satisfies a particular property, the product of the `foldl` function applied to the `Q` Clifford Algebra, the linear map `f`, the property, and `n`, mapped over the list `l` using the canonical linear map `ι` of the `Q` Clifford Algebra, is equal to the `foldl` function applied to a given function, `n`, and `l`. The particular property `hf` that needs to be satisfied is that for all elements `m` from `M` and `x` from `N`, applying `f` twice to `x` using `m` is the same as scaling `x` by the application of the quadratic form `Q` to `m`.
More concisely: For any commutative ring `R`, additive commutative groups `M` and `N`, modules `M` and `N` over `R`, quadratic form `Q` over `M`, list `l` of elements from `M`, linear map `f` from `M` to the endomorphism ring of `N`, and element `n` from `N` satisfying `f(mx) = Q(m) * f(x)` for all `m` in `M` and `x` in `N`, the product of `foldl` of `Q.algebra.mul`, `f`, the property `hf`, and `n` on list `l` via the canonical map `ι`, equals the `foldl` of a given function, `n`, and `l`.
|