shiftFunctor₁ — Mathlib

English

The shift by x in the first index defines a functor on bicomplexes, shifting the a-index while preserving the second index structure, giving a new bicomplex with indices moved by x.

Русский

Сдвиг на x по первому индексу задаёт функтор на бикомплексах, смещая индекс a на x и сохраняю структуру по второму индексу.

LaTeX

$$$\\text{shiftFunctor}_1(C,x) : \\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 first indices (and changing the
sign of differentials). -/
abbrev shiftFunctor₁ (x : ℤ) : HomologicalComplex₂ C (up ℤ) (up ℤ) ⥤ HomologicalComplex₂ C (up ℤ) (up ℤ) :=
  shiftFunctor _ x

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