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 right adjoint of Cocones.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F).

Auxiliary definition for functorialityIsLeftAdjoint.

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

    The unit for the adjunction for Cocones.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F).

    Auxiliary definition for functorialityIsLeftAdjoint.

    Equations
    Instances For
      @[simp]
      theorem CategoryTheory.Adjunction.functorialityCounit_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cocone (K.comp F)) :
      ((adj.functorialityCounit K).app c).hom = adj.counit.app c.pt

      The counit for the adjunction for Cocones.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F).

      Auxiliary definition for functorialityIsLeftAdjoint.

      Equations
      • adj.functorialityCounit K = { app := fun (c : CategoryTheory.Limits.Cocone (K.comp F)) => { hom := adj.counit.app c.pt, w := }, naturality := }
      Instances For

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

        Equations
        • adj.functorialityAdjunction K = { unit := adj.functorialityUnit K, counit := adj.functorialityCounit K, left_triangle_components := , right_triangle_components := }
        Instances For
          Equations
          • CategoryTheory.Adjunction.colimPreservesColimits = CategoryTheory.Limits.colimConstAdj.leftAdjointPreservesColimits
          @[instance 100]
          Equations
          • One or more equations did not get rendered due to their size.
          @[instance 100]
          Equations
          • One or more equations did not get rendered due to their size.

          The left adjoint of Cones.functoriality K G : Cone K ⥤ Cone (K ⋙ G).

          Auxiliary definition for functorialityIsRightAdjoint.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem CategoryTheory.Adjunction.functorialityUnit'_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F G) {J : Type u} [CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J D) (c : CategoryTheory.Limits.Cone (K.comp G)) :
            ((adj.functorialityUnit' K).app c).hom = adj.unit.app c.pt

            The unit for the adjunction for Cones.functoriality K G : Cone K ⥤ Cone (K ⋙ G).

            Auxiliary definition for functorialityIsRightAdjoint.

            Equations
            • adj.functorialityUnit' K = { app := fun (c : CategoryTheory.Limits.Cone (K.comp G)) => { hom := adj.unit.app c.pt, w := }, naturality := }
            Instances For
              @[simp]

              The counit for the adjunction for Cones.functoriality K G : Cone K ⥤ Cone (K ⋙ G).

              Auxiliary definition for functorialityIsRightAdjoint.

              Equations
              • adj.functorialityCounit' K = { app := fun (c : CategoryTheory.Limits.Cone K) => { hom := adj.counit.app c.pt, w := }, naturality := }
              Instances For

                The functor Cones.functoriality K G : Cone K ⥤ Cone (K ⋙ G) is a right adjoint.

                Equations
                • adj.functorialityAdjunction' K = { unit := adj.functorialityUnit' K, counit := adj.functorialityCounit' K, left_triangle_components := , right_triangle_components := }
                Instances For
                  Equations
                  • CategoryTheory.Adjunction.limPreservesLimits = CategoryTheory.Limits.constLimAdj.rightAdjointPreservesLimits
                  @[instance 100]
                  Equations
                  • One or more equations did not get rendered due to their size.
                  @[instance 100]
                  Equations
                  • One or more equations did not get rendered due to their size.

                  auxiliary construction for coconesIso

                  Equations
                  • adj.coconesIsoComponentHom Y t = { app := fun (j : J) => (adj.homEquiv (K.obj j) Y) (t.app j), naturality := }
                  Instances For

                    auxiliary construction for coconesIso

                    Equations
                    • adj.coconesIsoComponentInv Y t = { app := fun (j : J) => (adj.homEquiv (K.obj j) Y).symm (t.app j), naturality := }
                    Instances For

                      auxiliary construction for conesIso

                      Equations
                      • adj.conesIsoComponentHom X t = { app := fun (j : J) => (adj.homEquiv (Opposite.unop X) (K.obj j)) (t.app j), naturality := }
                      Instances For

                        auxiliary construction for conesIso

                        Equations
                        • adj.conesIsoComponentInv X t = { app := fun (j : J) => (adj.homEquiv (Opposite.unop X) (K.obj j)).symm (t.app j), naturality := }
                        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.

                          Equations
                          • adj.coconesIso = CategoryTheory.NatIso.ofComponents (fun (Y : D) => { hom := adj.coconesIsoComponentHom Y, inv := adj.coconesIsoComponentInv Y, hom_inv_id := , inv_hom_id := })
                          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.

                            Equations
                            Instances For
                              Equations
                              • F.instPreservesColimitsOfShapeOfIsLeftAdjoint = CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape
                              Equations
                              Equations
                              • F.instPreservesLimitsOfShapeOfIsRightAdjoint = CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape
                              Equations