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?

@[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 Y : J} (f : X Y) (g : CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) X X CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) X Y), J.map CategoryTheory.CategoryStruct.toQuiver (Type v) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Cat.HasLimits.homDiagram X Y).toPrefunctor X Y f g = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) Y X = CategoryTheory.CategoryStruct.comp (Type v) CategoryTheory.Category.toCategoryStruct (CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj X) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj Y) (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) X) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).map f) X)) (CategoryTheory.CategoryStruct.comp ((F.map f).map g) (CategoryTheory.eqToHom (_ : CategoryTheory.CategoryStruct.comp (Type v) CategoryTheory.Category.toCategoryStruct (CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj X) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj Y) (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) X) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).map f) Y = CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) Y Y)))
@[simp]
theorem CategoryTheory.Cat.HasLimits.instCategoryLimitTypeTypesCompCatCategoryObjectsHasLimitSmall_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 => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Cat.HasLimits.homDiagram X Y) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Cat.HasLimits.homDiagram X Y)) j f) (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Cat.HasLimits.homDiagram Y Z) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Cat.HasLimits.homDiagram Y Z)) j g)) (_ : ∀ (j j' : J) (h : j j'), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j' X = CategoryTheory.CategoryStruct.comp (Type v) CategoryTheory.Category.toCategoryStruct (CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj j') (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).map h) X)) (CategoryTheory.CategoryStruct.comp ((F.map h).map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Cat.HasLimits.homDiagram X Y) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Cat.HasLimits.homDiagram X Y)) j f) (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Cat.HasLimits.homDiagram Y Z) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Cat.HasLimits.homDiagram Y Z)) j g))) (CategoryTheory.eqToHom (_ : CategoryTheory.CategoryStruct.comp (Type v) CategoryTheory.Category.toCategoryStruct (CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj j') (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).map h) Z = CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j' Z))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Cat.HasLimits.homDiagram X Y) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Cat.HasLimits.homDiagram X Y)) j' f) (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Cat.HasLimits.homDiagram Y Z) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Cat.HasLimits.homDiagram Y Z)) j' g))
@[simp]
theorem CategoryTheory.Cat.HasLimits.instCategoryLimitTypeTypesCompCatCategoryObjectsHasLimitSmall_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 => CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j X)) (_ : ∀ (j j' : J) (f : j j'), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j' X = CategoryTheory.CategoryStruct.comp (Type v) CategoryTheory.Category.toCategoryStruct (CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj j') (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).map f) X)) (CategoryTheory.CategoryStruct.comp ((F.map f).map (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j X))) (CategoryTheory.eqToHom (_ : CategoryTheory.CategoryStruct.comp (Type v) CategoryTheory.Category.toCategoryStruct (CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj j') (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).map f) X = CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j' X))) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j' X))

Auxiliary definition: the cone over the limit category.

Instances For
    @[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).map f = CategoryTheory.Limits.Types.Limit.mk (CategoryTheory.Cat.HasLimits.homDiagram (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.app j).obj } X) (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.app j).obj } Y)) (fun j => CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.app j).obj } X) = (s.app j).obj X)) (CategoryTheory.CategoryStruct.comp ((s.app j).map f) (CategoryTheory.eqToHom (_ : (s.app j).obj Y = CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.app j).obj } Y))))) (_ : ∀ (j j' : J) (h : j j'), J.map CategoryTheory.CategoryStruct.toQuiver (Type v) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Cat.HasLimits.homDiagram (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.app j).obj } X) (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.app j).obj } Y)).toPrefunctor j j' h (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.app j).obj } X) = (s.app j).obj X)) (CategoryTheory.CategoryStruct.comp ((s.app j).map f) (CategoryTheory.eqToHom (_ : (s.app j).obj Y = CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.app j).obj } Y))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j' (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.app j).obj } X) = (s.app j').obj X)) (CategoryTheory.CategoryStruct.comp ((s.app j').map f) (CategoryTheory.eqToHom (_ : (s.app j').obj Y = CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j' (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.app j).obj } Y)))))

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

    Instances For

      The category of small categories has all small limits.