Documentation

Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

Conjugations #

This file defines the grade reversal and grade involution functions on multivectors, reverse and involute. Together, these operations compose to form the "Clifford conjugate", hence the name of this file.

https://en.wikipedia.org/wiki/Clifford_algebra#Antiautomorphisms

Main definitions #

Main statements #

source
def CliffordAlgebra.involute {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
CliffordAlgebra Q →ₐ[R] CliffordAlgebra Q

Grade involution, inverting the sign of each basis vector.

Equations
Instances For
    source
    @[simp]
    theorem CliffordAlgebra.involute_ι {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (m : M) :
    involute ((ι Q) m) = -(ι Q) m
    source
    @[simp]
    theorem CliffordAlgebra.involute_comp_involute {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
    involute.comp involute = AlgHom.id R (CliffordAlgebra Q)
    source
    theorem CliffordAlgebra.involute_involutive {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
    Function.Involutive ⇑involute
    source
    @[simp]
    theorem CliffordAlgebra.involute_involute {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (a : CliffordAlgebra Q) :
    involute (involute a) = a
    source
    def CliffordAlgebra.involuteEquiv {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
    CliffordAlgebra Q ≃ₐ[R] CliffordAlgebra Q

    CliffordAlgebra.involute as an AlgEquiv.

    Equations
    Instances For
      source
      @[simp]
      theorem CliffordAlgebra.involuteEquiv_symm_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (a : CliffordAlgebra Q) :
      involuteEquiv.symm a = involute a
      source
      @[simp]
      theorem CliffordAlgebra.involuteEquiv_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (a : CliffordAlgebra Q) :
      involuteEquiv a = involute a
      source
      def CliffordAlgebra.reverseOp {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
      CliffordAlgebra Q →ₐ[R] (CliffordAlgebra Q)ᵐᵒᵖ

      CliffordAlgebra.reverse as an AlgHom to the opposite algebra

      Equations
      Instances For
        source
        @[simp]
        theorem CliffordAlgebra.reverseOp_ι {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (m : M) :
        reverseOp ((ι Q) m) = MulOpposite.op ((ι Q) m)
        source
        def CliffordAlgebra.reverseOpEquiv {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
        CliffordAlgebra Q ≃ₐ[R] (CliffordAlgebra Q)ᵐᵒᵖ

        CliffordAlgebra.reverseEquiv as an AlgEquiv to the opposite algebra

        Equations
        Instances For
          source
          @[simp]
          theorem CliffordAlgebra.reverseOpEquiv_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (a : CliffordAlgebra Q) :
          reverseOpEquiv a = reverseOp a
          source
          @[simp]
          theorem CliffordAlgebra.reverseOpEquiv_opComm {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
          AlgEquiv.opComm reverseOpEquiv = reverseOpEquiv.symm
          source
          def CliffordAlgebra.reverse {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
          CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q

          Grade reversion, inverting the multiplication order of basis vectors. Also called transpose in some literature.

          Equations
          Instances For
            source
            @[simp]
            theorem CliffordAlgebra.unop_reverseOp {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : CliffordAlgebra Q) :
            MulOpposite.unop (reverseOp x) = reverse x
            source
            @[simp]
            theorem CliffordAlgebra.op_reverse {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : CliffordAlgebra Q) :
            MulOpposite.op (reverse x) = reverseOp x
            source
            @[simp]
            theorem CliffordAlgebra.reverse_ι {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (m : M) :
            reverse ((ι Q) m) = (ι Q) m
            source
            @[simp]
            theorem CliffordAlgebra.reverse.commutes {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (r : R) :
            reverse ((algebraMap R (CliffordAlgebra Q)) r) = (algebraMap R (CliffordAlgebra Q)) r
            source
            @[simp]
            theorem CliffordAlgebra.reverse.map_one {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
            reverse 1 = 1
            source
            @[simp]
            theorem CliffordAlgebra.reverse.map_mul {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (a b : CliffordAlgebra Q) :
            reverse (a * b) = reverse b * reverse a
            source
            @[simp]
            theorem CliffordAlgebra.reverse_involutive {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
            Function.Involutive ⇑reverse
            source
            @[simp]
            theorem CliffordAlgebra.reverse_comp_reverse {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
            reverse ∘ₗ reverse = LinearMap.id
            source
            @[simp]
            theorem CliffordAlgebra.reverse_reverse {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (a : CliffordAlgebra Q) :
            reverse (reverse a) = a
            source
            def CliffordAlgebra.reverseEquiv {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
            CliffordAlgebra Q ≃ₗ[R] CliffordAlgebra Q

            CliffordAlgebra.reverse as a LinearEquiv.

            Equations
            Instances For
              source
              @[simp]
              theorem CliffordAlgebra.reverseEquiv_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (a✝ : CliffordAlgebra Q) :
              reverseEquiv a✝ = reverse a✝
              source
              @[simp]
              theorem CliffordAlgebra.reverseEquiv_symm_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (a✝ : CliffordAlgebra Q) :
              reverseEquiv.symm a✝ = reverse a✝
              source
              theorem CliffordAlgebra.reverse_comp_involute {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
              reverse ∘ₗ involute.toLinearMap = involute.toLinearMap ∘ₗ reverse
              source
              theorem CliffordAlgebra.reverse_involute_commute {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
              Function.Commute ⇑reverse ⇑involute

              CliffordAlgebra.reverse and CliffordAlgebra.involute commute. Note that the composition is sometimes referred to as the "clifford conjugate".

              source
              theorem CliffordAlgebra.reverse_involute {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (a : CliffordAlgebra Q) :
              reverse (involute a) = involute (reverse a)

              Statements about conjugations of products of lists #

              source
              theorem CliffordAlgebra.reverse_prod_map_ι {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (l : List M) :
              reverse (List.map (⇑(ι Q)) l).prod = (List.map (⇑(ι Q)) l).reverse.prod

              Taking the reverse of the product a list of $n$ vectors lifted via ι is equivalent to taking the product of the reverse of that list.

              source
              theorem CliffordAlgebra.involute_prod_map_ι {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (l : List M) :
              involute (List.map (⇑(ι Q)) l).prod = (-1) ^ l.length • (List.map (⇑(ι Q)) l).prod

              Taking the involute of the product a list of $n$ vectors lifted via ι is equivalent to premultiplying by ${-1}^n$.

              Statements about Submodule.map and Submodule.comap #

              source
              theorem CliffordAlgebra.submodule_map_involute_eq_comap {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (p : Submodule R (CliffordAlgebra Q)) :
              Submodule.map involute.toLinearMap p = Submodule.comap involute.toLinearMap p
              source
              @[simp]
              theorem CliffordAlgebra.ι_range_map_involute {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :
              Submodule.map involute.toLinearMap (LinearMap.range (ι Q)) = LinearMap.range (ι Q)
              source
              @[simp]
              theorem CliffordAlgebra.ι_range_comap_involute {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :
              Submodule.comap involute.toLinearMap (LinearMap.range (ι Q)) = LinearMap.range (ι Q)
              source
              @[simp]
              theorem CliffordAlgebra.evenOdd_map_involute {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (n : ZMod 2) :
              Submodule.map involute.toLinearMap (evenOdd Q n) = evenOdd Q n
              source
              @[simp]
              theorem CliffordAlgebra.evenOdd_comap_involute {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (n : ZMod 2) :
              Submodule.comap involute.toLinearMap (evenOdd Q n) = evenOdd Q n
              source
              theorem CliffordAlgebra.submodule_map_reverse_eq_comap {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (p : Submodule R (CliffordAlgebra Q)) :
              Submodule.map reverse p = Submodule.comap reverse p
              source
              @[simp]
              theorem CliffordAlgebra.ι_range_map_reverse {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :
              Submodule.map reverse (LinearMap.range (ι Q)) = LinearMap.range (ι Q)
              source
              @[simp]
              theorem CliffordAlgebra.ι_range_comap_reverse {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :
              Submodule.comap reverse (LinearMap.range (ι Q)) = LinearMap.range (ι Q)
              source
              theorem CliffordAlgebra.submodule_map_mul_reverse {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (p q : Submodule R (CliffordAlgebra Q)) :
              Submodule.map reverse (p * q) = Submodule.map reverse q * Submodule.map reverse p

              Like Submodule.map_mul, but with the multiplication reversed.

              source
              theorem CliffordAlgebra.submodule_comap_mul_reverse {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (p q : Submodule R (CliffordAlgebra Q)) :
              Submodule.comap reverse (p * q) = Submodule.comap reverse q * Submodule.comap reverse p
              source
              theorem CliffordAlgebra.submodule_map_pow_reverse {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (p : Submodule R (CliffordAlgebra Q)) (n : ℕ) :
              Submodule.map reverse (p ^ n) = Submodule.map reverse p ^ n

              Like Submodule.map_pow

              source
              theorem CliffordAlgebra.submodule_comap_pow_reverse {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (p : Submodule R (CliffordAlgebra Q)) (n : ℕ) :
              Submodule.comap reverse (p ^ n) = Submodule.comap reverse p ^ n
              source
              @[simp]
              theorem CliffordAlgebra.evenOdd_map_reverse {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (n : ZMod 2) :
              Submodule.map reverse (evenOdd Q n) = evenOdd Q n
              source
              @[simp]
              theorem CliffordAlgebra.evenOdd_comap_reverse {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (n : ZMod 2) :
              Submodule.comap reverse (evenOdd Q n) = evenOdd Q n
              source
              @[simp]
              theorem CliffordAlgebra.involute_mem_evenOdd_iff {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {x : CliffordAlgebra Q} {n : ZMod 2} :
              involute x ∈ evenOdd Q n ↔ x ∈ evenOdd Q n
              source
              @[simp]
              theorem CliffordAlgebra.reverse_mem_evenOdd_iff {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {x : CliffordAlgebra Q} {n : ZMod 2} :
              reverse x ∈ evenOdd Q n ↔ x ∈ evenOdd Q n

              TODO: show that these are iffs when Invertible (2 : R).

              source
              theorem CliffordAlgebra.involute_eq_of_mem_even {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} (h : x ∈ evenOdd Q 0) :
              involute x = x
              source
              theorem CliffordAlgebra.involute_eq_of_mem_odd {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} (h : x ∈ evenOdd Q 1) :
              involute x = -x