English
Let γ be a cocycle; applying a left shift and then a right shift yields γ shifted by a, multiplied by the sign factor (-1)^{an'+a(a−1)/2}, demonstrating a sign-controlled commutation between shifts.
Русский
Пусть γ — кокцикл; последовательное применение левого сдвига и правого сдвига даёт γ сдвинутый на a, умноженный на знак (-1)^{an'+a(a−1)/2}, что демонстрирует.sign-управляемое согласование сдвигов.
LaTeX
$$$ (\gamma^{\mathrm{leftShift}}(a,n',hn'))^{\mathrm{rightShift}}(a,n,hn') = (-1)^{a\,n' + \frac{a(a-1)}{2}} \, γ^{\mathrm{shift}}(a). $$$
Lean4
/-- The left and right shift of cochains commute only up to a sign. -/
theorem leftShift_rightShift_eq_negOnePow_rightShift_leftShift (a n' n'' : ℤ) (hn' : n' + a = n) (hn'' : n + a = n'') :
(γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn'' := by
rw [leftShift_rightShift, rightShift_leftShift, smul_smul, ← hn'', add_comm n a, mul_add, Int.negOnePow_add,
Int.negOnePow_add, Int.negOnePow_add, Int.negOnePow_mul_self, ← mul_assoc, ← mul_assoc, Int.units_mul_self, one_mul]
