instIsCompatibleWithShiftHomologicalComplexIntUpQuasiIso

English

The shift by integers is compatible with the HomologicalComplex structure on CochainComplex, giving a coherent shift by ℤ of homology functors.

Русский

Сдвиг по целым совместим с структурой гомологических комплексов на CochainComplex, обеспечивая согласованный сдвиг по ℤ функций гомологии.

LaTeX

$$$\\text{IsCompatibleWithShift}_{\\mathbb{Z}}(\\mathrm{HomologicalComplex}, \\mathrm{CochainComplex})$$$

Lean4

instance : (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)).IsCompatibleWithShift ℤ where
  condition n := by ext; apply quasiIso_shift_iff

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