ofCoconesIso — Mathlib

English

If cocones of F and G are isomorphic and F has a colimit, then G has a colimit.

Русский

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

LaTeX

$$$\\text{HasColimit } G$ from isomorphism of cocones with F$$

Lean4

/-- If a functor `G` has the same collection of cocones as a functor `F`
which has a colimit, then `G` also has a colimit. -/
theorem ofCoconesIso {K : Type u₁} [Category.{v₂} K] (F : J ⥤ C) (G : K ⥤ C) (h : F.cocones ≅ G.cocones)
    [HasColimit F] : HasColimit G :=
  HasColimit.mk ⟨_, IsColimit.ofCorepresentableBy ((colimit.isColimit F).corepresentableBy.ofIso h)⟩

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