Documentation

Mathlib.CategoryTheory.Adjunction.Limits

Adjunctions and limits #

A left adjoint preserves colimits (CategoryTheory.Adjunction.leftAdjoint_preservesColimits), and a right adjoint preserves limits (CategoryTheory.Adjunction.rightAdjoint_preservesLimits).

Equivalences create and reflect (co)limits. (CategoryTheory.Functor.createsLimitsOfIsEquivalence, CategoryTheory.Functor.createsColimitsOfIsEquivalence, CategoryTheory.Functor.reflectsLimits_of_isEquivalence, CategoryTheory.Functor.reflectsColimits_of_isEquivalence.)

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.

source
def CategoryTheory.Adjunction.functorialityRightAdjoint {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] (K : Functor J C) :
Functor (Limits.Cocone (K.comp F)) (Limits.Cocone K)

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
    source
    def CategoryTheory.Adjunction.functorialityUnit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] (K : Functor J C) :
    Functor.id (Limits.Cocone K) ⟶ (Limits.Cocones.functoriality K F).comp (adj.functorialityRightAdjoint K)

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

    Auxiliary definition for functorialityIsLeftAdjoint.

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Adjunction.functorialityUnit_app_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] (K : Functor J C) (c : Limits.Cocone K) :
      ((adj.functorialityUnit K).app c).hom = adj.unit.app c.pt
      source
      def CategoryTheory.Adjunction.functorialityCounit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] (K : Functor J C) :
      (adj.functorialityRightAdjoint K).comp (Limits.Cocones.functoriality K F) ⟶ Functor.id (Limits.Cocone (K.comp F))

      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
        source
        @[simp]
        theorem CategoryTheory.Adjunction.functorialityCounit_app_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] (K : Functor J C) (c : Limits.Cocone (K.comp F)) :
        ((adj.functorialityCounit K).app c).hom = adj.counit.app c.pt
        source
        def CategoryTheory.Adjunction.functorialityAdjunction {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] (K : Functor J C) :
        Limits.Cocones.functoriality K F ⊣ adj.functorialityRightAdjoint K

        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
          source
          theorem CategoryTheory.Adjunction.leftAdjoint_preservesColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) :
          Limits.PreservesColimitsOfSize.{v, u, v₁, v₂, u₁, u₂} F

          A left adjoint preserves colimits.

          See https://stacks.math.columbia.edu/tag/0038.

          source
          @[deprecated "No deprecation message was provided." (since := "2024-11-19")]
          theorem CategoryTheory.Adjunction.leftAdjointPreservesColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) :
          Limits.PreservesColimitsOfSize.{v, u, v₁, v₂, u₁, u₂} F
          source
          instance CategoryTheory.Adjunction.colim_preservesColimits {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] [Limits.HasColimitsOfShape J C] :
          Limits.PreservesColimits Limits.colim
          source
          @[instance 100]
          instance CategoryTheory.Adjunction.isEquivalence_preservesColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Functor C D) [E.IsEquivalence] :
          Limits.PreservesColimitsOfSize.{v, u, v₁, v₂, u₁, u₂} E
          source
          @[instance 100]
          instance CategoryTheory.Functor.reflectsColimits_of_isEquivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Functor D C) [E.IsEquivalence] :
          Limits.ReflectsColimitsOfSize.{v, u, v₂, v₁, u₂, u₁} E
          source
          @[deprecated "No deprecation message was provided." (since := "2024-11-18")]
          theorem CategoryTheory.Adjunction.isEquivalenceReflectsColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Functor D C) [E.IsEquivalence] :
          Limits.ReflectsColimitsOfSize.{v, u, v₂, v₁, u₂, u₁} E
          source
          @[instance 100]
          noncomputable instance CategoryTheory.Functor.createsColimitsOfIsEquivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (H : Functor D C) [H.IsEquivalence] :
          CreatesColimitsOfSize.{v, u, v₂, v₁, u₂, u₁} H
          Equations
          • One or more equations did not get rendered due to their size.
          source
          @[deprecated CategoryTheory.Functor.createsColimitsOfIsEquivalence (since := "2024-11-18")]
          def CategoryTheory.Adjunction.isEquivalenceCreatesColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (H : Functor D C) [H.IsEquivalence] :
          CreatesColimitsOfSize.{v, u, v₂, v₁, u₂, u₁} H

          Alias of CategoryTheory.Functor.createsColimitsOfIsEquivalence.

          Equations
          Instances For
            source
            theorem CategoryTheory.Adjunction.hasColimit_comp_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type u} [Category.{v, u} J] (K : Functor J C) (E : Functor C D) [E.IsEquivalence] [Limits.HasColimit K] :
            Limits.HasColimit (K.comp E)
            source
            theorem CategoryTheory.Adjunction.hasColimit_of_comp_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type u} [Category.{v, u} J] (K : Functor J C) (E : Functor C D) [E.IsEquivalence] [Limits.HasColimit (K.comp E)] :
            Limits.HasColimit K
            source
            theorem CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type u} [Category.{v, u} J] (E : Functor C D) [E.IsEquivalence] [Limits.HasColimitsOfShape J D] :
            Limits.HasColimitsOfShape J C

            Transport a HasColimitsOfShape instance across an equivalence.

            source
            theorem CategoryTheory.Adjunction.has_colimits_of_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Functor C D) [E.IsEquivalence] [Limits.HasColimitsOfSize.{v, u, v₂, u₂} D] :
            Limits.HasColimitsOfSize.{v, u, v₁, u₁} C

            Transport a HasColimitsOfSize instance across an equivalence.

            source
            def CategoryTheory.Adjunction.functorialityLeftAdjoint {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] (K : Functor J D) :
            Functor (Limits.Cone (K.comp G)) (Limits.Cone K)

            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
              source
              def CategoryTheory.Adjunction.functorialityUnit' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] (K : Functor J D) :
              Functor.id (Limits.Cone (K.comp G)) ⟶ (adj.functorialityLeftAdjoint K).comp (Limits.Cones.functoriality K G)

              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
                source
                @[simp]
                theorem CategoryTheory.Adjunction.functorialityUnit'_app_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] (K : Functor J D) (c : Limits.Cone (K.comp G)) :
                ((adj.functorialityUnit' K).app c).hom = adj.unit.app c.pt
                source
                def CategoryTheory.Adjunction.functorialityCounit' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] (K : Functor J D) :
                (Limits.Cones.functoriality K G).comp (adj.functorialityLeftAdjoint K) ⟶ Functor.id (Limits.Cone K)

                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
                  source
                  @[simp]
                  theorem CategoryTheory.Adjunction.functorialityCounit'_app_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] (K : Functor J D) (c : Limits.Cone K) :
                  ((adj.functorialityCounit' K).app c).hom = adj.counit.app c.pt
                  source
                  def CategoryTheory.Adjunction.functorialityAdjunction' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] (K : Functor J D) :
                  adj.functorialityLeftAdjoint K ⊣ Limits.Cones.functoriality K G

                  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
                    source
                    theorem CategoryTheory.Adjunction.rightAdjoint_preservesLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) :
                    Limits.PreservesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} G

                    A right adjoint preserves limits.

                    See https://stacks.math.columbia.edu/tag/0038.

                    source
                    @[deprecated "No deprecation message was provided." (since := "2024-11-19")]
                    theorem CategoryTheory.Adjunction.rightAdjointPreservesLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) :
                    Limits.PreservesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} G
                    source
                    instance CategoryTheory.Adjunction.lim_preservesLimits {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] [Limits.HasLimitsOfShape J C] :
                    Limits.PreservesLimits Limits.lim
                    source
                    @[instance 100]
                    instance CategoryTheory.Adjunction.isEquivalencePreservesLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Functor D C) [E.IsEquivalence] :
                    Limits.PreservesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} E
                    source
                    @[instance 100]
                    instance CategoryTheory.Functor.reflectsLimits_of_isEquivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Functor D C) [E.IsEquivalence] :
                    Limits.ReflectsLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} E
                    source
                    @[deprecated "No deprecation message was provided." (since := "2024-11-18")]
                    theorem CategoryTheory.Adjunction.isEquivalenceReflectsLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Functor D C) [E.IsEquivalence] :
                    Limits.ReflectsLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} E
                    source
                    @[instance 100]
                    noncomputable instance CategoryTheory.Functor.createsLimitsOfIsEquivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (H : Functor D C) [H.IsEquivalence] :
                    CreatesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} H
                    Equations
                    • One or more equations did not get rendered due to their size.
                    source
                    @[deprecated CategoryTheory.Functor.createsLimitsOfIsEquivalence (since := "2024-11-18")]
                    def CategoryTheory.Adjunction.isEquivalenceCreatesLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (H : Functor D C) [H.IsEquivalence] :
                    CreatesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} H

                    Alias of CategoryTheory.Functor.createsLimitsOfIsEquivalence.

                    Equations
                    Instances For
                      source
                      theorem CategoryTheory.Adjunction.hasLimit_comp_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type u} [Category.{v, u} J] (K : Functor J D) (E : Functor D C) [E.IsEquivalence] [Limits.HasLimit K] :
                      Limits.HasLimit (K.comp E)
                      source
                      theorem CategoryTheory.Adjunction.hasLimit_of_comp_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type u} [Category.{v, u} J] (K : Functor J D) (E : Functor D C) [E.IsEquivalence] [Limits.HasLimit (K.comp E)] :
                      Limits.HasLimit K
                      source
                      theorem CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type u} [Category.{v, u} J] (E : Functor D C) [E.IsEquivalence] [Limits.HasLimitsOfShape J C] :
                      Limits.HasLimitsOfShape J D

                      Transport a HasLimitsOfShape instance across an equivalence.

                      source
                      theorem CategoryTheory.Adjunction.has_limits_of_equivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Functor D C) [E.IsEquivalence] [Limits.HasLimitsOfSize.{v, u, v₁, u₁} C] :
                      Limits.HasLimitsOfSize.{v, u, v₂, u₂} D

                      Transport a HasLimitsOfSize instance across an equivalence.

                      source
                      def CategoryTheory.Adjunction.coconesIsoComponentHom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] {K : Functor J C} (Y : D) (t : ((cocones J D).obj (Opposite.op (K.comp F))).obj Y) :
                      (G.comp ((cocones J C).obj (Opposite.op K))).obj Y

                      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
                        source
                        def CategoryTheory.Adjunction.coconesIsoComponentInv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] {K : Functor J C} (Y : D) (t : (G.comp ((cocones J C).obj (Opposite.op K))).obj Y) :
                        ((cocones J D).obj (Opposite.op (K.comp F))).obj Y

                        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
                          source
                          def CategoryTheory.Adjunction.conesIsoComponentHom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] {K : Functor J D} (X : Cᵒᵖ) (t : (F.op.comp ((cones J D).obj K)).obj X) :
                          ((cones J C).obj (K.comp G)).obj X

                          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
                            source
                            def CategoryTheory.Adjunction.conesIsoComponentInv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] {K : Functor J D} (X : Cᵒᵖ) (t : ((cones J C).obj (K.comp G)).obj X) :
                            (F.op.comp ((cones J D).obj K)).obj X

                            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
                              source
                              def CategoryTheory.Adjunction.coconesIso {C : Type u₁} [Category.{v₀, u₁} C] {D : Type u₂} [Category.{v₀, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] {K : Functor J C} :
                              (cocones J D).obj (Opposite.op (K.comp F)) ≅ G.comp ((cocones J C).obj (Opposite.op K))

                              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
                                source
                                def CategoryTheory.Adjunction.conesIso {C : Type u₁} [Category.{v₀, u₁} C] {D : Type u₂} [Category.{v₀, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {J : Type u} [Category.{v, u} J] {K : Functor J D} :
                                F.op.comp ((cones J D).obj K) ≅ (cones J C).obj (K.comp G)

                                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
                                  source
                                  instance CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint {J : Type u_1} {C : Type u_2} {D : Type u_3} [Category.{u_6, u_1} J] [Category.{u_4, u_2} C] [Category.{u_5, u_3} D] (F : Functor C D) [F.IsLeftAdjoint] :
                                  Limits.PreservesColimitsOfShape J F
                                  source
                                  instance CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint {C : Type u_2} {D : Type u_3} [Category.{u_4, u_2} C] [Category.{u_5, u_3} D] (F : Functor C D) [F.IsLeftAdjoint] :
                                  Limits.PreservesColimitsOfSize.{v, u, u_4, u_5, u_2, u_3} F
                                  source
                                  instance CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint {J : Type u_1} {C : Type u_2} {D : Type u_3} [Category.{u_6, u_1} J] [Category.{u_5, u_2} C] [Category.{u_4, u_3} D] (F : Functor C D) [F.IsRightAdjoint] :
                                  Limits.PreservesLimitsOfShape J F
                                  source
                                  instance CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint {C : Type u_2} {D : Type u_3} [Category.{u_5, u_2} C] [Category.{u_4, u_3} D] (F : Functor C D) [F.IsRightAdjoint] :
                                  Limits.PreservesLimitsOfSize.{v, u, u_5, u_4, u_2, u_3} F