Recursive computation rules for the Clifford algebra

This file provides API for a special case CliffordAlgebra.foldr of the universal property CliffordAlgebra.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 CliffordAlgebra.foldl, implemented via CliffordAlgebra.reverse

Main definitions

• CliffordAlgebra.foldr: a computation rule for building linear maps out of the clifford algebra starting on the right, analogous to using list.foldr on the generators.
• CliffordAlgebra.foldl: a computation rule for building linear maps out of the clifford algebra starting on the left, analogous to using list.foldl on the generators.

Main statements

• CliffordAlgebra.right_induction: an induction rule that adds generators from the right.
• CliffordAlgebra.left_induction: an induction rule that adds generators from the left.

def CliffordAlgebra.foldr {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] N →ₗ[R] N) (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) : N →ₗ[R] CliffordAlgebra 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

• CliffordAlgebra.foldr Q f hf = ((CliffordAlgebra.lift Q) ⟨f, ⋯⟩).toLinearMap.flip

@[simp]

theorem CliffordAlgebra.foldr_ι {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm 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) : ((CliffordAlgebra.foldr Q f hf) n) ((CliffordAlgebra.ι Q) m) = (f m) n

@[simp]

theorem CliffordAlgebra.foldr_algebraMap {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm 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) : ((CliffordAlgebra.foldr Q f hf) n) ((algebraMap R (CliffordAlgebra Q)) r) = r • n

@[simp]

theorem CliffordAlgebra.foldr_one {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm R 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) 1 = n

@[simp]

theorem CliffordAlgebra.foldr_mul {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm 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 : CliffordAlgebra Q) : ((CliffordAlgebra.foldr Q f hf) n) (a * b) = ((CliffordAlgebra.foldr Q f hf) (((CliffordAlgebra.foldr Q f hf) n) b)) a

theorem CliffordAlgebra.foldr_prod_map_ι {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [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 : M) (n : N) => (f m) n) n l

This lemma demonstrates the origin of the foldr name.

def CliffordAlgebra.foldl {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] N →ₗ[R] N) (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) : N →ₗ[R] CliffordAlgebra 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

• CliffordAlgebra.foldl Q f hf = (CliffordAlgebra.foldr Q f hf).compl₂ CliffordAlgebra.reverse

@[simp]

theorem CliffordAlgebra.foldl_reverse {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] N →ₗ[R] N) (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) (n : N) (x : CliffordAlgebra Q) : ((CliffordAlgebra.foldl Q f hf) n) (CliffordAlgebra.reverse x) = ((CliffordAlgebra.foldr Q f hf) n) x

@[simp]

theorem CliffordAlgebra.foldr_reverse {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] N →ₗ[R] N) (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) (n : N) (x : CliffordAlgebra Q) : ((CliffordAlgebra.foldr Q f hf) n) (CliffordAlgebra.reverse x) = ((CliffordAlgebra.foldl Q f hf) n) x

@[simp]

theorem CliffordAlgebra.foldl_ι {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm 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) : ((CliffordAlgebra.foldl Q f hf) n) ((CliffordAlgebra.ι Q) m) = (f m) n

@[simp]

theorem CliffordAlgebra.foldl_algebraMap {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm 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) : ((CliffordAlgebra.foldl Q f hf) n) ((algebraMap R (CliffordAlgebra Q)) r) = r • n

@[simp]

theorem CliffordAlgebra.foldl_one {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm R 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) 1 = n

@[simp]

theorem CliffordAlgebra.foldl_mul {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm 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 : CliffordAlgebra Q) : ((CliffordAlgebra.foldl Q f hf) n) (a * b) = ((CliffordAlgebra.foldl Q f hf) (((CliffordAlgebra.foldl Q f hf) n) a)) b

theorem CliffordAlgebra.foldl_prod_map_ι {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [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) (n : M) => (f n) m) n l

This lemma demonstrates the origin of the foldl name.

theorem CliffordAlgebra.right_induction {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {P : CliffordAlgebra Q → Prop} (algebraMap : ∀ (r : R), P ((algebraMap R (CliffordAlgebra Q)) r)) (add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)) (mul_ι : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * (CliffordAlgebra.ι Q) m)) (x : CliffordAlgebra Q) : P x

theorem CliffordAlgebra.left_induction {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {P : CliffordAlgebra Q → Prop} (algebraMap : ∀ (r : R), P ((algebraMap R (CliffordAlgebra Q)) r)) (add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)) (ι_mul : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((CliffordAlgebra.ι Q) m * x)) (x : CliffordAlgebra Q) : P x

Versions with extra state

def CliffordAlgebra.foldr'Aux {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N) : M →ₗ[R] Module.End R (CliffordAlgebra Q × N)

Auxiliary definition for CliffordAlgebra.foldr'

Equations

• One or more equations did not get rendered due to their size.

theorem CliffordAlgebra.foldr'Aux_apply_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N) (m : M) (x_fx : CliffordAlgebra Q × N) : ((CliffordAlgebra.foldr'Aux Q f) m) x_fx = ((CliffordAlgebra.ι Q) m * x_fx.1, (f m) x_fx)

theorem CliffordAlgebra.foldr'Aux_foldr'Aux {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N) (hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((CliffordAlgebra.ι Q) m * x, (f m) (x, fx)) = Q m • fx) (v : M) (x_fx : CliffordAlgebra Q × N) : ((CliffordAlgebra.foldr'Aux Q f) v) (((CliffordAlgebra.foldr'Aux Q f) v) x_fx) = Q v • x_fx

def CliffordAlgebra.foldr' {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N) (hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((CliffordAlgebra.ι Q) m * x, (f m) (x, fx)) = Q m • fx) (n : N) : CliffordAlgebra 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 CliffordAlgebra.foldr, but with an extra x argument. Implement the recursion scheme F[n0](m * x) = f(m, (x, F[n0](x))).

Equations

• CliffordAlgebra.foldr' Q f hf n = LinearMap.snd R (CliffordAlgebra Q) N ∘ₗ (CliffordAlgebra.foldr Q (CliffordAlgebra.foldr'Aux Q f) ⋯) (1, n)

theorem CliffordAlgebra.foldr'_algebraMap {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N) (hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((CliffordAlgebra.ι Q) m * x, (f m) (x, fx)) = Q m • fx) (n : N) (r : R) : (CliffordAlgebra.foldr' Q f hf n) ((algebraMap R (CliffordAlgebra Q)) r) = r • n

theorem CliffordAlgebra.foldr'_ι {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N) (hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((CliffordAlgebra.ι Q) m * x, (f m) (x, fx)) = Q m • fx) (n : N) (m : M) : (CliffordAlgebra.foldr' Q f hf n) ((CliffordAlgebra.ι Q) m) = (f m) (1, n)

theorem CliffordAlgebra.foldr'_ι_mul {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N) (hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((CliffordAlgebra.ι Q) m * x, (f m) (x, fx)) = Q m • fx) (n : N) (m : M) (x : CliffordAlgebra Q) : (CliffordAlgebra.foldr' Q f hf n) ((CliffordAlgebra.ι Q) m * x) = (f m) (x, (CliffordAlgebra.foldr' Q f hf n) x)