instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso

English

There is a natural commShift between the homological functor in the quotient setting and its shifted version; compatibility of shifts with quotient/QuasiIso data is established.

Русский

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

LaTeX

$$$\mathrm{NatTrans.CommShift}\bigl((\text{quotientCompQhIso } C).\mathrm{hom}\bigr)\; \mathbb{Z} \text{ exists and is compatible with shifts}$$$

Lean4

instance : NatTrans.CommShift (quotientCompQhIso C).hom ℤ :=
  Functor.CommShift.ofIso_compatibility (quotientCompQhIso C) ℤ

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