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 : (fun (X : Type w) => X) ((F.obj j).obj k)), x = (ConcreteCategory.hom ((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 : (fun (X : Type w) => X) ((F.obj j).obj k)}
:
(ConcreteCategory.hom ((Limits.colimit F).map f)) ((ConcreteCategory.hom ((Limits.colimit.ι F j).app k)) x) = (ConcreteCategory.hom ((Limits.colimit.ι F j).app k')) ((ConcreteCategory.hom ((F.obj j).map f)) x)