Conjugations #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 vectorclifford_algebra.reverse: the grade reversion, reversing the order of a product of vectors
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 (⇑(clifford_algebra.ι Q) m) = -⇑(clifford_algebra.ι Q) m
@[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} :
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} :
@[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) :
@[simp]
theorem
clifford_algebra.involute_equiv_symm_apply
{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) :
@[simp]
theorem
clifford_algebra.involute_equiv_apply
{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) :
def
clifford_algebra.involute_equiv
{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 as an alg_equiv.
Equations
- clifford_algebra.involute_equiv = alg_equiv.of_alg_hom clifford_algebra.involute clifford_algebra.involute clifford_algebra.involute_equiv._proof_1 clifford_algebra.involute_equiv._proof_2
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.
@[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
@[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
@[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} :
@[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) :
@[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} :
@[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} :
@[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) :
def
clifford_algebra.reverse_equiv
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M} :
@[simp]
theorem
clifford_algebra.reverse_equiv_symm_apply
{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) :
@[simp]
theorem
clifford_algebra.reverse_equiv_apply
{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) :
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} :
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} :
clifford_algebra.reverse and clifford_algebra.inverse commute. Note that the composition
is sometimes referred to as the "clifford conjugate".
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) :
Statements about conjugations of products of lists #
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.
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$.
Statements about submodule.map and submodule.comap #
theorem
clifford_algebra.submodule_map_involute_eq_comap
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(p : submodule R (clifford_algebra Q)) :
@[simp]
theorem
clifford_algebra.ι_range_map_involute
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
@[simp]
theorem
clifford_algebra.ι_range_comap_involute
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
@[simp]
theorem
clifford_algebra.even_odd_map_involute
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(n : zmod 2) :
@[simp]
theorem
clifford_algebra.even_odd_comap_involute
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(n : zmod 2) :
theorem
clifford_algebra.submodule_map_reverse_eq_comap
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(p : submodule R (clifford_algebra Q)) :
@[simp]
theorem
clifford_algebra.ι_range_map_reverse
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
@[simp]
theorem
clifford_algebra.ι_range_comap_reverse
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
theorem
clifford_algebra.submodule_map_mul_reverse
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(p q : submodule R (clifford_algebra Q)) :
Like submodule.map_mul, but with the multiplication reversed.
theorem
clifford_algebra.submodule_comap_mul_reverse
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(p q : submodule R (clifford_algebra Q)) :
theorem
clifford_algebra.submodule_map_pow_reverse
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(p : submodule R (clifford_algebra Q))
(n : ℕ) :
Like submodule.map_pow
theorem
clifford_algebra.submodule_comap_pow_reverse
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(p : submodule R (clifford_algebra Q))
(n : ℕ) :
@[simp]
theorem
clifford_algebra.even_odd_map_reverse
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(n : zmod 2) :
@[simp]
theorem
clifford_algebra.even_odd_comap_reverse
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(n : zmod 2) :
@[simp]
theorem
clifford_algebra.involute_mem_even_odd_iff
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
{x : clifford_algebra Q}
{n : zmod 2} :
@[simp]
theorem
clifford_algebra.reverse_mem_even_odd_iff
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
{x : clifford_algebra Q}
{n : zmod 2} :
Related properties of the even and odd submodules #
TODO: show that these are iffs when invertible (2 : R).
theorem
clifford_algebra.involute_eq_of_mem_even
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
{x : clifford_algebra Q}
(h : x ∈ clifford_algebra.even_odd Q 0) :
theorem
clifford_algebra.involute_eq_of_mem_odd
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
{x : clifford_algebra Q}
(h : x ∈ clifford_algebra.even_odd Q 1) :