instShiftSequenceHomologyFunctorOfNatInt

English

The functors in the homology sequence are compatible with shifts; they form a shift sequence around degree zero.

Русский

Функторы в гомологической последовательности совместимы со сдвигами; образуют последовательность сдвигов вокруг нулевого слоя.

LaTeX

$$$\\text{homologyFunctor } C\\,0 \\;\\text{ShiftSequence} \\mathbb{Z} \\to \\text{homologyFunctor } C n$$$

Lean4

/-- The functors `homologyFunctor C n : DerivedCategory C ⥤ C` for all `n : ℤ` are part
of a "shift sequence", i.e. they satisfy compatibilities with shifts. -/
noncomputable instance : (homologyFunctor C 0).ShiftSequence ℤ :=
  Functor.ShiftSequence.induced (homologyFunctorFactorsh C 0) ℤ (homologyFunctor C) (homologyFunctorFactorsh C)

Похожие утверждения