English
Let γ be a degree n cochain between K and L in a preadditive category. If we first apply a right shift by an integer a and then a left shift by the same a, the result equals the original shift γ shifted by a, multiplied by the sign (-1)^{a n + a(a−1)/2}. This expresses that the left and right shifts commute up to a sign depending on a and n.
Русский
Пусть γ — коцепнь степени n между K и L в преддобавной категории. Если выполнить правый сдвиг на целое a, затем левый сдвиг на то же a, получаем тот же результат, что и сдвиг γ на a, умноженный на знак (−1)^{a n + a(a−1)/2}. Это выражение говорит, что левые и правые сдвиги коммутируют с учетом знака, зависящего от a и n.
LaTeX
$$$ (\gamma^{\mathrm{rightShift}}(a,n',hn'))^{\mathrm{leftShift}}(a,n,hn') = (-1)^{a\,n + \frac{a(a-1)}{2}} \; \gamma^{\mathrm{shift}}(a). $$$
Lean4
theorem leftShift_rightShift (a n' : ℤ) (hn' : n' + a = n) :
(γ.rightShift a n' hn').leftShift a n hn' = (a * n + (a * (a - 1)) / 2).negOnePow • γ.shift a :=
by
ext p q hpq
simp only [leftShift_v _ a n hn' p q hpq (p + a) (by cutsat),
rightShift_v _ a n' hn' (p + a) q (by cutsat) (q + a) (by cutsat), units_smul_v, shift_v']
dsimp
rw [id_comp, comp_id]
