English
The homotopy category equipped with ShiftSequence by integers admits a natural linear structure compatible with homology and shift operations.
Русский
Гомотопическая категория, оснащенная ShiftSequence по целым числам, обладает естественной линейной структурой, совместимой с гомологией и сдвигами.
LaTeX
$$$((\\mathrm{HomotopyCategory}.SHIFT)\\mathbb{Z})$ is a ShiftSequence on the homotopy category with natural compatibility to homology.$$
Lean4
@[reassoc]
theorem homologyFunctor_shiftMap {K L : CochainComplex C ℤ} {n : ℤ} (f : K ⟶ L⟦n⟧) (a a' : ℤ) (h : n + a = a') :
(homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap
((quotient _ _).map f ≫ ((quotient _ _).commShiftIso n).hom.app _) a a' h =
(homologyFunctorFactors _ _ a).hom.app K ≫
(HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h ≫
(homologyFunctorFactors _ _ a').inv.app L :=
by apply Functor.ShiftSequence.induced_shiftMap
