Documentation

Mathlib.CategoryTheory.Limits.Creates

Creating (co)limits #

We say that F creates limits of K if, given any limit cone c for K ⋙ F (i.e. below) we can lift it to a cone "above", and further that F reflects limits for K.

Define the lift of a cone: For a cone c for K ⋙ F, give a cone for K which is a lift of c, i.e. the image of it under F is (iso) to c.

We will then use this as part of the definition of creation of limits: every limit cone has a lift.

Note this definition is really only useful when c is a limit already.

Instances For

    Define the lift of a cocone: For a cocone c for K ⋙ F, give a cocone for K which is a lift of c, i.e. the image of it under F is (iso) to c.

    We will then use this as part of the definition of creation of colimits: every limit cocone has a lift.

    Note this definition is really only useful when c is a colimit already.

    Instances For

      Definition 3.3.1 of [Riehl]. We say that F creates limits of K if, given any limit cone c for K ⋙ F (i.e. below) we can lift it to a cone "above", and further that F reflects limits for K.

      If F reflects isomorphisms, it suffices to show only that the lifted cone is a limit - see createsLimitOfReflectsIso.

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

        F creates limits of shape J if F creates the limit of any diagram K : J ⥤ C.

        Instances
          class CategoryTheory.CreatesLimitsOfSize {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))

          F creates limits if it creates limits of shape J for any J.

          Instances
            @[reducible, inline]
            abbrev CategoryTheory.CreatesLimits {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))

            F creates small limits if it creates limits of shape J for any small J.

            Equations
            Instances For

              Dual of definition 3.3.1 of [Riehl]. We say that F creates colimits of K if, given any limit cocone c for K ⋙ F (i.e. below) we can lift it to a cocone "above", and further that F reflects limits for K.

              If F reflects isomorphisms, it suffices to show only that the lifted cocone is a limit - see createsColimitOfReflectsIso.

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

                F creates colimits of shape J if F creates the colimit of any diagram K : J ⥤ C.

                Instances
                  class CategoryTheory.CreatesColimitsOfSize {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))

                  F creates colimits if it creates colimits of shape J for any small J.

                  Instances
                    @[reducible, inline]
                    abbrev CategoryTheory.CreatesColimits {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))

                    F creates small colimits if it creates colimits of shape J for any small J.

                    Equations
                    Instances For

                      A helper to show a functor creates limits. In particular, if we can show that for any limit cone c for K ⋙ F, there is a lift of it which is a limit and F reflects isomorphisms, then F creates limits. Usually, F creating limits says that any lift of c is a limit, but here we only need to show that our particular lift of c is a limit.

                      Instances For

                        A helper to show a functor creates colimits. In particular, if we can show that for any limit cocone c for K ⋙ F, there is a lift of it which is a limit and F reflects isomorphisms, then F creates colimits. Usually, F creating colimits says that any lift of c is a colimit, but here we only need to show that our particular lift of c is a colimit.

                        Instances For

                          If F reflects isomorphisms and we can lift any limit cone to a limit cone, then F creates limits. In particular here we don't need to assume that F reflects limits.

                          Equations
                          Instances For

                            If F reflects isomorphisms and we can lift a single limit cone to a limit cone, then F creates limits. Note that unlike createsLimitOfReflectsIso, to apply this result it is necessary to know that K ⋙ F actually has a limit.

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

                              When F is fully faithful, to show that F creates the limit for K it suffices to exhibit a lift of a limit cone for K ⋙ F.

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

                                When F is fully faithful, and HasLimit (K ⋙ F), to show that F creates the limit for K it suffices to exhibit a lift of the chosen limit cone for K ⋙ F.

                                Equations
                                Instances For

                                  When F is fully faithful, to show that F creates the limit for K it suffices to show that a limit point is in the essential image of F.

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

                                    When F is fully faithful, and HasLimit (K ⋙ F), to show that F creates the limit for K it suffices to show that the chosen limit point is in the essential image of F.

                                    Equations
                                    Instances For

                                      A fully faithful functor that preserves a limit that exists also creates the limit.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[instance 100]

                                        F preserves the limit of K if it creates the limit and K ⋙ F has the limit.

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

                                        If F reflects isomorphisms and we can lift any colimit cocone to a colimit cocone, then F creates colimits. In particular here we don't need to assume that F reflects colimits.

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

                                          If F reflects isomorphisms and we can lift a single colimit cocone to a colimit cocone, then F creates limits. Note that unlike createsColimitOfReflectsIso, to apply this result it is necessary to know that K ⋙ F actually has a colimit.

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

                                            When F is fully faithful, to show that F creates the colimit for K it suffices to exhibit a lift of a colimit cocone for K ⋙ F.

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

                                              When F is fully faithful, and HasColimit (K ⋙ F), to show that F creates the colimit for K it suffices to exhibit a lift of the chosen colimit cocone for K ⋙ F.

                                              Equations
                                              Instances For

                                                A fully faithful functor that preserves a colimit that exists also creates the colimit.

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

                                                  When F is fully faithful, to show that F creates the colimit for K it suffices to show that a colimit point is in the essential image of F.

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

                                                    When F is fully faithful, and HasColimit (K ⋙ F), to show that F creates the colimit for K it suffices to show that the chosen colimit point is in the essential image of F.

                                                    Equations
                                                    Instances For
                                                      @[instance 100]

                                                      F preserves the colimit of K if it creates the colimit and K ⋙ F has the colimit.

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

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

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

                                                        If F creates the limit of K and F ≅ G, then G creates the limit of K.

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

                                                          If F creates limits and F ≅ G, then G creates limits.

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

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

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

                                                              If F creates the colimit of K and F ≅ G, then G creates the colimit of K.

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

                                                                If F creates colimits and F ≅ G, then G creates colimits.

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

                                                                  If F creates the limit of K, any cone lifts to a limit.

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

                                                                    If F creates the colimit of K, any cocone lifts to a colimit.

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

                                                                      Any cone lifts through the identity functor.

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

                                                                        The identity functor creates all limits.

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

                                                                        Any cocone lifts through the identity functor.

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

                                                                          The identity functor creates all colimits.

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