instShiftSequenceIntUpHomologyFunctorOfNat

English

The homology shift map is compatible with quotient and shifted functors, relating homology maps after quotienting and shifting.

Русский

Сдвиг гомологии совместим с отображениями после квотирования и сдвигами функторов, связывая отображения гомологии после квотирования и сдвига.

LaTeX

$$$\\text{homologyShiftIso}_\\mathrm{app} : \\mathrm{…}$$$

Lean4

noncomputable instance : (homologyFunctor C (ComplexShape.up ℤ) 0).ShiftSequence ℤ :=
  Functor.ShiftSequence.induced (homologyFunctorFactors C (ComplexShape.up ℤ) 0) ℤ
    (homologyFunctor C (ComplexShape.up ℤ)) (homologyFunctorFactors C (ComplexShape.up ℤ))

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