instLinearSingleFunctor — Mathlib

English

For each integer n, the single functor (DerivedCategory.singleFunctor C n) is R-linear.

Русский

Для каждого целого n функтор (DerivedCategory.singleFunctor C n) линейный по отношению к R.

LaTeX

$$$$ (\text{singleFunctor}(C, n)) : \mathrm{DerivedCategory}(C) \to \mathrm{DerivedCategory}(C) \quad \text{is } R\text{-linear}. $$$$

Lean4

instance (n : ℤ) : Functor.Linear R (DerivedCategory.singleFunctor C n) :=
  inferInstanceAs (Functor.Linear R (HomotopyCategory.singleFunctor C n ⋙ Qh))

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