Morphisms between (co)filtered (co)limits #
Let D : I ⥤ C and D' : I' ⥤ C be cofiltered diagrams with limit cones c and c' and let
f : c.pt ⟶ c'.pt be an arbitrary morphism between the limits. We show that if Hom(-, D'.obj i')
preserves the colimit of D.op, then f is induced by a natural transformation of diagrams.
We also show the dual result.
theorem
CategoryTheory.Limits.exists_eq_isLimitMap_of_preservesColimit_yoneda
{C : Type u₁}
[Category.{v₁, u₁} C]
{I : Type u₂}
[Category.{v₂, u₂} I]
{I' : Type u₃}
[Category.{v₃, u₃} I']
{D : Functor I C}
{D' : Functor I' C}
{c : Cone D}
{c' : Cone D'}
(hc : IsLimit c)
(hc' : IsLimit c')
(f : c.pt ⟶ c'.pt)
[IsCofiltered I]
[IsCofiltered I']
[∀ (i : I'), PreservesColimit D.op (yoneda.obj (D'.obj i))]
:
∃ (J : Type (max u₂ u₃ v₁)) (x : Category.{max v₂ v₃, max (max u₂ u₃) v₁} J) (_ : IsCofiltered J) (G : Functor J I) (G'
: Functor J I') (_ : G.Initial) (x_3 : G'.Initial) (g : G.comp D ⟶ G'.comp D'),
f = IsLimit.map (Cone.whisker G c) ((Functor.Initial.isLimitWhiskerEquiv G' c').symm hc') g
A morphism f between cofiltered limits, where every object of the target diagram is
presentable relative to the source diagram, is initially induced by a natural transformation of
diagrams.
theorem
CategoryTheory.Limits.exists_eq_isColimitMap_of_preservesColimit_coyoneda
{C : Type u₁}
[Category.{v₁, u₁} C]
{I : Type u₂}
[Category.{v₂, u₂} I]
{I' : Type u₃}
[Category.{v₃, u₃} I']
{D : Functor I C}
{D' : Functor I' C}
{c : Cocone D}
{c' : Cocone D'}
(hc : IsColimit c)
(hc' : IsColimit c')
(f : c.pt ⟶ c'.pt)
[IsFiltered I]
[IsFiltered I']
[∀ (i : I), PreservesColimit D' (coyoneda.obj (Opposite.op (D.obj i)))]
:
∃ (J : Type (max u₂ u₃ v₁)) (x : Category.{max v₂ v₃, max (max u₂ u₃) v₁} J) (_ : IsFiltered J) (G : Functor J I) (G' :
Functor J I') (x_2 : G.Final) (_ : G'.Final) (g : G.comp D ⟶ G'.comp D'),
f = ((Functor.Final.isColimitWhiskerEquiv G c).symm hc).map (Cocone.whisker G' c') g
A morphism f between filtered colimits, where every object of the source diagram is
presentable relative to the target diagram, is finally induced by a natural transformation of
diagrams.is induced by a natural transformation of diagrams.