English
For any category C and additive structure, the category of CochainComplexes over C with index set ℤ supports a shift by any integer n. In particular, there is a shift functor by n for every n ∈ ℤ and this construction is compatible with addition of indices.
Русский
Для любой категории C и аддитивной структуры существует сдвиг по целочисленным индексам для категории CochainComplexes(C, ℤ); то есть для каждого n ∈ ℤ задан соответствующий сдвиг, и он совместим с суммой индексов.
LaTeX
$$$$\forall C\,[\text{Category}(C)],\forall n\in \mathbb{Z},\ \text{exists } \text{Shift}_n:\mathrm{CochainComplex}(C,\mathbb{Z})\to\mathrm{CochainComplex}(C,\mathbb{Z})\ \text{and} \ \text{Shift}_0=\mathrm{Id},\ \text{Shift}_{n+m}\cong \text{Shift}_n\circ\text{Shift}_m.$$$$
Lean4
instance : HasShift (CochainComplex C ℤ) ℤ :=
hasShiftMk _ _
{ F := shiftFunctor C
zero := shiftFunctorZero' C _ rfl
add := fun n₁ n₂ => shiftFunctorAdd' C n₁ n₂ _ rfl }
