HepLean 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 G preserves limits, we have an isomorphism from the image of the limit of a functor F to the limit of the functor F ⋙ G.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

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

    Equations
    Instances For

      If G preserves colimits, we have an isomorphism from the image of the colimit of a functor F to the colimit of the functor F ⋙ G.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For