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

def CategoryTheory.Limits.Types.coneOfSection {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {s : (j : J) → F.obj j} (hs : s F.sections) :

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

      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
        @[simp]
        theorem CategoryTheory.Limits.Types.isLimitEquivSections_apply {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {c : Cone F} (t : IsLimit c) (j : J) (x : c.pt) :
        ((isLimitEquivSections t) x) j = c.π.app j x
        @[simp]
        theorem CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {c : Cone F} (t : IsLimit c) (x : F.sections) (j : J) :
        c.π.app j ((isLimitEquivSections t).symm x) = x j

        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
            @[simp]
            theorem CategoryTheory.Limits.Types.Small.limitConeIsLimit_lift {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} F.sections] (s : Cone F) (v : s.pt) :
            (limitConeIsLimit F).lift s v = (equivShrink F.sections) fun (j : J) => s.π.app j v,

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

            Equations
            Instances For
              @[simp]
              theorem CategoryTheory.Limits.Types.limitCone_π_app {J : Type v} [Category.{w, v} J] (F : Functor J TypeMax) (j : J) (u : ((Functor.const J).obj F.sections).obj j) :
              (limitCone F).π.app j u = u j

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

              Equations
              Instances For
                @[simp]
                theorem CategoryTheory.Limits.Types.limitConeIsLimit_lift_coe {J : Type v} [Category.{w, v} J] (F : Functor J TypeMax) (s : Cone F) (v : s.pt) (j : J) :
                ((limitConeIsLimit F).lift s v) j = s.π.app j v

                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.

                Stacks Tag 002U

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

                Equations
                Instances For
                  @[simp]
                  noncomputable def CategoryTheory.Limits.Types.Limit.mk {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [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} [Category.{w, v} J] (F : Functor J (Type u)) [HasLimit F] (x : (j : J) → F.obj j) (h : ∀ (j j' : J) (f : j j'), F.map f (x j) = x j') (j : J) :
                    limit.π F j (mk F x h) = x j
                    theorem CategoryTheory.Limits.Types.limit_ext {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasLimit F] (x y : limit F) (w : ∀ (j : J), limit.π F j x = limit.π F j y) :
                    x = y
                    theorem CategoryTheory.Limits.Types.limit_ext' {J : Type v} [Category.{w, v} J] (F : Functor J (Type v)) (x y : limit F) (w : ∀ (j : J), limit.π F j x = limit.π F j y) :
                    x = y
                    theorem CategoryTheory.Limits.Types.limit_ext_iff' {J : Type v} [Category.{w, v} J] (F : Functor J (Type v)) (x y : limit F) :
                    x = y ∀ (j : J), limit.π F j x = limit.π F j y
                    theorem CategoryTheory.Limits.Types.Limit.w_apply {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasLimit F] {j j' : J} {x : limit F} (f : j j') :
                    F.map f (limit.π F j x) = limit.π F j' x
                    theorem CategoryTheory.Limits.Types.Limit.lift_π_apply {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasLimit F] (s : Cone F) (j : J) (x : s.pt) :
                    limit.π F j (limit.lift F s x) = s.π.app j x
                    theorem CategoryTheory.Limits.Types.Limit.map_π_apply {J : Type v} [Category.{w, v} J] {F G : Functor J (Type u)} [HasLimit F] [HasLimit G] (α : F G) (j : J) (x : limit F) :
                    limit.π G j (limMap α x) = α.app j (limit.π F j x)
                    @[simp]
                    theorem CategoryTheory.Limits.Types.Limit.w_apply' {J : Type v} [Category.{w, v} J] {F : Functor J (Type v)} {j j' : J} {x : limit F} (f : j j') :
                    F.map f (limit.π F j x) = limit.π F j' x
                    @[simp]
                    theorem CategoryTheory.Limits.Types.Limit.lift_π_apply' {J : Type v} [Category.{w, v} J] (F : Functor J (Type v)) (s : Cone F) (j : J) (x : s.pt) :
                    limit.π F j (limit.lift F s x) = s.π.app j x
                    @[simp]
                    theorem CategoryTheory.Limits.Types.Limit.map_π_apply' {J : Type v} [Category.{w, v} J] {F G : Functor J (Type v)} (α : F G) (j : J) (x : limit F) :
                    limit.π G j (limMap α x) = α.app j (limit.π F j x)

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

                    def CategoryTheory.Limits.Types.Quot.Rel {J : Type v} [Category.{w, v} J] (F : 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
                        def CategoryTheory.Limits.Types.Quot.ι {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) (j : J) :
                        F.obj jQuot F

                        Inclusion into the quotient type implementing the colimit.

                        Equations
                        Instances For
                          theorem CategoryTheory.Limits.Types.Quot.jointly_surjective {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} (x : Quot F) :
                          ∃ (j : J) (y : F.obj j), x = ι F j y

                          (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
                            @[simp]
                            theorem CategoryTheory.Limits.Types.Quot.ι_desc {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} (c : Cocone F) (j : J) (x : F.obj j) :
                            desc c (ι F j x) = c.ι.app j x
                            @[simp]
                            theorem CategoryTheory.Limits.Types.Quot.map_ι {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {j j' : J} {f : j j'} (x : F.obj j) :
                            ι F j' (F.map f x) = ι F j x

                            The obvious map from Quot F to Quot (F ⋙ uliftFunctor.{u'}).

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[simp]
                              theorem CategoryTheory.Limits.Types.quotToQuotUlift_ι {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) (j : J) (x : F.obj j) :

                              The obvious map from Quot (F ⋙ uliftFunctor.{u'}) to Quot F.

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

                                The equivalence between Quot F and Quot (F ⋙ uliftFunctor.{u'}).

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  def CategoryTheory.Limits.Types.toCocone {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {α : Type u} (f : Quot Fα) :

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

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem CategoryTheory.Limits.Types.toCocone_ι_app {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {α : Type u} (f : Quot Fα) (j : J) (a✝ : F.obj j) :
                                    (toCocone f).ι.app j a✝ = (f Quot.ι F j) a✝
                                    @[simp]
                                    theorem CategoryTheory.Limits.Types.toCocone_pt {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {α : Type u} (f : Quot Fα) :
                                    (toCocone f).pt = α
                                    theorem CategoryTheory.Limits.Types.Quot.desc_toCocone_desc {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} (c : Cocone F) {α : Type u} (f : Quot Fα) (hc : IsColimit c) (x : Quot F) :
                                    hc.desc (toCocone f) (desc c x) = f x

                                    (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
                                      @[simp]
                                      theorem CategoryTheory.Limits.Types.colimitCocone_ι_app {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} (Quot F)] (j : J) (x : F.obj j) :
                                      (colimitCocone F).ι.app j x = (equivShrink (Quot F)) (Quot.mk (Quot.Rel F) j, x)

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

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

                                          (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]
                                              @[simp]
                                              theorem CategoryTheory.Limits.Types.colimitEquivQuot_apply {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasColimit F] (j : J) (x : F.obj j) :
                                              (colimitEquivQuot F) (colimit.ι F j x) = Quot.mk (Quot.Rel F) j, x
                                              theorem CategoryTheory.Limits.Types.Colimit.w_apply {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasColimit F] {j j' : J} {x : F.obj j} (f : j j') :
                                              colimit.ι F j' (F.map f x) = colimit.ι F j x
                                              theorem CategoryTheory.Limits.Types.Colimit.ι_desc_apply {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasColimit F] (s : Cocone F) (j : J) (x : F.obj j) :
                                              colimit.desc F s (colimit.ι F j x) = s.ι.app j x
                                              theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply {J : Type v} [Category.{w, v} J] {F G : Functor J (Type u)} [HasColimitsOfShape J (Type u)] (α : F G) (j : J) (x : F.obj j) :
                                              colim.map α (colimit.ι F j x) = colimit.ι G j (α.app j x)
                                              @[simp]
                                              theorem CategoryTheory.Limits.Types.Colimit.w_apply' {J : Type v} [Category.{w, v} J] {F : Functor J (Type v)} {j j' : J} {x : F.obj j} (f : j j') :
                                              colimit.ι F j' (F.map f x) = colimit.ι F j x
                                              @[simp]
                                              theorem CategoryTheory.Limits.Types.Colimit.ι_desc_apply' {J : Type v} [Category.{w, v} J] (F : Functor J (Type v)) (s : Cocone F) (j : J) (x : F.obj j) :
                                              colimit.desc F s (colimit.ι F j x) = s.ι.app j x
                                              @[simp]
                                              theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply' {J : Type v} [Category.{w, v} J] {F G : Functor J (Type v)} (α : F G) (j : J) (x : F.obj j) :
                                              colim.map α (colimit.ι F j x) = colimit.ι G j (α.app j x)
                                              theorem CategoryTheory.Limits.Types.colimit_sound {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasColimit F] {j j' : J} {x : F.obj j} {x' : F.obj j'} (f : j j') (w : F.map f x = x') :
                                              colimit.ι F j x = colimit.ι F j' x'
                                              theorem CategoryTheory.Limits.Types.colimit_sound' {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasColimit F] {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') :
                                              colimit.ι F j x = colimit.ι F j' x'
                                              theorem CategoryTheory.Limits.Types.colimit_eq {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasColimit F] {j j' : J} {x : F.obj j} {x' : F.obj j'} (w : colimit.ι F j x = colimit.ι F j' x') :
                                              Relation.EqvGen (Quot.Rel F) j, x j', x'
                                              theorem CategoryTheory.Limits.Types.jointly_surjective_of_isColimit {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {t : Cocone F} (h : IsColimit t) (x : t.pt) :
                                              ∃ (j : J) (y : F.obj j), t.ι.app j y = x
                                              theorem CategoryTheory.Limits.Types.jointly_surjective {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) {t : Cocone F} (h : IsColimit t) (x : t.pt) :
                                              ∃ (j : J) (y : F.obj j), t.ι.app j y = x
                                              theorem CategoryTheory.Limits.Types.jointly_surjective' {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasColimit F] (x : colimit F) :
                                              ∃ (j : J) (y : F.obj j), colimit.ι F j y = x

                                              A variant of jointly_surjective for x : colimit F.

                                              If a colimit is nonempty, also its index category is nonempty.

                                              def CategoryTheory.Limits.Types.Image {α β : Type u} (f : α β) :

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

                                              Equations
                                              Instances For
                                                def CategoryTheory.Limits.Types.Image.ι {α β : Type u} (f : α β) :
                                                Image f β

                                                the inclusion of Image f into the target

                                                Equations
                                                Instances For
                                                  noncomputable def CategoryTheory.Limits.Types.Image.lift {α β : Type u} {f : α β} (F' : MonoFactorisation f) :
                                                  Image f F'.I

                                                  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
                                                      noncomputable def CategoryTheory.Limits.Types.isImage {α β : Type u} (f : α β) :

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

                                                      Equations
                                                      Instances For

                                                        Auxiliary lemma. Use limit_of_surjections_surjective instead.

                                                        Given surjections ⋯ ⟶ Xₙ₊₁ ⟶ Xₙ ⟶ ⋯ ⟶ X₀, the projection map lim Xₙ ⟶ X₀ is surjective.

                                                        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]
                                                          @[simp]
                                                          theorem CategoryTheory.Limits.compCoyonedaSectionsEquiv_symm_apply_coe {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] (F : Functor J C) (X : C) (τ : (Functor.const J).obj X F) (X✝ : J) :
                                                          ((compCoyonedaSectionsEquiv F X).symm τ) X✝ = τ.app 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]

                                                            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]

                                                              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.limitCompCoyonedaIsoCone_hom_app {J : Type v} [SmallCategory J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (X : C) (a✝ : limit (F.comp (coyoneda.obj (Opposite.op X)))) (j : J) :

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

                                                                    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.limitCompYonedaIsoCocone_hom_app {J : Type v} [SmallCategory J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (X : C) (a✝ : limit (F.op.comp (yoneda.obj X))) (j : J) :

                                                                      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