instAdditiveIntUpShiftFunctor — Mathlib

English

Each shift functor by an integer is additive on the Homotopy category: for every integer n, the functor shift by n preserves addition of morphisms.

Русский

Для каждого целого n сдвиговой функтор по gомотопической категории сохраняет сложение морфизмов (является аддитивным).

LaTeX

$$$\\forall n \\in \\mathbb{Z},\\; (\\mathrm{shiftFunctor} (\\mathrm{HomotopyCategory} (C, \\mathrm{ComplexShape.up} \\mathbb{Z}))\\; n).\\mathrm{Additive}$$$

Lean4

instance (n : ℤ) : (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).Additive :=
  by
  have : ((quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor _ n)).Additive :=
    Functor.additive_of_iso ((quotient C (ComplexShape.up ℤ)).commShiftIso n)
  apply Functor.additive_of_full_essSurj_comp (quotient _ _)

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