English
There is a natural isomorphism identifying the evaluation after a shift with the evaluation at the shifted index.
Русский
Существуют естественные изоморфизмы, идентифицирующие оценку после сдвига с оценкой в смещённом индексе.
LaTeX
$$$$ \mathrm{shiftEval}(n,i,i',h i) : \ (\mathrm{Shift}(C, n) \circ \mathrm{eval}(C, i)) \cong \mathrm{eval}(C, i'). $$$$
Lean4
/-- Shifting cochain complexes by `n` and evaluating in a degree `i` identifies
to the evaluation in degree `i'` when `n + i = i'`. -/
@[simps!]
def shiftEval (n i i' : ℤ) (hi : n + i = i') :
(CategoryTheory.shiftFunctor (CochainComplex C ℤ) n) ⋙ HomologicalComplex.eval C (ComplexShape.up ℤ) i ≅
HomologicalComplex.eval C (ComplexShape.up ℤ) i' :=
NatIso.ofComponents (fun K => K.XIsoOfEq (by dsimp; rw [← hi, add_comm i])) (by simp)
