instHasShiftInt — Mathlib

English

There is a shift functor on the derived category by integers, i.e., a ℤ-indexed family of autoequivalences corresponding to shifting complexes by n ∈ ℤ.

Русский

В производной категории существует сдвиг на целые, то есть множество взаимно однозначных сопряжённых переходов, индексируемых ℤ, соответствующих сдвигу цепочек на n ∈ ℤ.

LaTeX

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

Lean4

noncomputable instance : HasShift (DerivedCategory C) ℤ :=
  HasShift.localized Qh (HomotopyCategory.subcategoryAcyclic C).trW ℤ

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