instHasShiftInt — Mathlib

English

There is a canonical shift structure on the triangle category by integers, i.e., HasShift (Triangle C) ℤ.

Русский

Существует каноническая структура сдвига на категорию треугольников по целым числам: HasShift (Triangle C) ℤ.

LaTeX

$$$\\text{HasShift}(\\operatorname{Triangle} C, \\mathbb{Z})$$$

Lean4

noncomputable instance : HasShift (Triangle C) ℤ :=
  hasShiftMk (Triangle C) ℤ
    { F := Triangle.shiftFunctor C
      zero := Triangle.shiftFunctorZero C
      add := fun a b => Triangle.shiftFunctorAdd' C a b _ rfl
      assoc_hom_app := fun a b c T => by
        ext
        all_goals
          dsimp
          rw [← shiftFunctorAdd'_assoc_hom_app a b c _ _ _ rfl rfl (add_assoc a b c)]
          dsimp only [CategoryTheory.shiftFunctorAdd']
          simp }

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