Documentation

Mathlib.CategoryTheory.Limits.Preserves.Basic

Preservation and reflection of (co)limits. #

There are various distinct notions of "preserving limits". The one we aim to capture here is: A functor F : C → D "preserves limits" if it sends every limit cone in C to a limit cone in D. Informally, F preserves all the limits which exist in C.

Note that:

In order to be able to express the property of preserving limits of a certain form, we say that a functor F preserves the limit of a diagram K if F sends every limit cone on K to a limit cone. This is vacuously satisfied when K does not admit a limit, which is consistent with the above definition of "preserves limits".

A functor F preserves limits of K (written as PreservesLimit K F) if F maps any limit cone over K to a limit cone.

Instances

    A functor F preserves colimits of K (written as PreservesColimit K F) if F maps any colimit cocone over K to a colimit cocone.

    Instances

      We say that F preserves limits of shape J if F preserves limits for every diagram K : J ⥤ C, i.e., F maps limit cones over K to limit cones.

      Instances

        We say that F preserves colimits of shape J if F preserves colimits for every diagram K : J ⥤ C, i.e., F maps colimit cocones over K to colimit cocones.

        Instances
          class CategoryTheory.Limits.PreservesLimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
          Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))

          PreservesLimitsOfSize.{v u} F means that F sends all limit cones over any diagram J ⥤ C to limit cones, where J : Type u with [Category.{v} J].

          Instances
            @[inline, reducible]
            abbrev CategoryTheory.Limits.PreservesLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
            Type (max (max (max (max u₁ u₂) v₁) v₂) (v₂ + 1))

            We say that F preserves (small) limits if it sends small limit cones over any diagram to limit cones.

            Instances For
              class CategoryTheory.Limits.PreservesColimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
              Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))

              PreservesColimitsOfSize.{v u} F means that F sends all colimit cocones over any diagram J ⥤ C to colimit cocones, where J : Type u with [Category.{v} J].

              Instances
                @[inline, reducible]
                abbrev CategoryTheory.Limits.PreservesColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
                Type (max (max (max (max u₁ u₂) v₁) v₂) (v₂ + 1))

                We say that F preserves (small) limits if it sends small limit cones over any diagram to limit cones.

                Instances For

                  A convenience function for PreservesLimit, which takes the functor as an explicit argument to guide typeclass resolution.

                  Instances For

                    A convenience function for PreservesColimit, which takes the functor as an explicit argument to guide typeclass resolution.

                    Instances For

                      Transfer preservation of limits along a natural isomorphism in the diagram.

                      Instances For

                        Transfer preservation of colimits along a natural isomorphism in the shape.

                        Instances For

                          A functor F : C ⥤ D reflects limits for K : J ⥤ C if whenever the image of a cone over K under F is a limit cone in D, the cone was already a limit cone in C. Note that we do not assume a priori that D actually has any limits.

                          Instances

                            A functor F : C ⥤ D reflects colimits for K : J ⥤ C if whenever the image of a cocone over K under F is a colimit cocone in D, the cocone was already a colimit cocone in C. Note that we do not assume a priori that D actually has any colimits.

                            Instances

                              A functor F : C ⥤ D reflects limits of shape J if whenever the image of a cone over some K : J ⥤ C under F is a limit cone in D, the cone was already a limit cone in C. Note that we do not assume a priori that D actually has any limits.

                              Instances

                                A functor F : C ⥤ D reflects colimits of shape J if whenever the image of a cocone over some K : J ⥤ C under F is a colimit cocone in D, the cocone was already a colimit cocone in C. Note that we do not assume a priori that D actually has any colimits.

                                Instances
                                  class CategoryTheory.Limits.ReflectsLimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
                                  Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))

                                  A functor F : C ⥤ D reflects limits if whenever the image of a cone over some K : J ⥤ C under F is a limit cone in D, the cone was already a limit cone in C. Note that we do not assume a priori that D actually has any limits.

                                  Instances
                                    @[inline, reducible]
                                    abbrev CategoryTheory.Limits.ReflectsLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
                                    Type (max (max (max (max u₁ u₂) v₁) v₂) (v₂ + 1))

                                    A functor F : C ⥤ D reflects (small) limits if whenever the image of a cone over some K : J ⥤ C under F is a limit cone in D, the cone was already a limit cone in C. Note that we do not assume a priori that D actually has any limits.

                                    Instances For
                                      class CategoryTheory.Limits.ReflectsColimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
                                      Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))

                                      A functor F : C ⥤ D reflects colimits if whenever the image of a cocone over some K : J ⥤ C under F is a colimit cocone in D, the cocone was already a colimit cocone in C. Note that we do not assume a priori that D actually has any colimits.

                                      Instances
                                        @[inline, reducible]
                                        abbrev CategoryTheory.Limits.ReflectsColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
                                        Type (max (max (max (max u₁ u₂) v₁) v₂) (v₂ + 1))

                                        A functor F : C ⥤ D reflects (small) colimits if whenever the image of a cocone over some K : J ⥤ C under F is a colimit cocone in D, the cocone was already a colimit cocone in C. Note that we do not assume a priori that D actually has any colimits.

                                        Instances For

                                          A convenience function for ReflectsLimit, which takes the functor as an explicit argument to guide typeclass resolution.

                                          Instances For

                                            A convenience function for ReflectsColimit, which takes the functor as an explicit argument to guide typeclass resolution.

                                            Instances For

                                              Transfer reflection of limits along a natural isomorphism in the diagram.

                                              Instances For

                                                Transfer reflection of colimits along a natural isomorphism in the diagram.

                                                Instances For