Documentation

Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Contraction in Clifford Algebras #

This file contains some of the results from [grinberg_clifford_2016][]. The key result is CliffordAlgebra.equivExterior.

Main definitions #

Implementation notes #

This file somewhat follows [grinberg_clifford_2016][], although we are missing some of the induction principles needed to prove many of the results. Here, we avoid the quotient-based approach described in [grinberg_clifford_2016][], instead directly constructing our objects using the universal property.

Note that [grinberg_clifford_2016][] concludes that its contents are not novel, and are in fact just a rehash of parts of [bourbaki2007][]; we should at some point consider swapping our references to refer to the latter.

Within this file, we use the local notation

@[simp]
theorem CliffordAlgebra.contractLeftAux_apply_apply {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (d : Module.Dual R M) (a : M) (a : CliffordAlgebra Q × CliffordAlgebra Q) :
↑(↑(CliffordAlgebra.contractLeftAux Q d) a) a = d a a.fst - ↑(CliffordAlgebra.ι Q) a * a.snd
theorem CliffordAlgebra.contractLeftAux_contractLeftAux {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (d : Module.Dual R M) (v : M) (x : CliffordAlgebra Q) (fx : CliffordAlgebra Q) :
↑(↑(CliffordAlgebra.contractLeftAux Q d) v) (↑(CliffordAlgebra.ι Q) v * x, ↑(↑(CliffordAlgebra.contractLeftAux Q d) v) (x, fx)) = Q v fx

Contract an element of the clifford algebra with an element d : Module.Dual R M from the left.

Note that $v ⌋ x$ is spelt contractLeft (Q.associated v) x.

This includes [grinberg_clifford_2016][] Theorem 10.75

Instances For

    Contract an element of the clifford algebra with an element d : Module.Dual R M from the right.

    Note that $x ⌊ v$ is spelt contractRight x (Q.associated v).

    This includes [grinberg_clifford_2016][] Theorem 16.75

    Instances For
      theorem CliffordAlgebra.contractRight_eq {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (d : Module.Dual R M) (x : CliffordAlgebra Q) :
      ↑(CliffordAlgebra.contractRight x) d = CliffordAlgebra.reverse (↑(CliffordAlgebra.contractLeft d) (CliffordAlgebra.reverse x))
      theorem CliffordAlgebra.contractLeft_ι_mul {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (d : Module.Dual R M) (a : M) (b : CliffordAlgebra Q) :
      ↑(CliffordAlgebra.contractLeft d) (↑(CliffordAlgebra.ι Q) a * b) = d a b - ↑(CliffordAlgebra.ι Q) a * ↑(CliffordAlgebra.contractLeft d) b

      This is [grinberg_clifford_2016][] Theorem 6

      theorem CliffordAlgebra.contractRight_mul_ι {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (d : Module.Dual R M) (a : M) (b : CliffordAlgebra Q) :
      ↑(CliffordAlgebra.contractRight (b * ↑(CliffordAlgebra.ι Q) a)) d = d a b - ↑(CliffordAlgebra.contractRight b) d * ↑(CliffordAlgebra.ι Q) a

      This is [grinberg_clifford_2016][] Theorem 12

      theorem CliffordAlgebra.contractLeft_algebraMap_mul {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (d : Module.Dual R M) (r : R) (b : CliffordAlgebra Q) :
      ↑(CliffordAlgebra.contractLeft d) (↑(algebraMap R (CliffordAlgebra Q)) r * b) = ↑(algebraMap R (CliffordAlgebra Q)) r * ↑(CliffordAlgebra.contractLeft d) b
      theorem CliffordAlgebra.contractLeft_mul_algebraMap {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (d : Module.Dual R M) (a : CliffordAlgebra Q) (r : R) :
      ↑(CliffordAlgebra.contractLeft d) (a * ↑(algebraMap R (CliffordAlgebra Q)) r) = ↑(CliffordAlgebra.contractLeft d) a * ↑(algebraMap R (CliffordAlgebra Q)) r
      theorem CliffordAlgebra.contractRight_algebraMap_mul {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (d : Module.Dual R M) (r : R) (b : CliffordAlgebra Q) :
      ↑(CliffordAlgebra.contractRight (↑(algebraMap R (CliffordAlgebra Q)) r * b)) d = ↑(algebraMap R (CliffordAlgebra Q)) r * ↑(CliffordAlgebra.contractRight b) d
      theorem CliffordAlgebra.contractRight_mul_algebraMap {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (d : Module.Dual R M) (a : CliffordAlgebra Q) (r : R) :
      ↑(CliffordAlgebra.contractRight (a * ↑(algebraMap R (CliffordAlgebra Q)) r)) d = ↑(CliffordAlgebra.contractRight a) d * ↑(algebraMap R (CliffordAlgebra Q)) r
      @[simp]
      theorem CliffordAlgebra.contractLeft_ι {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (d : Module.Dual R M) (x : M) :
      ↑(CliffordAlgebra.contractLeft d) (↑(CliffordAlgebra.ι Q) x) = ↑(algebraMap R (CliffordAlgebra Q)) (d x)
      @[simp]
      theorem CliffordAlgebra.contractRight_ι {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (d : Module.Dual R M) (x : M) :
      ↑(CliffordAlgebra.contractRight (↑(CliffordAlgebra.ι Q) x)) d = ↑(algebraMap R (CliffordAlgebra Q)) (d x)
      @[simp]
      theorem CliffordAlgebra.contractLeft_algebraMap {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (d : Module.Dual R M) (r : R) :
      ↑(CliffordAlgebra.contractLeft d) (↑(algebraMap R (CliffordAlgebra Q)) r) = 0
      @[simp]
      theorem CliffordAlgebra.contractRight_algebraMap {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (d : Module.Dual R M) (r : R) :
      ↑(CliffordAlgebra.contractRight (↑(algebraMap R (CliffordAlgebra Q)) r)) d = 0
      @[simp]
      theorem CliffordAlgebra.contractLeft_one {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (d : Module.Dual R M) :
      ↑(CliffordAlgebra.contractLeft d) 1 = 0
      @[simp]
      theorem CliffordAlgebra.contractRight_one {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (d : Module.Dual R M) :
      ↑(CliffordAlgebra.contractRight 1) d = 0
      theorem CliffordAlgebra.contractLeft_contractLeft {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (d : Module.Dual R M) (x : CliffordAlgebra Q) :
      ↑(CliffordAlgebra.contractLeft d) (↑(CliffordAlgebra.contractLeft d) x) = 0

      This is [grinberg_clifford_2016][] Theorem 7

      theorem CliffordAlgebra.contractRight_contractRight {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (d : Module.Dual R M) (x : CliffordAlgebra Q) :
      ↑(CliffordAlgebra.contractRight (↑(CliffordAlgebra.contractRight x) d)) d = 0

      This is [grinberg_clifford_2016][] Theorem 13

      theorem CliffordAlgebra.contractLeft_comm {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (d : Module.Dual R M) (d' : Module.Dual R M) (x : CliffordAlgebra Q) :
      ↑(CliffordAlgebra.contractLeft d) (↑(CliffordAlgebra.contractLeft d') x) = -↑(CliffordAlgebra.contractLeft d') (↑(CliffordAlgebra.contractLeft d) x)

      This is [grinberg_clifford_2016][] Theorem 8

      theorem CliffordAlgebra.contractRight_comm {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (d : Module.Dual R M) (d' : Module.Dual R M) (x : CliffordAlgebra Q) :
      ↑(CliffordAlgebra.contractRight (↑(CliffordAlgebra.contractRight x) d)) d' = -↑(CliffordAlgebra.contractRight (↑(CliffordAlgebra.contractRight x) d')) d

      This is [grinberg_clifford_2016][] Theorem 14

      @[simp]
      theorem CliffordAlgebra.changeFormAux_apply_apply {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (B : BilinForm R M) (a : M) (a : CliffordAlgebra Q) :
      ↑(↑(CliffordAlgebra.changeFormAux Q B) a) a = ↑(CliffordAlgebra.ι Q) a * a - ↑(CliffordAlgebra.contractLeft (↑(BilinForm.toLin B) a)) a

      Auxiliary construction for CliffordAlgebra.changeForm

      Instances For
        theorem CliffordAlgebra.changeFormAux_changeFormAux {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (B : BilinForm R M) (v : M) (x : CliffordAlgebra Q) :
        ↑(↑(CliffordAlgebra.changeFormAux Q B) v) (↑(↑(CliffordAlgebra.changeFormAux Q B) v) x) = (Q v - BilinForm.bilin B v v) x

        Convert between two algebras of different quadratic form, sending vector to vectors, scalars to scalars, and adjusting products by a contraction term.

        This is $\lambda_B$ from [bourbaki2007][] $9 Lemma 2.

        Instances For

          Auxiliary lemma used as an argument to CliffordAlgebra.changeForm

          theorem CliffordAlgebra.changeForm.add_proof {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {Q' : QuadraticForm R M} {Q'' : QuadraticForm R M} {B : BilinForm R M} {B' : BilinForm R M} (h : BilinForm.toQuadraticForm B = Q' - Q) (h' : BilinForm.toQuadraticForm B' = Q'' - Q') :

          Auxiliary lemma used as an argument to CliffordAlgebra.changeForm

          theorem CliffordAlgebra.changeForm.neg_proof {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {Q' : QuadraticForm R M} {B : BilinForm R M} (h : BilinForm.toQuadraticForm B = Q' - Q) :

          Auxiliary lemma used as an argument to CliffordAlgebra.changeForm

          theorem CliffordAlgebra.changeForm.associated_neg_proof {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] :
          BilinForm.toQuadraticForm (QuadraticForm.associated (-Q)) = 0 - Q
          @[simp]
          theorem CliffordAlgebra.changeForm_algebraMap {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {Q' : QuadraticForm R M} {B : BilinForm R M} (h : BilinForm.toQuadraticForm B = Q' - Q) (r : R) :
          @[simp]
          theorem CliffordAlgebra.changeForm_one {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {Q' : QuadraticForm R M} {B : BilinForm R M} (h : BilinForm.toQuadraticForm B = Q' - Q) :
          @[simp]
          theorem CliffordAlgebra.changeForm_ι {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {Q' : QuadraticForm R M} {B : BilinForm R M} (h : BilinForm.toQuadraticForm B = Q' - Q) (m : M) :
          theorem CliffordAlgebra.changeForm_ι_mul {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {Q' : QuadraticForm R M} {B : BilinForm R M} (h : BilinForm.toQuadraticForm B = Q' - Q) (m : M) (x : CliffordAlgebra Q) :
          ↑(CliffordAlgebra.changeForm h) (↑(CliffordAlgebra.ι Q) m * x) = ↑(CliffordAlgebra.ι Q') m * ↑(CliffordAlgebra.changeForm h) x - ↑(CliffordAlgebra.contractLeft (↑(BilinForm.toLin B) m)) (↑(CliffordAlgebra.changeForm h) x)
          theorem CliffordAlgebra.changeForm_ι_mul_ι {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {Q' : QuadraticForm R M} {B : BilinForm R M} (h : BilinForm.toQuadraticForm B = Q' - Q) (m₁ : M) (m₂ : M) :
          ↑(CliffordAlgebra.changeForm h) (↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂) = ↑(CliffordAlgebra.ι Q') m₁ * ↑(CliffordAlgebra.ι Q') m₂ - ↑(algebraMap R (CliffordAlgebra Q')) (BilinForm.bilin B m₁ m₂)
          theorem CliffordAlgebra.changeForm_contractLeft {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {Q' : QuadraticForm R M} {B : BilinForm R M} (h : BilinForm.toQuadraticForm B = Q' - Q) (d : Module.Dual R M) (x : CliffordAlgebra Q) :
          ↑(CliffordAlgebra.changeForm h) (↑(CliffordAlgebra.contractLeft d) x) = ↑(CliffordAlgebra.contractLeft d) (↑(CliffordAlgebra.changeForm h) x)

          Theorem 23 of [grinberg_clifford_2016][]

          @[simp]
          theorem CliffordAlgebra.changeForm_changeForm {R : Type u1} [CommRing R] {M : Type u2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {Q' : QuadraticForm R M} {Q'' : QuadraticForm R M} {B : BilinForm R M} {B' : BilinForm R M} (h : BilinForm.toQuadraticForm B = Q' - Q) (h' : BilinForm.toQuadraticForm B' = Q'' - Q') (x : CliffordAlgebra Q) :

          This is [bourbaki2007][] $9 Lemma 3.

          Any two algebras whose quadratic forms differ by a bilinear form are isomorphic as modules.

          This is $\bar \lambda_B$ from [bourbaki2007][] $9 Proposition 3.

          Instances For

            The module isomorphism to the exterior algebra.

            Note that this holds more generally when Q is divisible by two, rather than only when 1 is divisible by two; but that would be more awkward to use.

            Instances For