English
Let C be a category with shifts by the integers. There is a canonical isomorphism between the zero-shift functor on triangles and the identity functor on the triangle category, i.e. shift by 0 is naturally isomorphic to the identity.
Русский
Пусть C — категория с сдвигами по целым числам. Существует каноническое естественное изоморождение между нулевым сдвигом в треугольниках и тождественным функтором на категории треугольников.
LaTeX
$$$\\operatorname{Iso}(\\operatorname{Triangle.shiftFunctor} \\, C \\, 0, \\operatorname{Id}_{\\text{Triangle } C})$$$
Lean4
/-- The canonical isomorphism `Triangle.shiftFunctor C 0 ≅ 𝟭 (Triangle C)`. -/
@[simps!]
noncomputable def shiftFunctorZero : Triangle.shiftFunctor C 0 ≅ 𝟭 _ :=
NatIso.ofComponents
(fun T =>
Triangle.isoMk _ _ ((CategoryTheory.shiftFunctorZero C ℤ).app _) ((CategoryTheory.shiftFunctorZero C ℤ).app _)
((CategoryTheory.shiftFunctorZero C ℤ).app _) (by simp) (by simp)
(by
dsimp
simp only [one_smul, assoc, shiftFunctorComm_zero_hom_app, ← Functor.map_comp, Iso.inv_hom_id_app,
Functor.id_obj, Functor.map_id, comp_id, NatTrans.naturality, Functor.id_map]))
(by cat_disch)
