zero_hom_app_obj — Mathlib

English

Let F: C ⥤ D and i a family of isomorphisms providing HasShift.induced; then the zero morphism's app on F.obj X factors through i(0) and shift functor zero, giving the equality (zero F s i).hom.app (F.obj X) = (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X).

Русский

Пусть F: C ⥤ D и i последовательность изоморфизмов, задающая HasShift.induced; нулевой морфизм на F.obj X раскладывается через i(0) и сдвиг-функтор нуль, получаем равенство (zero F s i).hom.app (F.obj X) = (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X).

LaTeX

$$$(zero F s i).hom.app (F.obj X) = (i 0).hom.app X \\;\\circ\\; F.map ((shiftFunctorZero C A).hom.app X)$$$

Lean4

@[simp]
theorem zero_hom_app_obj (X : C) :
    (zero F s i).hom.app (F.obj X) = (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X) :=
  by
  have h : whiskerLeft F (zero F s i).hom = _ := ((whiskeringLeft C D D).obj F).map_preimage _
  exact (NatTrans.congr_app h X).trans (by simp)

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