preservesTerminalObject_of_preservesZeroMorphisms

English

If G is zero (IsZero G), then G preserves limits of shape J for every J: PreservesLimitsOfShape J G, and hence PreservesLimitsOfSize G.

Русский

Если G является нулевым (IsZero G), тогда G сохраняет пределы формы J для любого J: PreservesLimitsOfShape J G, следовательно PreservesLimitsOfSize G.

LaTeX

$$$\IsZero(G) \Rightarrow \forall J, [Category J] \Rightarrow PreservesLimitsOfShape J G$$

Lean4

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

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