Concrete description of (co)limits in functor categories #
Some of the concrete descriptions of (co)limits in Type v
extend to (co)limits in the functor
category K ⥤ Type v
.
theorem
CategoryTheory.FunctorToTypes.jointly_surjective
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
(F : CategoryTheory.Functor J (CategoryTheory.Functor K TypeMax))
(k : K)
{t : CategoryTheory.Limits.Cocone F}
(h : CategoryTheory.Limits.IsColimit t)
(x : t.pt.obj k)
:
∃ (j : J) (y : (F.obj j).obj k), x = (t.ι.app j).app k y
theorem
CategoryTheory.FunctorToTypes.jointly_surjective'
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
(F : CategoryTheory.Functor J (CategoryTheory.Functor K TypeMax))
(k : K)
(x : (CategoryTheory.Limits.colimit F).obj k)
:
∃ (j : J) (y : (F.obj j).obj k), x = (CategoryTheory.Limits.colimit.ι F j).app k y