commShiftQuotient — Mathlib

English

The quotient of the homotopy category by homotopy inherits a shift by integers, i.e., there is a canonical shift-structure on the quotient category compatible with the base shift.

Русский

Куотируемая гомотопическая категория по отношению к гомотопии наследует сдвиг на целые; существует каноническая структура сдвига на квотиентной категории, совместимая с базовым сдвигом.

LaTeX

$$$\\big( \\mathrm{HomotopyCategory.quotient}(C, \\mathrm{ComplexShape.up} \\mathbb{Z}) \\big).\\mathrm{CommShift} \\mathbb{Z}$$$$

Lean4

noncomputable instance commShiftQuotient : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).CommShift ℤ :=
  Quotient.functor_commShift (homotopic C (ComplexShape.up ℤ)) ℤ

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