Documentation

Mathlib.CategoryTheory.Limits.Preserves.Limits

Isomorphisms about functors which preserve (co)limits #

If G preserves limits, and C and D have limits, then for any diagram F : J ⥤ C we have a canonical isomorphism preservesLimitsIso : G.obj (Limit F) ≅ Limit (F ⋙ G). We also show that we can commute IsLimit.lift of a preserved limit with Functor.mapCone: (PreservesLimit.preserves t).lift (G.mapCone c₂) = G.map (t.lift c₂).

The duals of these are also given. For functors which preserve (co)limits of specific shapes, see preserves/shapes.lean.

If C, D has all limits of shape J, and G preserves them, then preservesLimitsIso is functorial wrt F.

Instances For