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 #

Grade involution, inverting the sign of each basis vector.

Instances For
    @[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) :
    CliffordAlgebra.involute (↑(CliffordAlgebra.ι Q) m) = -↑(CliffordAlgebra.ι Q) m
    @[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} :
    AlgHom.comp CliffordAlgebra.involute CliffordAlgebra.involute = AlgHom.id R (CliffordAlgebra Q)
    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 CliffordAlgebra.involute
    @[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) :
    CliffordAlgebra.involute (CliffordAlgebra.involute a) = a
    @[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) :
    ↑(AlgEquiv.symm CliffordAlgebra.involuteEquiv) a = CliffordAlgebra.involute a
    @[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) :
    CliffordAlgebra.involuteEquiv a = CliffordAlgebra.involute a

    CliffordAlgebra.reverse as an AlgHom to the opposite algebra

    Instances For
      @[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) :
      CliffordAlgebra.reverseOp (↑(CliffordAlgebra.ι Q) m) = MulOpposite.op (↑(CliffordAlgebra.ι Q) m)
      @[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) :
      CliffordAlgebra.reverseOpEquiv a = CliffordAlgebra.reverseOp a
      @[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 CliffordAlgebra.reverseOpEquiv = AlgEquiv.symm CliffordAlgebra.reverseOpEquiv

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

      Instances For
        @[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 (CliffordAlgebra.reverseOp x) = CliffordAlgebra.reverse x
        @[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 (CliffordAlgebra.reverse x) = CliffordAlgebra.reverseOp x
        @[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) :
        CliffordAlgebra.reverse (↑(CliffordAlgebra.ι Q) m) = ↑(CliffordAlgebra.ι Q) m
        @[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) :
        CliffordAlgebra.reverse (↑(algebraMap R (CliffordAlgebra Q)) r) = ↑(algebraMap R (CliffordAlgebra Q)) r
        @[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} :
        CliffordAlgebra.reverse 1 = 1
        @[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 : CliffordAlgebra Q) (b : CliffordAlgebra Q) :
        CliffordAlgebra.reverse (a * b) = CliffordAlgebra.reverse b * CliffordAlgebra.reverse a
        @[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 CliffordAlgebra.reverse
        @[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} :
        LinearMap.comp CliffordAlgebra.reverse CliffordAlgebra.reverse = LinearMap.id
        @[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) :
        CliffordAlgebra.reverse (CliffordAlgebra.reverse a) = a
        @[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), CliffordAlgebra.reverseEquiv a = CliffordAlgebra.reverse a
        @[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), ↑(LinearEquiv.symm CliffordAlgebra.reverseEquiv) a = CliffordAlgebra.reverse a
        theorem CliffordAlgebra.reverse_comp_involute {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
        LinearMap.comp CliffordAlgebra.reverse (AlgHom.toLinearMap CliffordAlgebra.involute) = LinearMap.comp (AlgHom.toLinearMap CliffordAlgebra.involute) CliffordAlgebra.reverse
        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 CliffordAlgebra.reverse CliffordAlgebra.involute

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

        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) :
        CliffordAlgebra.reverse (CliffordAlgebra.involute a) = CliffordAlgebra.involute (CliffordAlgebra.reverse a)

        Statements about conjugations of products of lists #

        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) :
        CliffordAlgebra.reverse (List.prod (List.map (↑(CliffordAlgebra.ι Q)) l)) = List.prod (List.reverse (List.map (↑(CliffordAlgebra.ι Q)) l))

        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.

        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) :
        CliffordAlgebra.involute (List.prod (List.map (↑(CliffordAlgebra.ι Q)) l)) = (-1) ^ List.length l List.prod (List.map (↑(CliffordAlgebra.ι Q)) l)

        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 #

        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 (AlgHom.toLinearMap CliffordAlgebra.involute) p = Submodule.comap (AlgHom.toLinearMap CliffordAlgebra.involute) p
        @[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) :
        @[simp]
        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 CliffordAlgebra.reverse p = Submodule.comap CliffordAlgebra.reverse p
        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 : Submodule R (CliffordAlgebra Q)) (q : Submodule R (CliffordAlgebra Q)) :
        Submodule.map CliffordAlgebra.reverse (p * q) = Submodule.map CliffordAlgebra.reverse q * Submodule.map CliffordAlgebra.reverse p

        Like Submodule.map_mul, but with the multiplication reversed.

        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 : Submodule R (CliffordAlgebra Q)) (q : Submodule R (CliffordAlgebra Q)) :
        Submodule.comap CliffordAlgebra.reverse (p * q) = Submodule.comap CliffordAlgebra.reverse q * Submodule.comap CliffordAlgebra.reverse p
        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 CliffordAlgebra.reverse (p ^ n) = Submodule.map CliffordAlgebra.reverse p ^ n

        Like Submodule.map_pow

        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 CliffordAlgebra.reverse (p ^ n) = Submodule.comap CliffordAlgebra.reverse p ^ n
        @[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) :
        @[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) :
        @[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} :
        CliffordAlgebra.involute x CliffordAlgebra.evenOdd Q n x CliffordAlgebra.evenOdd Q n
        @[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} :
        CliffordAlgebra.reverse x CliffordAlgebra.evenOdd Q n x CliffordAlgebra.evenOdd Q n

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

        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 CliffordAlgebra.evenOdd Q 0) :
        CliffordAlgebra.involute x = x
        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 CliffordAlgebra.evenOdd Q 1) :
        CliffordAlgebra.involute x = -x