instIsCompatibleWithShiftHomologicalComplexIntUpHomotopic

English

Shifting a homotopy by an integer n yields a homotopy between the shifted morphisms; the shift operator is compatible with the homotopy relation in the homotopy category.

Русский

Сдвиг гомотопии на целое число n даёт гомотопию между сдвинутыми морфизмами; сдвиг совместим с отношением гомотопии в гомотопической категории.

LaTeX

$$$\\forall C \\; \\forall n \\in \\mathbb{Z}, \\; \\forall h:\\ f \\simeq g, \\; h^{(n)}:\\ f^{(n)} \\simeq g^{(n)}$$$

Lean4

instance : (homotopic C (ComplexShape.up ℤ)).IsCompatibleWithShift ℤ :=
  ⟨fun n _ _ _ _ ⟨h⟩ => ⟨h.shift n⟩⟩

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