instLinear — Mathlib

English

For every integer n, the n-shift functor on the derived category is linear over the base ring R.

Русский

Для каждого целого n сдвиг по каталогу производной категории является линейным над основанием кольца R.

LaTeX

$$$$ \text{For all } n \in \mathbb{Z},\quad (\text{shiftFunctor}(\mathrm{DerivedCategory}(C), n)) \in \mathrm{Linear}_R. $$$$

Lean4

noncomputable instance : Linear R (DerivedCategory C) :=
  Localization.linear R (DerivedCategory.Qh : _ ⥤ DerivedCategory C) (HomotopyCategory.quasiIso C _)

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