CategoryTheory.Limits.Concrete.isColimit_exists_rep

theorem CategoryTheory.Limits.Concrete.isColimit_exists_rep : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ConcreteCategory C] {J : Type w} [inst_2 : CategoryTheory.Category.{r, w} J] (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)] {D : CategoryTheory.Limits.Cocone F}, CategoryTheory.Limits.IsColimit D → ∀ (x : (CategoryTheory.forget C).obj D.pt), ∃ j y, (D.ι.app j) y = x

This theorem, `CategoryTheory.Limits.Concrete.isColimit_exists_rep`, states that for any type `C` that has a category structure and is a concrete category, along with any type `J` that also has a category structure, and any functor `F` from `J` to `C`. If `F` preserves colimits under the forgetful functor (which maps `C` to the type `w`) and `D` is a cocone over `F`, then for any `IsColimit` of the cocone `D`, for any object `x` in the image under the forgetful functor of the vertex of the cocone, there exists a `j` in `J` and `y` in the domain of the morphism `D.ι.app j` such that `D.ι.app j` of `y` equals `x`. This theorem basically states the condition for an object to be a colimit in the concrete category.

More concisely: For a concrete category `C` with a forgetful functor `w` to Type, if functor `F: J → C` preserves colimits under `w` and `D: J → C` is a cocone over `F` with `IsColimit D`, then for each object `x` in the image of `w` on the vertex of `D`, there exists `j` in `J` and `y` in the domain of `D.ι.app j` such that `D.ι.app j(y) = x`.