mathlib documentation

linear_algebra.clifford_algebra.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 #

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

Grade involution, inverting the sign of each basis vector.

Equations
@[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 as an alg_equiv.

Equations
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} :

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

Equations
@[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) :
@[simp]
@[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 and clifford_algebra.inverse commute. Note that the composition is sometimes referred to as the "clifford conjugate".

Statements about conjugations of products of lists #

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.

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 #

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