preservesInitialObject_of_preservesZeroMorphisms

English

If G is zero (IsZero G), then G preserves limits of all sizes: PreservesColimitsOfSize G.

Русский

Если G нулевой, тогда G сохраняет пределы в любых размерах: PreservesColimitsOfSize G.

LaTeX

$$$IsZero(G) \Rightarrow PreservesColimitsOfSize G$$$

Lean4

/-- Preserving zero morphisms implies preserving terminal objects. -/
theorem preservesInitialObject_of_preservesZeroMorphisms [PreservesZeroMorphisms F] :
    PreservesColimit (Functor.empty.{0} C) F :=
  preservesInitial_of_iso F <|
    HasZeroObject.zeroIsoInitial.symm ≪≫ (mapZeroObject F).symm ≪≫ (F.mapIso HasZeroObject.zeroIsoInitial.symm).symm

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