Documentation

Mathlib.CategoryTheory.Category.Cat.Limit

The category of small categories has all small limits. #

An object in the limit consists of a family of objects, which are carried to one another by the functors in the diagram. A morphism between two such objects is a family of morphisms between the corresponding objects, which are carried to one another by the action on morphisms of the functors in the diagram.

Future work #

Can the indexing category live in a lower universe?

source
instance CategoryTheory.Cat.HasLimits.categoryObjects {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CategoryTheory.Cat} {j : J} :
CategoryTheory.SmallCategory ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).toPrefunctor.obj j)
Equations
source
@[simp]
theorem CategoryTheory.Cat.HasLimits.homDiagram_map {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CategoryTheory.Cat} (X : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) (Y : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) :
∀ {X_1 Y_1 : J} (f : X_1 ⟶ Y_1) (g : CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) X_1 X ⟶ CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) X_1 Y), (CategoryTheory.Cat.HasLimits.homDiagram X Y).toPrefunctor.map f g = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) Y_1 X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) X_1) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).toPrefunctor.map f) X)) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map f).toPrefunctor.map g) (CategoryTheory.eqToHom (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) X_1) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).toPrefunctor.map f) Y = CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) Y_1 Y)))
source
@[simp]
theorem CategoryTheory.Cat.HasLimits.homDiagram_obj {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CategoryTheory.Cat} (X : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) (Y : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) (j : J) :
(CategoryTheory.Cat.HasLimits.homDiagram X Y).toPrefunctor.obj j = (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j X ⟶ CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j Y)
source
def CategoryTheory.Cat.HasLimits.homDiagram {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CategoryTheory.Cat} (X : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) (Y : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) :
CategoryTheory.Functor J (Type v)

Auxiliary definition: the diagram whose limit gives the morphism space between two objects of the limit category.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Cat.HasLimits.instCategoryLimitTypeTypesCompCatCategoryObjectsHasLimitUnivLE_of_maxSmall_self_id {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (X : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) :
    CategoryTheory.CategoryStruct.id X = CategoryTheory.Limits.Types.Limit.mk (CategoryTheory.Cat.HasLimits.homDiagram X X) (fun (j : J) => CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j X)) (_ : ∀ (j j' : J) (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j' X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).toPrefunctor.map f) X)) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map f).toPrefunctor.map (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j X))) (CategoryTheory.eqToHom (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).toPrefunctor.map f) X = CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j' X))) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j' X))
    source
    @[simp]
    theorem CategoryTheory.Cat.HasLimits.instCategoryLimitTypeTypesCompCatCategoryObjectsHasLimitUnivLE_of_maxSmall_self_comp {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) {X : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)} {Y : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)} {Z : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)} (f : X ⟶ Y) (g : Y ⟶ Z) :
    CategoryTheory.CategoryStruct.comp f g = CategoryTheory.Limits.Types.Limit.mk (CategoryTheory.Cat.HasLimits.homDiagram X Z) (fun (j : J) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram X Y) j f) (CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram Y Z) j g)) (_ : ∀ (j j' : J) (h : j ⟶ j'), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j' X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).toPrefunctor.map h) X)) (CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map h).toPrefunctor.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram X Y) j f) (CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram Y Z) j g))) (CategoryTheory.eqToHom (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).toPrefunctor.map h) Z = CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j' Z))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram X Y) j' f) (CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram Y Z) j' g))
    source
    instance CategoryTheory.Cat.HasLimits.instCategoryLimitTypeTypesCompCatCategoryObjectsHasLimitUnivLE_of_maxSmall_self {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) :
    CategoryTheory.Category.{v, v} (CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects))
    Equations
    source
    @[simp]
    theorem CategoryTheory.Cat.HasLimits.limitConeX_α {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) :
    ↑(CategoryTheory.Cat.HasLimits.limitConeX F) = CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)
    source
    @[simp]
    theorem CategoryTheory.Cat.HasLimits.limitConeX_str {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) :
    (CategoryTheory.Cat.HasLimits.limitConeX F).str = inferInstance
    source
    def CategoryTheory.Cat.HasLimits.limitConeX {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) :
    CategoryTheory.Cat

    Auxiliary definition: the limit category.

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Cat.HasLimits.limitCone_pt {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) :
      (CategoryTheory.Cat.HasLimits.limitCone F).pt = CategoryTheory.Cat.HasLimits.limitConeX F
      source
      @[simp]
      theorem CategoryTheory.Cat.HasLimits.limitCone_π_app_obj {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (j : J) :
      ∀ (a : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)), ((CategoryTheory.Cat.HasLimits.limitCone F).π.app j).toPrefunctor.obj a = CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j a
      source
      @[simp]
      theorem CategoryTheory.Cat.HasLimits.limitCone_π_app_map {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (j : J) :
      ∀ {X Y : ↑(((CategoryTheory.Functor.const J).toPrefunctor.obj (CategoryTheory.Cat.HasLimits.limitConeX F)).toPrefunctor.obj j)} (f : X ⟶ Y), ((CategoryTheory.Cat.HasLimits.limitCone F).π.app j).toPrefunctor.map f = CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram X Y) j f
      source
      def CategoryTheory.Cat.HasLimits.limitCone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) :
      CategoryTheory.Limits.Cone F

      Auxiliary definition: the cone over the limit category.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Cat.HasLimits.limitConeLift_map {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (s : CategoryTheory.Limits.Cone F) :
        ∀ {X Y : ↑s.pt} (f : X ⟶ Y), (CategoryTheory.Cat.HasLimits.limitConeLift F s).toPrefunctor.map f = CategoryTheory.Limits.Types.Limit.mk (CategoryTheory.Cat.HasLimits.homDiagram (CategoryTheory.Limits.limit.lift (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun (j : J) => (s.π.app j).obj } X) (CategoryTheory.Limits.limit.lift (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun (j : J) => (s.π.app j).obj } Y)) (fun (j : J) => CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j (CategoryTheory.Limits.limit.lift (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun (j : J) => (s.π.app j).obj } X) = (s.π.app j).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((s.π.app j).toPrefunctor.map f) (CategoryTheory.eqToHom (_ : (s.π.app j).toPrefunctor.obj Y = CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j (CategoryTheory.Limits.limit.lift (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun (j : J) => (s.π.app j).obj } Y))))) (_ : ∀ (j j' : J) (h : j ⟶ j'), (CategoryTheory.Cat.HasLimits.homDiagram (CategoryTheory.Limits.limit.lift (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun (j : J) => (s.π.app j).obj } X) (CategoryTheory.Limits.limit.lift (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun (j : J) => (s.π.app j).obj } Y)).toPrefunctor.map h (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j (CategoryTheory.Limits.limit.lift (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun (j : J) => (s.π.app j).obj } X) = (s.π.app j).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((s.π.app j).toPrefunctor.map f) (CategoryTheory.eqToHom (_ : (s.π.app j).toPrefunctor.obj Y = CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j (CategoryTheory.Limits.limit.lift (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun (j : J) => (s.π.app j).obj } Y))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j' (CategoryTheory.Limits.limit.lift (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun (j : J) => (s.π.app j).obj } X) = (s.π.app j').toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((s.π.app j').toPrefunctor.map f) (CategoryTheory.eqToHom (_ : (s.π.app j').toPrefunctor.obj Y = CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j' (CategoryTheory.Limits.limit.lift (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun (j : J) => (s.π.app j).obj } Y)))))
        source
        @[simp]
        theorem CategoryTheory.Cat.HasLimits.limitConeLift_obj {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (s : CategoryTheory.Limits.Cone F) :
        ∀ (a : { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun (j : J) => (s.π.app j).obj }.pt), (CategoryTheory.Cat.HasLimits.limitConeLift F s).toPrefunctor.obj a = CategoryTheory.Limits.limit.lift (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun (j : J) => (s.π.app j).obj } a
        source
        def CategoryTheory.Cat.HasLimits.limitConeLift {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (s : CategoryTheory.Limits.Cone F) :
        s.pt ⟶ CategoryTheory.Cat.HasLimits.limitConeX F

        Auxiliary definition: the universal morphism to the proposed limit cone.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Cat.HasLimits.limit_π_homDiagram_eqToHom {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CategoryTheory.Cat} (X : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) (Y : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) (j : J) (h : X = Y) :
          CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram X Y) j (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j X = CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j Y)
          source
          def CategoryTheory.Cat.HasLimits.limitConeIsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) :
          CategoryTheory.Limits.IsLimit (CategoryTheory.Cat.HasLimits.limitCone F)

          Auxiliary definition: the proposed cone is a limit cone.

          Equations
          Instances For
            source
            instance CategoryTheory.Cat.instHasLimitsCatCategory :
            CategoryTheory.Limits.HasLimits CategoryTheory.Cat

            The category of small categories has all small limits.

            Equations
            source
            instance CategoryTheory.Cat.instPreservesLimitsCatCategoryTypeTypesObjects :
            CategoryTheory.Limits.PreservesLimits CategoryTheory.Cat.objects
            Equations