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 #

clifford_algebra.involute: the grade involution, negating each basis vector
clifford_algebra.reverse: the grade reversion, reversing the order of a product of vectors

Main statements #

source

def clifford_algebra.involute {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} :

clifford_algebra Q →ₐ[R] clifford_algebra Q

Grade involution, inverting the sign of each basis vector.

Equations

clifford_algebra.involute = ⇑(clifford_algebra.lift Q) ⟨-clifford_algebra.ι Q, _⟩

source

@[simp]

theorem clifford_algebra.involute_ι {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (m : M) :

⇑clifford_algebra.involute (⇑(clifford_algebra.ι Q) m) = -⇑(clifford_algebra.ι Q) m

source

@[simp]

theorem clifford_algebra.involute_comp_involute {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} :

clifford_algebra.involute.comp clifford_algebra.involute = alg_hom.id R (clifford_algebra Q)

source

theorem clifford_algebra.involute_involutive {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} :

function.involutive ⇑clifford_algebra.involute

source

@[simp]

theorem clifford_algebra.involute_involute {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (a : clifford_algebra Q) :

⇑clifford_algebra.involute (⇑clifford_algebra.involute a) = a

source

def clifford_algebra.reverse {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} :

clifford_algebra Q →ₗ[R] clifford_algebra Q

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

Equations

clifford_algebra.reverse = (mul_opposite.op_linear_equiv R).symm.to_linear_map.comp (⇑(clifford_algebra.lift Q) ⟨(mul_opposite.op_linear_equiv R).to_linear_map.comp (clifford_algebra.ι Q), _⟩).to_linear_map

source

@[simp]

theorem clifford_algebra.reverse_ι {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (m : M) :

⇑clifford_algebra.reverse (⇑(clifford_algebra.ι Q) m) = ⇑(clifford_algebra.ι Q) m

source

@[simp]

theorem clifford_algebra.reverse.commutes {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (r : R) :

⇑clifford_algebra.reverse (⇑(algebra_map R (clifford_algebra Q)) r) = ⇑(algebra_map R (clifford_algebra Q)) r

source

@[simp]

theorem clifford_algebra.reverse.map_one {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} :

⇑clifford_algebra.reverse 1 = 1

source

@[simp]

theorem clifford_algebra.reverse.map_mul {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (a b : clifford_algebra Q) :

⇑clifford_algebra.reverse (a * b) = (⇑clifford_algebra.reverse b) * ⇑clifford_algebra.reverse a

source

@[simp]

theorem clifford_algebra.reverse_comp_reverse {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} :

clifford_algebra.reverse.comp clifford_algebra.reverse = linear_map.id

source

@[simp]

theorem clifford_algebra.reverse_involutive {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} :

function.involutive ⇑clifford_algebra.reverse

source

@[simp]

theorem clifford_algebra.reverse_reverse {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (a : clifford_algebra Q) :

⇑clifford_algebra.reverse (⇑clifford_algebra.reverse a) = a

source

theorem clifford_algebra.reverse_comp_involute {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} :

clifford_algebra.reverse.comp clifford_algebra.involute.to_linear_map = clifford_algebra.involute.to_linear_map.comp clifford_algebra.reverse

source

theorem clifford_algebra.reverse_involute_commute {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} :

function.commute ⇑clifford_algebra.reverse ⇑clifford_algebra.involute

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

source

theorem clifford_algebra.reverse_involute {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (a : clifford_algebra Q) :

⇑clifford_algebra.reverse (⇑clifford_algebra.involute a) = ⇑clifford_algebra.involute (⇑clifford_algebra.reverse a)

Statements about conjugations of products of lists #

source

theorem clifford_algebra.reverse_prod_map_ι {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (l : list M) :

⇑clifford_algebra.reverse (list.map ⇑(clifford_algebra.ι Q) l).prod = (list.map ⇑(clifford_algebra.ι 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 clifford_algebra.involute_prod_map_ι {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R M} (l : list M) :

⇑clifford_algebra.involute (list.map ⇑(clifford_algebra.ι Q) l).prod = (-1) ^ l.length • (list.map ⇑(clifford_algebra.ι Q) l).prod

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