Documentation

Mathlib.CategoryTheory.Adjunction.Limits

Adjunctions and limits #

A left adjoint preserves colimits (CategoryTheory.Adjunction.leftAdjointPreservesColimits), and a right adjoint preserves limits (CategoryTheory.Adjunction.rightAdjointPreservesLimits).

Equivalences create and reflect (co)limits. (CategoryTheory.Adjunction.isEquivalenceCreatesLimits, CategoryTheory.Adjunction.isEquivalenceCreatesColimits, CategoryTheory.Adjunction.isEquivalenceReflectsLimits, CategoryTheory.Adjunction.isEquivalenceReflectsColimits,)

In CategoryTheory.Adjunction.coconesIso we show that when F ⊣ G, the functor associating to each Y the cocones over K ⋙ F with cone point Y is naturally isomorphic to the functor associating to each Y the cocones over K with cone point G.obj Y.

The functor Cocones.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F) is a left adjoint.

Instances For

    When F ⊣ G, the functor associating to each Y the cocones over K ⋙ F with cone point Y is naturally isomorphic to the functor associating to each Y the cocones over K with cone point G.obj Y.

    Instances For

      When F ⊣ G, the functor associating to each X the cones over K with cone point F.op.obj X is naturally isomorphic to the functor associating to each X the cones over K ⋙ G with cone point X.

      Instances For