instAdditiveHomologicalComplexIntUpShiftFunctor

English

Each shift functor by an integer n acts additively on CochainComplexes, provided the ambient category is additive. In particular, for each n, the functor shift by n is additive.

Русский

Каждый сдвиг на целое число n действует аддитивно на CochainComplexes, если окружающая категория аддитивна. То есть сдвиг на n является аддитивным функтором.

LaTeX

$$$$\forall n\in \mathbb{Z},\ Shift_n:\mathrm{CochainComplex}(C,\mathbb{Z})\to \mathrm{CochainComplex}(C,\mathbb{Z})\ \text{является аддитивным функтором.}$$$$

Lean4

instance (n : ℤ) : (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).Additive :=
  (inferInstance : (CochainComplex.shiftFunctor C n).Additive)

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