English
There is a canonical isomorphism between the shifted cochain complex functor and the short complex functor with updated indices; this isomorphism is natural in the complexes involved.
Русский
Существует каноническая изоморфия между сдвиговым функтором и функтором короткого комплексa с обновлёнными индексами; изоморфия естественна по всем компонентам.
LaTeX
$$$ (\\mathrm{shiftFunctor} C n)\\;\\circ\\; \\mathrm{shortComplexFunctor}' C i j k \\cong \\mathrm{shortComplexFunctor}' C i' j' k' $ при соответствующих отношениях между n,i,i',j,j',k,k'$$
Lean4
/-- The natural isomorphism `(K⟦n⟧).sc i ≅ K.sc i'` when `n + i = i'`. -/
@[simps!]
noncomputable def shiftShortComplexFunctorIso (n i i' : ℤ) (hi : n + i = i') :
shiftFunctor C n ⋙ shortComplexFunctor C _ i ≅ shortComplexFunctor C _ i' :=
shiftShortComplexFunctor' C n _ i _ _ i' _ (by simp only [prev]; cutsat) hi (by simp only [next]; cutsat)
