preservesColimitsOfShape_of_isZero

English

If F preserves zero morphisms, then F preserves colimits (in particular the empty shape preserves the initial object).

Русский

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

LaTeX

$$[PreservesZeroMorphisms F] ⇒ PreservesColimitsOfSize F$$

Lean4

/-- A zero functor preserves colimits. -/
theorem preservesColimitsOfShape_of_isZero : PreservesColimitsOfShape J G where
  preservesColimit
    {K} :=
    ⟨fun _ =>
      ⟨by
        rw [Functor.isZero_iff] at hG
        exact IsColimit.ofIsZero _ ((K ⋙ G).isZero (fun X ↦ hG _)) (hG _)⟩⟩

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