Documentation

Mathlib.CategoryTheory.Limits.IsLimit

Limits and colimits #

We set up the general theory of limits and colimits in a category. In this introduction we only describe the setup for limits; it is repeated, with slightly different names, for colimits.

The main structures defined in this file is

See also CategoryTheory.Limits.HasLimits which further builds:

Implementation #

At present we simply say everything twice, in order to handle both limits and colimits. It would be highly desirable to have some automation support, e.g. a @[dualize] attribute that behaves similarly to @[to_additive].

References #

A cone t on F is a limit cone if each cone on F admits a unique cone morphism to t.

See https://stacks.math.columbia.edu/tag/002E.

Instances For
    @[simp]

    The map makes the triangle with the two natural transformations commute

    It is the unique such map to do this

    Given a natural transformation α : F ⟶ G, we give a morphism from the cone point of any cone over F to the cone point of a limit cone over G.

    Equations
    Instances For

      The universal morphism from any other cone to a limit cone.

      Equations
      • h.liftConeMorphism s = { hom := h.lift s, w := }
      Instances For

        Restating the definition of a limit cone in terms of the ∃! operator.

        Noncomputably make a limit cone from the existence of unique factorizations.

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

          Alternative constructor for isLimit, providing a morphism of cones rather than a morphism between the cone points and separately the factorisation condition.

          Equations
          Instances For

            Limit cones on F are unique up to isomorphism.

            Equations
            • P.uniqueUpToIso Q = { hom := Q.liftConeMorphism s, inv := P.liftConeMorphism t, hom_inv_id := , inv_hom_id := }
            Instances For

              Limits of F are unique up to isomorphism.

              Equations
              Instances For

                Transport evidence that a cone is a limit cone across an isomorphism of cones.

                Equations
                Instances For

                  Isomorphism of cones preserves whether or not they are limiting cones.

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

                    If the canonical morphism from a cone point to a limiting cone point is an iso, then the first cone was limiting also.

                    Equations
                    Instances For
                      theorem CategoryTheory.Limits.IsLimit.hom_lift {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit t) {W : C} (m : W t.pt) :
                      m = h.lift { pt := W, π := { app := fun (b : J) => CategoryTheory.CategoryStruct.comp m (t.app b), naturality := } }

                      Two morphisms into a limit are equal if their compositions with each cone morphism are equal.

                      Given a right adjoint functor between categories of cones, the image of a limit cone is a limit cone.

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

                        Given two functors which have equivalent categories of cones, we can transport a limiting cone across the equivalence.

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

                          Constructing an equivalence IsLimit c ≃ IsLimit d from a natural isomorphism between the underlying functors, and then an isomorphism between c transported along this and d.

                          Equations
                          Instances For

                            The cone points of two limit cones for naturally isomorphic functors are themselves isomorphic.

                            Equations
                            Instances For

                              If s : Cone F whiskered by an equivalence e is a limit cone, so is s.

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

                                Given an equivalence of diagrams e, s is a limit cone iff s.whisker e.functor is.

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

                                  We can prove two cone points (s : Cone F).pt and (t : Cone G).pt are isomorphic if

                                  • both cones are limit cones
                                  • their indexing categories are equivalent via some e : J ≌ K,
                                  • the triangle of functors commutes up to a natural isomorphism: e.functor ⋙ G ≅ F.

                                  This is the most general form of uniqueness of cone points, allowing relabelling of both the indexing category (up to equivalence) and the functor (up to natural isomorphism).

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

                                    The universal property of a limit cone: a map W ⟶ X is the same as a cone on F with cone point W.

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

                                      The limit of F represents the functor taking W to the set of cones on F with cone point W.

                                      Equations
                                      Instances For
                                        def CategoryTheory.Limits.IsLimit.homIso' {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit t) (W : C) :
                                        ULift.{u₁, v₃} (W t.pt) { p : (j : J) → W F.obj j // ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp (p j) (F.map f) = p j' }

                                        Another, more explicit, formulation of the universal property of a limit cone. See also homIso.

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

                                          If G : C → D is a faithful functor which sends t to a limit cone, then it suffices to check that the induced maps for the image of t can be lifted to maps of C.

                                          Equations
                                          Instances For

                                            If F and G are naturally isomorphic, then F.mapCone c being a limit implies G.mapCone c is also a limit.

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

                                              A cone is a limit cone exactly if there is a unique cone morphism from any other cone.

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

                                                If F.cones is represented by X, each morphism f : Y ⟶ X gives a cone with cone point Y.

                                                Equations
                                                Instances For

                                                  If F.cones is represented by X, each cone s gives a morphism s.pt ⟶ X.

                                                  Equations
                                                  Instances For

                                                    If F.cones is represented by X, the cone corresponding to the identity morphism on X will be a limit cone.

                                                    Equations
                                                    Instances For

                                                      If F.cones is represented by X, the cone corresponding to a morphism f : Y ⟶ X is the limit cone extended by f.

                                                      If F.cones is represented by X, any cone is the extension of the limit cone by the corresponding morphism.

                                                      If F.cones is representable, then the cone corresponding to the identity morphism on the representing object is a limit cone.

                                                      Equations
                                                      Instances For

                                                        A cocone t on F is a colimit cocone if each cocone on F admits a unique cocone morphism from t.

                                                        See https://stacks.math.columbia.edu/tag/002F.

                                                        Instances For
                                                          @[simp]

                                                          The map desc makes the diagram with the natural transformations commute

                                                          desc is the unique such map

                                                          Given a natural transformation α : F ⟶ G, we give a morphism from the cocone point of a colimit cocone over F to the cocone point of any cocone over G.

                                                          Equations
                                                          Instances For

                                                            The universal morphism from a colimit cocone to any other cocone.

                                                            Equations
                                                            • h.descCoconeMorphism s = { hom := h.desc s, w := }
                                                            Instances For

                                                              Restating the definition of a colimit cocone in terms of the ∃! operator.

                                                              Noncomputably make a colimit cocone from the existence of unique factorizations.

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

                                                                Alternative constructor for IsColimit, providing a morphism of cocones rather than a morphism between the cocone points and separately the factorisation condition.

                                                                Equations
                                                                Instances For

                                                                  Colimit cocones on F are unique up to isomorphism.

                                                                  Equations
                                                                  • P.uniqueUpToIso Q = { hom := P.descCoconeMorphism t, inv := Q.descCoconeMorphism s, hom_inv_id := , inv_hom_id := }
                                                                  Instances For

                                                                    Colimits of F are unique up to isomorphism.

                                                                    Equations
                                                                    Instances For

                                                                      Transport evidence that a cocone is a colimit cocone across an isomorphism of cocones.

                                                                      Equations
                                                                      Instances For

                                                                        Isomorphism of cocones preserves whether or not they are colimiting cocones.

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

                                                                          If the canonical morphism to a cocone point from a colimiting cocone point is an iso, then the first cocone was colimiting also.

                                                                          Equations
                                                                          Instances For
                                                                            theorem CategoryTheory.Limits.IsColimit.hom_desc {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) {W : C} (m : t.pt W) :
                                                                            m = h.desc { pt := W, ι := { app := fun (b : J) => CategoryTheory.CategoryStruct.comp (t.app b) m, naturality := } }

                                                                            Two morphisms out of a colimit are equal if their compositions with each cocone morphism are equal.

                                                                            Given a left adjoint functor between categories of cocones, the image of a colimit cocone is a colimit cocone.

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

                                                                              Given two functors which have equivalent categories of cocones, we can transport a colimiting cocone across the equivalence.

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

                                                                                Constructing an equivalence is_colimit c ≃ is_colimit d from a natural isomorphism between the underlying functors, and then an isomorphism between c transported along this and d.

                                                                                Equations
                                                                                Instances For

                                                                                  The cocone points of two colimit cocones for naturally isomorphic functors are themselves isomorphic.

                                                                                  Equations
                                                                                  • P.coconePointsIsoOfNatIso Q w = { hom := P.map t w.hom, inv := Q.map s w.inv, hom_inv_id := , inv_hom_id := }
                                                                                  Instances For

                                                                                    If s : Cocone F whiskered by an equivalence e is a colimit cocone, so is s.

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

                                                                                      Given an equivalence of diagrams e, s is a colimit cocone iff s.whisker e.functor is.

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

                                                                                        We can prove two cocone points (s : Cocone F).pt and (t : Cocone G).pt are isomorphic if

                                                                                        • both cocones are colimit cocones
                                                                                        • their indexing categories are equivalent via some e : J ≌ K,
                                                                                        • the triangle of functors commutes up to a natural isomorphism: e.functor ⋙ G ≅ F.

                                                                                        This is the most general form of uniqueness of cocone points, allowing relabelling of both the indexing category (up to equivalence) and the functor (up to natural isomorphism).

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

                                                                                          The universal property of a colimit cocone: a map X ⟶ W is the same as a cocone on F with cone point W.

                                                                                          Equations
                                                                                          • h.homEquiv W = { toFun := fun (f : t.pt W) => (t.extend f), invFun := fun (ι : F (CategoryTheory.Functor.const J).obj W) => h.desc { pt := W, ι := ι }, left_inv := , right_inv := }
                                                                                          Instances For

                                                                                            The universal property of a colimit cocone: a map X ⟶ W is the same as a cocone on F with cone point W.

                                                                                            Equations
                                                                                            • h.homIso W = (Equiv.ulift.trans (h.homEquiv W)).toIso
                                                                                            Instances For

                                                                                              The colimit of F represents the functor taking W to the set of cocones on F with cone point W.

                                                                                              Equations
                                                                                              Instances For

                                                                                                Another, more explicit, formulation of the universal property of a colimit cocone. See also homIso.

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

                                                                                                  If G : C → D is a faithful functor which sends t to a colimit cocone, then it suffices to check that the induced maps for the image of t can be lifted to maps of C.

                                                                                                  Equations
                                                                                                  Instances For

                                                                                                    If F and G are naturally isomorphic, then F.mapCocone c being a colimit implies G.mapCocone c is also a colimit.

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

                                                                                                      A cocone is a colimit cocone exactly if there is a unique cocone morphism from any other cocone.

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

                                                                                                        If F.cocones is corepresented by X, each morphism f : X ⟶ Y gives a cocone with cone point Y.

                                                                                                        Equations
                                                                                                        Instances For

                                                                                                          If F.cocones is corepresented by X, each cocone s gives a morphism X ⟶ s.pt.

                                                                                                          Equations
                                                                                                          Instances For

                                                                                                            If F.cocones is corepresented by X, the cocone corresponding to the identity morphism on X will be a colimit cocone.

                                                                                                            Equations
                                                                                                            Instances For

                                                                                                              If F.cocones is corepresented by X, the cocone corresponding to a morphism f : Y ⟶ X is the colimit cocone extended by f.

                                                                                                              If F.cocones is corepresented by X, any cocone is the extension of the colimit cocone by the corresponding morphism.

                                                                                                              If F.cocones is corepresentable, then the cocone corresponding to the identity morphism on the representing object is a colimit cocone.

                                                                                                              Equations
                                                                                                              Instances For