English
Let d and d' be dual vectors in the dual space M*, with the left contraction operation defined on the Clifford algebra. Then for all x in CliffordAlgebra Q we have d ⌟ (d' ⌟ x) = − (d' ⌟ (d ⌟ x)); in other words, left contractions anti-commute up to a sign.
Русский
Пусть d и d' — двойственные векторы в двойственом пространстве M*, и определена операция левого сжатия на клиффордовой алгебре. Тогда для всякого x в CliffordAlgebra Q выполняется d ⌟(d' ⌟ x) = −(d' ⌟(d ⌟ x)); то есть операции сжатий anti- commute
LaTeX
$$$ d \\lrcorner (d' \\lrcorner x) = -\\bigl(d'\\lrcorner (d \\lrcorner x)\\bigr) $$$
Lean4
/-- This is [grinberg_clifford_2016][] Theorem 8 -/
theorem contractLeft_comm (x : CliffordAlgebra Q) : d⌋(d'⌋x) = -(d'⌋(d⌋x)) := by
induction x using CliffordAlgebra.left_induction with
| algebraMap => simp_rw [contractLeft_algebraMap, map_zero, neg_zero]
| add _ _ hx hy => rw [map_add, map_add, map_add, map_add, hx, hy, neg_add]
| ι_mul _ _ hx =>
simp only [contractLeft_ι_mul, map_sub, LinearMap.map_smul]
rw [neg_sub, sub_sub_eq_add_sub, hx, mul_neg, ← sub_eq_add_neg]
