hasColimit_of_iso — Mathlib

English

If F is a colimit and G is isomorphic to F, then G has a colimit.

Русский

Если F имеет колимит, и G изоморфен F, то G имеет колимит.

LaTeX

$$$\\text{HasColimit } G \\;\\Leftarrow\\; \\text{HasColimit } F$ via isomorphism$$

Lean4

/-- If `F` has a colimit, so does any naturally isomorphic functor.
-/
theorem hasColimit_of_iso {F G : J ⥤ C} [HasColimit F] (α : G ≅ F) : HasColimit G :=
  HasColimit.mk
    { cocone := (Cocones.precompose α.hom).obj (colimit.cocone F)
      isColimit := (IsColimit.precomposeHomEquiv _ _).symm (colimit.isColimit F) }

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