instCommShiftCochainComplexIntQ — Mathlib

English

There is a commutative shift structure of the derived category by ℤ, i.e., a natural commutation of shifts by integers with the functor structure.

Русский

Существует структура коммутативного сдвига производной категории по ℤ: естественное commute-сдвигов по целым с сохранением функторной структуры.

LaTeX

$$$\text{HasCommShift}(\mathrm{DerivedCategory}(\mathcal{C}), \mathbb{Z})$$$

Lean4

noncomputable instance : (Q (C := C)).CommShift ℤ :=
  Functor.CommShift.ofIso (quotientCompQhIso C) ℤ

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