mathlib3 documentation

linear_algebra.clifford_algebra.fold

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 #

Main statements #

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) :

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
@[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) :
@[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) :
@[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) :
@[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) :
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) :

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
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
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) :

Auxiliary definition for clifford_algebra.foldr'

Equations
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) :
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) :

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
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) :
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) :
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) :