Documentation

Mathlib.CategoryTheory.Limits.Types

Limits in the category of types. #

We show that the category of types has all (co)limits, by providing the usual concrete models.

We also give a characterisation of filtered colimits in Type, via colimit.ι F i xi = colimit.ι F j xj ↔ ∃ k (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj.

Next, we prove the category of types has categorical images, and that these agree with the range of a function.

Finally, we give the natural isomorphism between cones on F with cone point X and the type lim Hom(X, F·), and similarly the natural isomorphism between cocones on F with cocone point X and the type lim Hom(F·, X).

Given a section of a functor F into Type*, construct a cone over F with PUnit as the cone point.

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

    Given a cone over a functor F into Type* and an element in the cone point, construct a section of F.

    Equations
    Instances For

      The equivalence between a limiting cone of F in Type u and the "concrete" definition as the sections of F.

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

        We now provide two distinct implementations in the category of types.

        The first, in the CategoryTheory.Limits.Types.Small namespace, assumes Small.{u} J and constructs J-indexed limits in Type u.

        The second, in the CategoryTheory.Limits.Types.TypeMax namespace constructs limits for functors F : J ⥤ TypeMax.{v, u}, for J : Type v. This construction is slightly nicer, as the limit is definitionally just F.sections, rather than Shrink F.sections, which makes an arbitrary choice of u-small representative.

        Hopefully we might be able to entirely remove the TypeMax constructions, but for now they are useful glue for the later parts of the library.

        (internal implementation) the limit cone of a functor, implemented as flat sections of a pi type

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

          (internal implementation) the fact that the proposed limit cone is the limit

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

            (internal implementation) the limit cone of a functor, implemented as flat sections of a pi type

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

              (internal implementation) the fact that the proposed limit cone is the limit

              Equations
              Instances For

                The results in this section have a UnivLE.{v, u} hypothesis, but as they only use the constructions from the CategoryTheory.Limits.Types.UnivLE namespace in their definitions (rather than their statements), we leave them in the main CategoryTheory.Limits.Types namespace.

                The category of types has all limits.

                More specifically, when UnivLE.{v, u}, the category Type u has all v-small limits.

                See .

                Equations
                • =
                noncomputable def CategoryTheory.Limits.Types.Limit.mk {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasLimit F] (x : (j : J) → F.obj j) (h : ∀ (j j' : J) (f : j j'), F.map f (x j) = x j') :

                Construct a term of limit F : Type u from a family of terms x : Π j, F.obj j which are "coherent": ∀ (j j') (f : j ⟶ j'), F.map f (x j) = x j'.

                Equations
                Instances For
                  @[simp]
                  theorem CategoryTheory.Limits.Types.Limit.π_mk {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasLimit F] (x : (j : J) → F.obj j) (h : ∀ (j j' : J) (f : j j'), F.map f (x j) = x j') (j : J) :

                  In this section we verify that instances are available as expected.

                  def CategoryTheory.Limits.Types.Quot.Rel {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) :
                  (j : J) × F.obj j(j : J) × F.obj jProp

                  The relation defining the quotient type which implements the colimit of a functor F : J ⥤ Type u. See CategoryTheory.Limits.Types.Quot.

                  Equations
                  Instances For

                    A quotient type implementing the colimit of a functor F : J ⥤ Type u, as pairs ⟨j, x⟩ where x : F.obj j, modulo the equivalence relation generated by ⟨j, x⟩ ~ ⟨j', x'⟩ whenever there is a morphism f : j ⟶ j' so F.map f x = x'.

                    Equations
                    Instances For

                      Inclusion into the quotient type implementing the colimit.

                      Equations
                      Instances For

                        (implementation detail) Part of the universal property of the colimit cocone, but without assuming that Quot F lives in the correct universe.

                        Equations
                        Instances For

                          (implementation detail) A function Quot F → α induces a cocone on F as long as the universes work out.

                          Equations
                          Instances For

                            (internal implementation) the colimit cocone of a functor, implemented as a quotient of a sigma type

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

                              (internal implementation) the colimit cocone of a functor, implemented as a quotient of a sigma type

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

                                (internal implementation) the fact that the proposed colimit cocone is the colimit

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

                                  The equivalence between the abstract colimit of F in Type u and the "concrete" definition as a quotient.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[simp]
                                    theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply' {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type v)} {G : CategoryTheory.Functor J (Type v)} (α : F G) (j : J) (x : F.obj j) :
                                    CategoryTheory.Limits.colim.map α (CategoryTheory.Limits.colimit.ι F j x) = CategoryTheory.Limits.colimit.ι G j (α.app j x)
                                    theorem CategoryTheory.Limits.Types.colimit_sound' {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} [CategoryTheory.Limits.HasColimit F] {j : J} {j' : J} {x : F.obj j} {x' : F.obj j'} {j'' : J} (f : j j'') (f' : j' j'') (w : F.map f x = F.map f' x') :
                                    theorem CategoryTheory.Limits.Types.colimit_eq {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} [CategoryTheory.Limits.HasColimit F] {j : J} {j' : J} {x : F.obj j} {x' : F.obj j'} (w : CategoryTheory.Limits.colimit.ι F j x = CategoryTheory.Limits.colimit.ι F j' x') :
                                    EqvGen (CategoryTheory.Limits.Types.Quot.Rel F) { fst := j, snd := x } { fst := j', snd := x' }
                                    def CategoryTheory.Limits.Types.FilteredColimit.Rel {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) (x : (j : J) × F.obj j) (y : (j : J) × F.obj j) :

                                    An alternative relation on Σ j, F.obj j, which generates the same equivalence relation as we use to define the colimit in Type above, but that is more convenient when working with filtered colimits.

                                    Elements in F.obj j and F.obj j' are equivalent if there is some k : J to the right where their images are equal.

                                    Equations
                                    Instances For
                                      noncomputable def CategoryTheory.Limits.Types.FilteredColimit.isColimitOf {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasColimit F] (t : CategoryTheory.Limits.Cocone F) (hsurj : ∀ (x : t.pt), ∃ (i : J) (xi : F.obj i), x = t.app i xi) (hinj : ∀ (i j : J) (xi : F.obj i) (xj : F.obj j), t.app i xi = t.app j xj∃ (k : J) (f : i k) (g : j k), F.map f xi = F.map g xj) :

                                      Recognizing filtered colimits of types.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        theorem CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasColimit F] [CategoryTheory.IsFilteredOrEmpty J] {t : CategoryTheory.Limits.Cocone F} (ht : CategoryTheory.Limits.IsColimit t) {i : J} {j : J} {xi : F.obj i} {xj : F.obj j} :
                                        t.app i xi = t.app j xj ∃ (k : J) (f : i k) (g : j k), F.map f xi = F.map g xj
                                        def CategoryTheory.Limits.Types.Image {α : Type u} {β : Type u} (f : α β) :

                                        the image of a morphism in Type is just Set.range f

                                        Equations
                                        Instances For
                                          Equations

                                          the inclusion of Image f into the target

                                          Equations
                                          Instances For

                                            the universal property for the image factorisation

                                            Equations
                                            Instances For

                                              the factorisation of any morphism in Type through a mono.

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

                                                the factorisation through a mono has the universal property of the image.

                                                Equations
                                                Instances For

                                                  A cone on F with cone point X is the same as an element of lim Hom(X, F·).

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

                                                    A cone on F with cone point X is the same as an element of lim Hom(X, F·), naturally in X.

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem CategoryTheory.Limits.whiskeringLimYonedaIsoCones_hom_app_app_app (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor J C) (X : Cᵒᵖ) :
                                                      ∀ (a : (CategoryTheory.Functor.comp CategoryTheory.coyoneda (CategoryTheory.Functor.comp ((CategoryTheory.whiskeringLeft J C (Type v)).obj X✝) CategoryTheory.Limits.lim)).obj X) (j : J), (((CategoryTheory.Limits.whiskeringLimYonedaIsoCones J C).hom.app X✝).app X a).app j = CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp X✝ (CategoryTheory.coyoneda.obj X)) j a

                                                      A cone on F with cone point X is the same as an element of lim Hom(X, F·), naturally in F and X.

                                                      Equations
                                                      Instances For

                                                        A cocone on F with cocone point X is the same as an element of lim Hom(F·, X).

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

                                                          A cocone on F with cocone point X is the same as an element of lim Hom(F·, X), naturally in X.

                                                          Equations
                                                          Instances For

                                                            A cocone on F with cocone point X is the same as an element of lim Hom(F·, X), naturally in F and X.

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