Documentation

Mathlib.CategoryTheory.Limits.HasLimits

Existence of limits and colimits #

In CategoryTheory.Limits.IsLimit we defined IsLimit c, the data showing that a cone c is a limit cone.

The two main structures defined in this file are:

HasLimit is a propositional typeclass (it's important that it is a proposition merely asserting the existence of a limit, as otherwise we would have non-defeq problems from incompatible instances).

While HasLimit only asserts the existence of a limit cone, we happily use the axiom of choice in mathlib, so there are convenience functions all depending on HasLimit F:

Key to using the HasLimit interface is that there is an @[ext] lemma stating that to check f = g, for f g : Z ⟶ limit F, it suffices to check f ≫ limit.π F j = g ≫ limit.π F j for every j. This, combined with @[simp] lemmas, makes it possible to prove many easy facts about limits using automation (e.g. tidy).

There are abbreviations HasLimitsOfShape J C and HasLimits C asserting the existence of classes of limits. Later more are introduced, for finite limits, special shapes of limits, etc.

Ideally, many results about limits should be stated first in terms of IsLimit, and then a result in terms of HasLimit derived from this. At this point, however, this is far from uniformly achieved in mathlib --- often statements are only written in terms of HasLimit.

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 #

LimitCone F contains a cone over F together with the information that it is a limit.

Instances For

    HasLimit F represents the mere existence of a limit for F.

    Instances

      C has limits of shape J if there exists a limit for every functor F : J ⥤ C.

      Instances

        C has all limits of size v₁ u₁ (HasLimitsOfSize.{v₁ u₁} C) if it has limits of every shape J : Type u₁ with [Category.{v₁} J].

        Instances
          @[inline, reducible]

          C has all (small) limits if it has limits of every shape that is as big as its hom-sets.

          Equations
          Instances For

            The projection from the limit object to a value of the functor.

            Equations
            Instances For

              Functoriality of limits.

              Usually this morphism should be accessed through lim.map, but may be needed separately when you have specified limits for the source and target functors, but not necessarily for all functors of shape J.

              Equations
              Instances For

                The isomorphism (in Type) between morphisms from a specified object W to the limit object, and cones with cone point W.

                Equations
                Instances For

                  The isomorphism (in Type) between morphisms from a specified object W to the limit object, and an explicit componentwise description of cones with cone point W.

                  Equations
                  Instances For

                    If a functor F has a limit, so does any naturally isomorphic functor.

                    The limits of F : J ⥤ C and G : K ⥤ C are isomorphic, if there is an equivalence e : J ≌ K making the triangle commute up to natural isomorphism.

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

                      limit F is functorial in F, when C has all limits of shape J.

                      Equations
                      Instances For

                        The isomorphism between morphisms from W to the cone point of the limit cone for F and cones over F with cone point W is natural in F.

                        Equations
                        Instances For

                          The constant functor and limit functor are adjoint to each other

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • CategoryTheory.Limits.instIsRightAdjointFunctorCategoryLim = { left := CategoryTheory.Functor.const J, adj := CategoryTheory.Limits.constLimAdj }

                            ColimitCocone F contains a cocone over F together with the information that it is a colimit.

                            Instances For

                              HasColimit F represents the mere existence of a colimit for F.

                              Instances

                                C has colimits of shape J if there exists a colimit for every functor F : J ⥤ C.

                                Instances

                                  C has all colimits of size v₁ u₁ (HasColimitsOfSize.{v₁ u₁} C) if it has colimits of every shape J : Type u₁ with [Category.{v₁} J].

                                  Instances
                                    @[inline, reducible]

                                    C has all (small) colimits if it has colimits of every shape that is as big as its hom-sets.

                                    Equations
                                    Instances For

                                      The coprojection from a value of the functor to the colimit object.

                                      Equations
                                      Instances For
                                        @[simp]

                                        We have lots of lemmas describing how to simplify colimit.ι F j ≫ _, and combined with colimit.ext we rely on these lemmas for many calculations.

                                        However, since Category.assoc is a @[simp] lemma, often expressions are right associated, and it's hard to apply these lemmas about colimit.ι.

                                        We thus use reassoc to define additional @[simp] lemmas, with an arbitrary extra morphism. (see Tactic/reassoc_axiom.lean)

                                        Functoriality of colimits.

                                        Usually this morphism should be accessed through colim.map, but may be needed separately when you have specified colimits for the source and target functors, but not necessarily for all functors of shape J.

                                        Equations
                                        Instances For

                                          The isomorphism (in Type) between morphisms from the colimit object to a specified object W, and cocones with cone point W.

                                          Equations
                                          Instances For

                                            The isomorphism (in Type) between morphisms from the colimit object to a specified object W, and an explicit componentwise description of cocones with cone point W.

                                            Equations
                                            Instances For

                                              The colimits of F : J ⥤ C and G : J ⥤ C are isomorphic, if the functors are naturally isomorphic.

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

                                                The colimits of F : J ⥤ C and G : K ⥤ C are isomorphic, if there is an equivalence e : J ≌ K making the triangle commute up to natural isomorphism.

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

                                                  colimit F is functorial in F, when C has all colimits of shape J.

                                                  Equations
                                                  Instances For

                                                    The isomorphism between morphisms from the cone point of the colimit cocone for F to W and cocones over F with cone point W is natural in F.

                                                    Equations
                                                    Instances For

                                                      The colimit functor and constant functor are adjoint to each other

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        Equations
                                                        • CategoryTheory.Limits.instIsLeftAdjointFunctorCategoryColim = { right := CategoryTheory.Functor.const J, adj := CategoryTheory.Limits.colimConstAdj }

                                                        t : Cone F is a limit cone if and only if t.op : Cocone F.op is a colimit cocone.

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

                                                          t : Cocone F is a colimit cocone if and only if t.op : Cone F.op is a limit cone.

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