hasShift — Mathlib

English

There exists a shift by integers on the Homotopy category: for each integer n, there is an endofunctor shifting objects and morphisms by n in the ℤ-graded indexing.

Русский

Существует сдвиг по целым числам на гомотопической категории: для каждого целого числа n существует концевой функтор, сдвигающий объекты и морфизмы по индексации ℤ.

LaTeX

$$$\\exists \\text{Shift}_n : \\mathrm{Ho}(C, \\mathrm{ComplexShape.up} \\mathbb{Z}) \\to \\mathrm{Ho}(C, \\mathrm{ComplexShape.up} \\mathbb{Z}) \\\\text{for all } n \\in \\mathbb{Z}$$$

Lean4

noncomputable instance hasShift : HasShift (HomotopyCategory C (ComplexShape.up ℤ)) ℤ :=
  by
  dsimp only [HomotopyCategory]
  infer_instance

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