instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors

English

The shift associating quasi-isomorphisms is compatible with the shift by integers: shifting a quasi-isomorphism yields a quasi-isomorphism.

Русский

Сдвиг, сохраняющий квазиизоморфизм, совместим со сдвигом на целые: сдвиг квазиизоморфизма остаётся квазиизоморфизмом.

LaTeX

$$$\\forall \\text{φ}, n\\;\\mathrm{QuasiIso}(φ) \\Rightarrow \\mathrm{QuasiIso}(φ⟦n⟧')$$$

Lean4

instance : NatTrans.CommShift (F.mapHomotopyCategoryFactors (ComplexShape.up ℤ)).hom ℤ :=
  Quotient.liftCommShift_compatibility _ _ _ _

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