instLinearCochainComplexIntQ — Mathlib

English

The functor Q is linear over R, i.e., it preserves the R-module structures along the localization to the derived category.

Русский

Функтор Q линейный по отношению к R, то есть он сохраняет R-структуры модуля при локализации к производной категории.

LaTeX

$$$$ \text{Q} : \text{(appropriate source)} \to \mathrm{DerivedCategory}(C) \quad \text{is } R\text{-linear}. $$$$

Lean4

instance : Functor.Linear R (DerivedCategory.Q : _ ⥤ DerivedCategory C) :=
  Functor.linear_of_iso _ (quotientCompQhIso C)

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