Recursive computation rules for the Clifford algebra #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file provides API for a special case clifford_algebra.foldr of the universal property
clifford_algebra.lift with A = module.End R N for some arbitrary module N. This specialization
resembles the list.foldr operation, allowing a bilinear map to be "folded" along the generators.
For convenience, this file also provides clifford_algebra.foldl, implemented via
clifford_algebra.reverse
Main definitions #
clifford_algebra.foldr: a computation rule for building linear maps out of the clifford algebra starting on the right, analogous to usinglist.foldron the generators.clifford_algebra.foldl: a computation rule for building linear maps out of the clifford algebra starting on the left, analogous to usinglist.foldlon the generators.
Main statements #
clifford_algebra.right_induction: an induction rule that adds generators from the right.clifford_algebra.left_induction: an induction rule that adds generators from the left.
def
clifford_algebra.foldr
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] N →ₗ[R] N)
(hf : ∀ (m : M) (x : N), ⇑(⇑f m) (⇑(⇑f m) x) = ⇑Q m • x) :
N →ₗ[R] clifford_algebra Q →ₗ[R] N
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).
Equations
- clifford_algebra.foldr Q f hf = (⇑(clifford_algebra.lift Q) ⟨f, _⟩).to_linear_map.flip
@[simp]
theorem
clifford_algebra.foldr_ι
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] N →ₗ[R] N)
(hf : ∀ (m : M) (x : N), ⇑(⇑f m) (⇑(⇑f m) x) = ⇑Q m • x)
(n : N)
(m : M) :
⇑(⇑(clifford_algebra.foldr Q f hf) n) (⇑(clifford_algebra.ι Q) m) = ⇑(⇑f m) n
@[simp]
theorem
clifford_algebra.foldr_algebra_map
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] N →ₗ[R] N)
(hf : ∀ (m : M) (x : N), ⇑(⇑f m) (⇑(⇑f m) x) = ⇑Q m • x)
(n : N)
(r : R) :
⇑(⇑(clifford_algebra.foldr Q f hf) n) (⇑(algebra_map R (clifford_algebra Q)) r) = r • n
@[simp]
theorem
clifford_algebra.foldr_one
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] N →ₗ[R] N)
(hf : ∀ (m : M) (x : N), ⇑(⇑f m) (⇑(⇑f m) x) = ⇑Q m • x)
(n : N) :
⇑(⇑(clifford_algebra.foldr Q f hf) n) 1 = n
@[simp]
theorem
clifford_algebra.foldr_mul
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] N →ₗ[R] N)
(hf : ∀ (m : M) (x : N), ⇑(⇑f m) (⇑(⇑f m) x) = ⇑Q m • x)
(n : N)
(a b : clifford_algebra Q) :
⇑(⇑(clifford_algebra.foldr Q f hf) n) (a * b) = ⇑(⇑(clifford_algebra.foldr Q f hf) (⇑(⇑(clifford_algebra.foldr Q f hf) n) b)) a
theorem
clifford_algebra.foldr_prod_map_ι
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form 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) :
⇑(⇑(clifford_algebra.foldr Q f hf) n) (list.map ⇑(clifford_algebra.ι Q) l).prod = list.foldr (λ (m : M) (n : N), ⇑(⇑f m) n) n l
This lemma demonstrates the origin of the foldr name.
def
clifford_algebra.foldl
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] N →ₗ[R] N)
(hf : ∀ (m : M) (x : N), ⇑(⇑f m) (⇑(⇑f m) x) = ⇑Q m • x) :
N →ₗ[R] clifford_algebra Q →ₗ[R] N
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).
Equations
- clifford_algebra.foldl Q f hf = (clifford_algebra.foldr Q f hf).compl₂ clifford_algebra.reverse
@[simp]
theorem
clifford_algebra.foldl_reverse
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] N →ₗ[R] N)
(hf : ∀ (m : M) (x : N), ⇑(⇑f m) (⇑(⇑f m) x) = ⇑Q m • x)
(n : N)
(x : clifford_algebra Q) :
⇑(⇑(clifford_algebra.foldl Q f hf) n) (⇑clifford_algebra.reverse x) = ⇑(⇑(clifford_algebra.foldr Q f hf) n) x
@[simp]
theorem
clifford_algebra.foldr_reverse
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] N →ₗ[R] N)
(hf : ∀ (m : M) (x : N), ⇑(⇑f m) (⇑(⇑f m) x) = ⇑Q m • x)
(n : N)
(x : clifford_algebra Q) :
⇑(⇑(clifford_algebra.foldr Q f hf) n) (⇑clifford_algebra.reverse x) = ⇑(⇑(clifford_algebra.foldl Q f hf) n) x
@[simp]
theorem
clifford_algebra.foldl_ι
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] N →ₗ[R] N)
(hf : ∀ (m : M) (x : N), ⇑(⇑f m) (⇑(⇑f m) x) = ⇑Q m • x)
(n : N)
(m : M) :
⇑(⇑(clifford_algebra.foldl Q f hf) n) (⇑(clifford_algebra.ι Q) m) = ⇑(⇑f m) n
@[simp]
theorem
clifford_algebra.foldl_algebra_map
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] N →ₗ[R] N)
(hf : ∀ (m : M) (x : N), ⇑(⇑f m) (⇑(⇑f m) x) = ⇑Q m • x)
(n : N)
(r : R) :
⇑(⇑(clifford_algebra.foldl Q f hf) n) (⇑(algebra_map R (clifford_algebra Q)) r) = r • n
@[simp]
theorem
clifford_algebra.foldl_one
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] N →ₗ[R] N)
(hf : ∀ (m : M) (x : N), ⇑(⇑f m) (⇑(⇑f m) x) = ⇑Q m • x)
(n : N) :
⇑(⇑(clifford_algebra.foldl Q f hf) n) 1 = n
@[simp]
theorem
clifford_algebra.foldl_mul
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] N →ₗ[R] N)
(hf : ∀ (m : M) (x : N), ⇑(⇑f m) (⇑(⇑f m) x) = ⇑Q m • x)
(n : N)
(a b : clifford_algebra Q) :
⇑(⇑(clifford_algebra.foldl Q f hf) n) (a * b) = ⇑(⇑(clifford_algebra.foldl Q f hf) (⇑(⇑(clifford_algebra.foldl Q f hf) n) a)) b
theorem
clifford_algebra.foldl_prod_map_ι
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form 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) :
⇑(⇑(clifford_algebra.foldl Q f hf) n) (list.map ⇑(clifford_algebra.ι Q) l).prod = list.foldl (λ (m : N) (n : M), ⇑(⇑f n) m) n l
This lemma demonstrates the origin of the foldl name.
theorem
clifford_algebra.right_induction
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
{P : clifford_algebra Q → Prop}
(hr : ∀ (r : R), P (⇑(algebra_map R (clifford_algebra Q)) r))
(h_add : ∀ (x y : clifford_algebra Q), P x → P y → P (x + y))
(h_ι_mul : ∀ (m : M) (x : clifford_algebra Q), P x → P (x * ⇑(clifford_algebra.ι Q) m))
(x : clifford_algebra Q) :
P x
theorem
clifford_algebra.left_induction
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
{P : clifford_algebra Q → Prop}
(hr : ∀ (r : R), P (⇑(algebra_map R (clifford_algebra Q)) r))
(h_add : ∀ (x y : clifford_algebra Q), P x → P y → P (x + y))
(h_mul_ι : ∀ (x : clifford_algebra Q) (m : M), P x → P (⇑(clifford_algebra.ι Q) m * x))
(x : clifford_algebra Q) :
P x
Versions with extra state #
def
clifford_algebra.foldr'_aux
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] clifford_algebra Q × N →ₗ[R] N) :
M →ₗ[R] module.End R (clifford_algebra Q × N)
Auxiliary definition for clifford_algebra.foldr'
Equations
- clifford_algebra.foldr'_aux Q f = {to_fun := λ (m : M), (⇑(((algebra.lmul R (clifford_algebra Q)).to_linear_map.comp (clifford_algebra.ι Q)).compl₂ (linear_map.fst R (clifford_algebra Q) N)) m).prod (⇑f m), map_add' := _, map_smul' := _}
theorem
clifford_algebra.foldr'_aux_apply_apply
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] clifford_algebra Q × N →ₗ[R] N)
(m : M)
(x_fx : clifford_algebra Q × N) :
⇑(⇑(clifford_algebra.foldr'_aux Q f) m) x_fx = (⇑(clifford_algebra.ι Q) m * x_fx.fst, ⇑(⇑f m) x_fx)
theorem
clifford_algebra.foldr'_aux_foldr'_aux
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] clifford_algebra Q × N →ₗ[R] N)
(hf : ∀ (m : M) (x : clifford_algebra Q) (fx : N), ⇑(⇑f m) (⇑(clifford_algebra.ι Q) m * x, ⇑(⇑f m) (x, fx)) = ⇑Q m • fx)
(v : M)
(x_fx : clifford_algebra Q × N) :
⇑(⇑(clifford_algebra.foldr'_aux Q f) v) (⇑(⇑(clifford_algebra.foldr'_aux Q f) v) x_fx) = ⇑Q v • x_fx
def
clifford_algebra.foldr'
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] clifford_algebra Q × N →ₗ[R] N)
(hf : ∀ (m : M) (x : clifford_algebra Q) (fx : N), ⇑(⇑f m) (⇑(clifford_algebra.ι Q) m * x, ⇑(⇑f m) (x, fx)) = ⇑Q m • fx)
(n : N) :
clifford_algebra Q →ₗ[R] N
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 (x, foldr' Q f hf n x).
Note this is like clifford_algebra.foldr, but with an extra x argument.
Implement the recursion scheme F[n0](m * x) = f(m, (x, F[n0](x))).
Equations
- clifford_algebra.foldr' Q f hf n = (linear_map.snd R (clifford_algebra Q) N).comp (⇑(clifford_algebra.foldr Q (clifford_algebra.foldr'_aux Q f) _) (1, n))
theorem
clifford_algebra.foldr'_algebra_map
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] clifford_algebra Q × N →ₗ[R] N)
(hf : ∀ (m : M) (x : clifford_algebra Q) (fx : N), ⇑(⇑f m) (⇑(clifford_algebra.ι Q) m * x, ⇑(⇑f m) (x, fx)) = ⇑Q m • fx)
(n : N)
(r : R) :
⇑(clifford_algebra.foldr' Q f hf n) (⇑(algebra_map R (clifford_algebra Q)) r) = r • n
theorem
clifford_algebra.foldr'_ι
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] clifford_algebra Q × N →ₗ[R] N)
(hf : ∀ (m : M) (x : clifford_algebra Q) (fx : N), ⇑(⇑f m) (⇑(clifford_algebra.ι Q) m * x, ⇑(⇑f m) (x, fx)) = ⇑Q m • fx)
(n : N)
(m : M) :
⇑(clifford_algebra.foldr' Q f hf n) (⇑(clifford_algebra.ι Q) m) = ⇑(⇑f m) (1, n)
theorem
clifford_algebra.foldr'_ι_mul
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[add_comm_group N]
[module R M]
[module R N]
(Q : quadratic_form R M)
(f : M →ₗ[R] clifford_algebra Q × N →ₗ[R] N)
(hf : ∀ (m : M) (x : clifford_algebra Q) (fx : N), ⇑(⇑f m) (⇑(clifford_algebra.ι Q) m * x, ⇑(⇑f m) (x, fx)) = ⇑Q m • fx)
(n : N)
(m : M)
(x : clifford_algebra Q) :
⇑(clifford_algebra.foldr' Q f hf n) (⇑(clifford_algebra.ι Q) m * x) = ⇑(⇑f m) (x, ⇑(clifford_algebra.foldr' Q f hf n) x)