English
There is a canonical additive equivalence between Cochain K L n and Cochain K (L⟦a⟧) n' when n' + a = n, implemented by rightShift and rightUnshift. This equivalence preserves addition.
Русский
Существует каноническая аддитивная эквивалентность между Cochain(K,L,n) и Cochain(K, L⟦a⟧, n'), когда n' + a = n, реализованная rightShift и rightUnshift. Она сохраняет сложение.
LaTeX
$$$\\text{rightShiftAddEquiv}(n,a,n',hn'):\\; \\text{Cochain}(K,L,n) \\simeq_+ \\text{Cochain}(K,(L⟦a⟧),n'),\\; \\gamma \\mapsto \\gamma.rightShift a n' hn',\\; \\text{inv}=\\gamma.rightUnshift n hn',$$$
Lean4
/-- The additive equivalence `Cochain K L n ≃+ Cochain K L⟦a⟧ n'` when `n' + a = n`. -/
@[simps]
def rightShiftAddEquiv (n a n' : ℤ) (hn' : n' + a = n) : Cochain K L n ≃+ Cochain K (L⟦a⟧) n'
where
toFun γ := γ.rightShift a n' hn'
invFun γ := γ.rightUnshift n hn'
left_inv γ := by simp only [rightUnshift_rightShift]
right_inv γ := by simp only [rightShift_rightUnshift]
map_add' γ γ' := by simp only [rightShift_add]
