Documentation

Mathlib.LinearAlgebra.CliffordAlgebra.Fold

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 #

Main statements #

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

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

Instances For
    @[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 : CliffordAlgebra Q) (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.prod (List.map (↑(CliffordAlgebra.ι Q)) l)) = List.foldr (fun m 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) :

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

    Instances For
      @[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 : CliffordAlgebra Q) (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.prod (List.map (↑(CliffordAlgebra.ι Q)) l)) = List.foldl (fun m n => ↑(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 QProp} (hr : (r : R) → P (↑(algebraMap R (CliffordAlgebra Q)) r)) (h_add : (x y : CliffordAlgebra Q) → P xP yP (x + y)) (h_ι_mul : (m : M) → (x : CliffordAlgebra Q) → P xP (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 QProp} (hr : (r : R) → P (↑(algebraMap R (CliffordAlgebra Q)) r)) (h_add : (x y : CliffordAlgebra Q) → P xP yP (x + y)) (h_mul_ι : (x : CliffordAlgebra Q) → (m : M) → P xP (↑(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) :

      Auxiliary definition for CliffordAlgebra.foldr'

      Instances For
        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.fst, ↑(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) :

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

        Instances For
          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)