English
The shift by y in the second index gives a functor which shifts the b-index, producing a new bicomplex with indices moved in the second direction.
Русский
Сдвиг на y по второму индексу задаёт функтор, который смещает вторую координату b и порождает новый бикомплекс с индексами, смещёнными во втором направлении.
LaTeX
$$$\\text{shiftFunctor}_2(C,y) : \\text{HomologicalComplex}_2\\; C\\; (up\\;\\mathbb{Z})\\; (up\\;\\mathbb{Z}) \\to \\text{HomologicalComplex}_2\\; C\\; (up\\;\\mathbb{Z})\\; (up\\;\\mathbb{Z}).$$$
Lean4
/-- The shift on bicomplexes obtained by shifting the second indices (and changing the
sign of differentials). -/
abbrev shiftFunctor₂ (y : ℤ) : HomologicalComplex₂ C (up ℤ) (up ℤ) ⥤ HomologicalComplex₂ C (up ℤ) (up ℤ) :=
(shiftFunctor _ y).mapHomologicalComplex _
