English
There is a natural isomorphism between the shifted homology functor and the homology functor with updated index; the shift respects homology.
Русский
Существует естественная изоморфия между сдвигом гомологий и гомологией с обновленным индексом; сдвиг сохраняет гомологию.
LaTeX
$$$ (\\mathrm{shiftIso} C n a a' : \\; (\\mathrm{shiftFunctor} \\;n) \\circ \\mathrm{homologyFunctor} C (\\mathrm{up} \\mathbb{Z}) a \\cong \\mathrm{homologyFunctor} C (\\mathrm{up} \\mathbb{Z}) a' )$ при $a' = a+n$$$
Lean4
/-- The natural isomorphism `(K⟦n⟧).homology a ≅ K.homology a'`when `n + a = a`. -/
noncomputable def shiftIso (n a a' : ℤ) (ha' : n + a = a') :
(CategoryTheory.shiftFunctor _ n) ⋙ homologyFunctor C (ComplexShape.up ℤ) a ≅
homologyFunctor C (ComplexShape.up ℤ) a' :=
Functor.isoWhiskerLeft _ (homologyFunctorIso C (ComplexShape.up ℤ) a) ≪≫
(Functor.associator _ _ _).symm ≪≫
Functor.isoWhiskerRight (shiftShortComplexFunctorIso C n a a' ha') (ShortComplex.homologyFunctor C) ≪≫
(homologyFunctorIso C (ComplexShape.up ℤ) a').symm
