instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂

English

The total object after applying first then second shift is total: the bicomplex remains total after the two shifts.

Русский

Полный объект после применения сначала первого, потом второго сдвига сохраняется: бикомплекс остаётся полным после двух сдвигов.

LaTeX

$$(((shiftFunctor1 C x).obj K) .: shiftFunctor2 C y).total (up ℤ)$$

Lean4

instance : ((shiftFunctor₁ C x ⋙ shiftFunctor₂ C y).obj K).HasTotal (up ℤ) :=
  by
  dsimp
  infer_instance

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