English
For an additive functor F, the induced map on the homotopy category commutes with shifting by integers, i.e., there is a natural CommShift structure on the corresponding map between homotopy categories.
Русский
Для аддитивного Функтора F существeт естественная структура CommShift на соответствующую отображение между гомотопическими категориями, и оно коммутирует с сдвигами на целые.
LaTeX
$$$\\text{NatTrans.CommShift} (F.mapHomotopyCategory (\\mathrm{ComplexShape.up} \\mathbb{Z})).hom \\mathbb{Z}$$$
Lean4
theorem shiftIso_hom_app (n a a' : ℤ) (ha' : n + a = a') (K : CochainComplex C ℤ) :
(shiftIso C n a a' ha').hom.app K =
ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').hom.app K) :=
by
dsimp [shiftIso]
rw [id_comp, id_comp]
-- This `erw` is required to bridge the gap between
-- `((shortComplexFunctor C (up ℤ) a').obj K).homology`
-- (the target of the first morphism)
-- and
-- `homology K a'`
-- (the source of the identity morphism).
erw [comp_id]
