preservesZeroMorphisms_of_preserves_initial_object

English

If F preserves the initial object (i.e., preserves the colimit of the empty diagram), then F preserves zero morphisms.

Русский

Если F сохраняет начальный объект (то есть сохраняет предел пустой диаграммы), тогда F сохраняет нулевые морфизмы.

LaTeX

$$[PreservesColimit (Functor.empty C) F] ⇒ PreservesZeroMorphisms F$$

Lean4

instance (priority := 100) preservesZeroMorphisms_of_preserves_initial_object
    [PreservesColimit (Functor.empty.{0} C) F] : PreservesZeroMorphisms F :=
  preservesZeroMorphisms_of_map_zero_object <|
    F.mapIso HasZeroObject.zeroIsoInitial ≪≫ PreservesInitial.iso F ≪≫ HasZeroObject.zeroIsoInitial.symm

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