preservesColimit_of_preserves_colimit_cocone

English

If F preserves one colimit cocone for a diagram K, then F preserves any colimit cocone for K.

Русский

Если F сохраняет один колимитный когон для диаграммы K, то она сохраняет любой колимитный когон для K.

LaTeX

$$$ IsColimit(t) \\land IsColimit( F.mapCocone(t) ) \\Rightarrow PreservesColimit(K, F). $$$

Lean4

/-- If F preserves one colimit cocone for the diagram K,
  then it preserves any colimit cocone for K. -/
theorem preservesColimit_of_preserves_colimit_cocone {F : C ⥤ D} {t : Cocone K} (h : IsColimit t)
    (hF : IsColimit (F.mapCocone t)) : PreservesColimit K F :=
  ⟨fun h' => ⟨IsColimit.ofIsoColimit hF (Functor.mapIso _ (IsColimit.uniqueUpToIso h h'))⟩⟩

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