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₁}
[Category.{v₁, u₁} J]
{K : Type u₂}
[Category.{v₂, u₂} K]
(F : Functor J (Functor K (Type w)))
(k : K)
{t : Limits.Cocone F}
(h : Limits.IsColimit t)
(x : t.pt.obj k)
[∀ (k : K), Limits.HasColimit (F.flip.obj k)]
:
theorem
CategoryTheory.FunctorToTypes.jointly_surjective'
{J : Type u₁}
[Category.{v₁, u₁} J]
{K : Type u₂}
[Category.{v₂, u₂} K]
(F : Functor J (Functor K (Type w)))
[∀ (k : K), Limits.HasColimit (F.flip.obj k)]
(k : K)
(x : (Limits.colimit F).obj k)
:
∃ (j : J) (y : (F.obj j).obj k), x = (Limits.colimit.ι F j).app k y
theorem
CategoryTheory.FunctorToTypes.colimit.map_ι_apply
{J : Type u₁}
[Category.{v₁, u₁} J]
{K : Type u₂}
[Category.{v₂, u₂} K]
(F : Functor J (Functor K (Type w)))
[Limits.HasColimit F]
(j : J)
{k k' : K}
{f : k ⟶ k'}
{x : (F.obj j).obj k}
:
(Limits.colimit F).map f ((Limits.colimit.ι F j).app k x) = (Limits.colimit.ι F j).app k' ((F.obj j).map f x)