English
There is a canonical way to shift left by a and then shift right by a that produces the same result as shifting the original cochain γ by a, up to a sign; this is a core compatibility between left and right shifts.
Русский
Существует канонический способ выполнить сдвиг влево на a, затем сдвиг вправо на a, который даёт тот же результат, что и исходный коцеп γ со сдвигом на a, с учетом знака.
LaTeX
$$$ (\gamma^{\mathrm{leftShift}}(a,n'',hn''))^{\mathrm{rightShift}}(a,n,hn') = (-1)^{an'+a(a-1)/2} \; γ^{\mathrm{shift}}(a). $$$
Lean4
/-- The map `Cocycle K L n → Cocycle (K⟦a⟧) L n'` when `n + a = n'`. -/
@[simps!]
def leftShift (γ : Cocycle K L n) (a n' : ℤ) (hn' : n + a = n') : Cocycle (K⟦a⟧) L n' :=
Cocycle.mk (γ.1.leftShift a n' hn') _ rfl
(by
simp only [Cochain.δ_leftShift _ a n' (n' + 1) hn' (n + 1) (by cutsat), δ_eq_zero, Cochain.leftShift_zero,
smul_zero])
