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
            @[reducible, inline]
            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.

            Equations
            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
                @[reducible, inline]
                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.

                Equations
                Instances For

                  If F preserves one limit cone for the diagram K, then it preserves any limit cone for K.

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

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

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

                      Transfer preservation of a limit along a natural isomorphism in the functor.

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

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

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

                          Transfer preservation of limits along an equivalence in the shape.

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

                            If F preserves one colimit cocone for the diagram K, then it preserves any colimit cocone for K.

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

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

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

                                Transfer preservation of a colimit along a natural isomorphism in the functor.

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

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

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

                                    Transfer preservation of colimits along an equivalence in the shape.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    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
                                                @[reducible, inline]
                                                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.

                                                Equations
                                                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
                                                    @[reducible, inline]
                                                    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.

                                                    Equations
                                                    Instances For

                                                      If F ⋙ G preserves limits for K, and G reflects limits for K ⋙ F, then F preserves limits for K.

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

                                                        If F ⋙ G preserves limits of shape J and G reflects limits of shape J, then F preserves limits of shape J.

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

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

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

                                                            Transfer reflection of a limit along a natural isomorphism in the functor.

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

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

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

                                                                Transfer reflection of limits along an equivalence in the shape.

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

                                                                  If the limit of F exists and G preserves it, then if G reflects isomorphisms then it reflects the limit of F.

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

                                                                    If C has limits of shape J and G preserves them, then if G reflects isomorphisms then it reflects limits of shape J.

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

                                                                      If C has limits and G preserves limits, then if G reflects isomorphisms then it reflects limits.

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

                                                                        If F ⋙ G preserves colimits for K, and G reflects colimits for K ⋙ F, then F preserves colimits for K.

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

                                                                          If F ⋙ G preserves colimits of shape J and G reflects colimits of shape J, then F preserves colimits of shape J.

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

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

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

                                                                              Transfer reflection of a colimit along a natural isomorphism in the functor.

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

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

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

                                                                                  Transfer reflection of colimits along an equivalence in the shape.

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

                                                                                    If the colimit of F exists and G preserves it, then if G reflects isomorphisms then it reflects the colimit of F.

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

                                                                                      If C has colimits of shape J and G preserves them, then if G reflects isomorphisms then it reflects colimits of shape J.

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

                                                                                        If C has colimits and G preserves colimits, then if G reflects isomorphisms then it reflects colimits.

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

                                                                                          A fully faithful functor reflects limits.

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

                                                                                          A fully faithful functor reflects colimits.

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