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.

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
      theorem CategoryTheory.Limits.Types.isLimit_iff {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} (c : CategoryTheory.Limits.Cone F) :
      Nonempty (CategoryTheory.Limits.IsLimit c) sF.sections, ∃! x : c.pt, ∀ (j : J), c.app j x = s j

      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
          @[simp]

          (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
            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.

                @[instance 1300]

                The category of types has all limits.

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

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

                Equations
                • =

                The equivalence between the abstract limit of F in TypeMax.{v, u} and the "concrete" definition as the sections of F.

                Equations
                Instances For
                  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') :
                                      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

                                        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
                                                Equations
                                                • =
                                                @[simp]
                                                theorem CategoryTheory.Limits.compCoyonedaSectionsEquiv_apply_app {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (F : CategoryTheory.Functor J C) (X : C) (s : (F.comp (CategoryTheory.coyoneda.obj { unop := X })).sections) (j : J) :
                                                def CategoryTheory.Limits.compCoyonedaSectionsEquiv {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (F : CategoryTheory.Functor J C) (X : C) :
                                                (F.comp (CategoryTheory.coyoneda.obj { unop := X })).sections ((CategoryTheory.Functor.const J).obj X F)

                                                Sections of F ⋙ coyoneda.obj (op X) identify to natural transformations (const J).obj X ⟶ F.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[simp]
                                                  theorem CategoryTheory.Limits.opCompYonedaSectionsEquiv_apply_app {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (F : CategoryTheory.Functor J C) (X : C) (s : (F.op.comp (CategoryTheory.yoneda.obj X)).sections) (j : J) :
                                                  ((CategoryTheory.Limits.opCompYonedaSectionsEquiv F X) s).app j = s { unop := j }
                                                  def CategoryTheory.Limits.opCompYonedaSectionsEquiv {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (F : CategoryTheory.Functor J C) (X : C) :
                                                  (F.op.comp (CategoryTheory.yoneda.obj X)).sections (F (CategoryTheory.Functor.const J).obj X)

                                                  Sections of F.op ⋙ yoneda.obj X identify to natural transformations F ⟶ (const J).obj X.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[simp]
                                                    theorem CategoryTheory.Limits.compYonedaSectionsEquiv_apply_app {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) (s : (F.comp (CategoryTheory.yoneda.obj X)).sections) (j : J) :
                                                    def CategoryTheory.Limits.compYonedaSectionsEquiv {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) :
                                                    (F.comp (CategoryTheory.yoneda.obj X)).sections ((CategoryTheory.Functor.const J).obj { unop := X } F)

                                                    Sections of F ⋙ yoneda.obj X identify to natural transformations (const J).obj X ⟶ F.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[simp]
                                                      theorem CategoryTheory.Limits.limitCompCoyonedaIsoCone_hom_app {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) (X : C) :
                                                      ∀ (a : CategoryTheory.Limits.limit (F.comp (CategoryTheory.coyoneda.obj { unop := X }))) (j : J), ((CategoryTheory.Limits.limitCompCoyonedaIsoCone F X).hom a).app j = CategoryTheory.Limits.limit.π (F.comp (CategoryTheory.coyoneda.obj { unop := X })) j a
                                                      noncomputable def CategoryTheory.Limits.limitCompCoyonedaIsoCone {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) (X : C) :
                                                      CategoryTheory.Limits.limit (F.comp (CategoryTheory.coyoneda.obj { unop := X })) (CategoryTheory.Functor.const J).obj X F

                                                      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]
                                                        theorem CategoryTheory.Limits.coyonedaCompLimIsoCones_hom_app_app {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) :
                                                        ∀ (a : (CategoryTheory.coyoneda.comp (((CategoryTheory.whiskeringLeft J C (Type v)).obj F).comp CategoryTheory.Limits.lim)).obj X) (j : J), ((CategoryTheory.Limits.coyonedaCompLimIsoCones F).hom.app X a).app j = CategoryTheory.Limits.limit.π (F.comp (CategoryTheory.coyoneda.obj X)) j a
                                                        noncomputable def CategoryTheory.Limits.coyonedaCompLimIsoCones {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) :
                                                        CategoryTheory.coyoneda.comp (((CategoryTheory.whiskeringLeft J C (Type v)).obj F).comp CategoryTheory.Limits.lim) F.cones

                                                        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.coyoneda.comp (((CategoryTheory.whiskeringLeft J C (Type v)).obj X✝).comp CategoryTheory.Limits.lim)).obj X) (j : J), (((CategoryTheory.Limits.whiskeringLimYonedaIsoCones J C).hom.app X✝).app X a).app j = CategoryTheory.Limits.limit.π (X✝.comp (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
                                                            @[simp]
                                                            theorem CategoryTheory.Limits.limitCompYonedaIsoCocone_hom_app {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) (X : C) :
                                                            ∀ (a : CategoryTheory.Limits.limit (F.op.comp (CategoryTheory.yoneda.obj X))) (j : J), ((CategoryTheory.Limits.limitCompYonedaIsoCocone F X).hom a).app j = CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj X)) { unop := j } a

                                                            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
                                                              @[simp]
                                                              theorem CategoryTheory.Limits.yonedaCompLimIsoCocones_hom_app_app {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) (X : C) :
                                                              ∀ (a : (CategoryTheory.yoneda.comp (((CategoryTheory.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).obj F.op).comp CategoryTheory.Limits.lim)).obj X) (j : J), ((CategoryTheory.Limits.yonedaCompLimIsoCocones F).hom.app X a).app j = CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj X)) { unop := j } a
                                                              noncomputable def CategoryTheory.Limits.yonedaCompLimIsoCocones {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) :
                                                              CategoryTheory.yoneda.comp (((CategoryTheory.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).obj F.op).comp CategoryTheory.Limits.lim) F.cocones

                                                              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
                                                                @[simp]
                                                                theorem CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_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.yoneda.comp (((CategoryTheory.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).obj X✝.unop.op).comp CategoryTheory.Limits.lim)).obj X) (j : J), (((CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones J C).hom.app X✝).app X a).app j = CategoryTheory.Limits.limit.π (X✝.unop.op.comp (CategoryTheory.yoneda.obj X)) { unop := j } a

                                                                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