Isomorphisms about functors which preserve (co)limits
G preserves limits, and
D have limits, then for any diagram
F : J ⥤ C we have a
preserves_limit_iso : G.obj (limit F) ≅ limit (F ⋙ G).
We also show that we can commute
is_limit.lift of a preserved limit with
(preserves_limit.preserves t).lift (G.map_cone c₂) = G.map (t.lift c₂).
The duals of these are also given. For functors which preserve (co)limits of specific shapes, see
G preserves limits, we have an isomorphism from the image of the limit of a functor
to the limit of the functor
F ⋙ G.
G preserves colimits, we have an isomorphism from the image of the colimit of a functor
to the colimit of the functor
F ⋙ G.