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?

instance CategoryTheory.Cat.HasLimits.categoryObjects {J : Type v} [SmallCategory J] {F : Functor J Cat} {j : J} : SmallCategory ((F.comp objects).obj j)

Equations

• CategoryTheory.Cat.HasLimits.categoryObjects = (F.obj j).str

def CategoryTheory.Cat.HasLimits.homDiagram {J : Type v} [SmallCategory J] {F : Functor J Cat} (X Y : Limits.limit (F.comp objects)) : 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.

@[simp]

theorem CategoryTheory.Cat.HasLimits.homDiagram_obj {J : Type v} [SmallCategory J] {F : Functor J Cat} (X Y : Limits.limit (F.comp objects)) (j : J) : (homDiagram X Y).obj j = (Limits.limit.π (F.comp objects) j X ⟶ Limits.limit.π (F.comp objects) j Y)

@[simp]

theorem CategoryTheory.Cat.HasLimits.homDiagram_map {J : Type v} [SmallCategory J] {F : Functor J Cat} (X Y : Limits.limit (F.comp objects)) {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) (g : Limits.limit.π (F.comp objects) X✝ X ⟶ Limits.limit.π (F.comp objects) X✝ Y) : (homDiagram X Y).map f g = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((F.map f).toFunctor.map g) (eqToHom ⋯))

instance CategoryTheory.Cat.HasLimits.instCategoryLimitCompObjects {J : Type v} [SmallCategory J] (F : Functor J Cat) : Category.{v, v} (Limits.limit (F.comp objects))

Equations

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

@[simp]

theorem CategoryTheory.Cat.HasLimits.comp_def {J : Type v} [SmallCategory J] (F : Functor J Cat) {X Y Z : Limits.limit (F.comp objects)} (f : Limits.limit (homDiagram X Y)) (g : Limits.limit (homDiagram Y Z)) : CategoryStruct.comp f g = Limits.Types.Limit.mk (homDiagram X Z) (fun (j : J) => CategoryStruct.comp (Limits.limit.π (homDiagram X Y) j f) (Limits.limit.π (homDiagram Y Z) j g)) ⋯

@[simp]

theorem CategoryTheory.Cat.HasLimits.id_def {J : Type v} [SmallCategory J] (F : Functor J Cat) (X : Limits.limit (F.comp objects)) : CategoryStruct.id X = Limits.Types.Limit.mk (homDiagram X X) (fun (x : J) => CategoryStruct.id (Limits.limit.π (F.comp objects) x X)) ⋯

def CategoryTheory.Cat.HasLimits.limitConeX {J : Type v} [SmallCategory J] (F : Functor J Cat) : Cat

Auxiliary definition: the limit category.

Equations

• CategoryTheory.Cat.HasLimits.limitConeX F = { α := CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects), str := inferInstance }

@[simp]

theorem CategoryTheory.Cat.HasLimits.limitConeX_str {J : Type v} [SmallCategory J] (F : Functor J Cat) : (limitConeX F).str = inferInstance

@[simp]

theorem CategoryTheory.Cat.HasLimits.limitConeX_α {J : Type v} [SmallCategory J] (F : Functor J Cat) : ↑(limitConeX F) = Limits.limit (F.comp objects)

def CategoryTheory.Cat.HasLimits.limitCone {J : Type v} [SmallCategory J] (F : Functor J Cat) : Limits.Cone F

Auxiliary definition: the cone over the limit category.

Equations

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

@[simp]

theorem CategoryTheory.Cat.HasLimits.limitCone_pt {J : Type v} [SmallCategory J] (F : Functor J Cat) : (limitCone F).pt = limitConeX F

@[simp]

theorem CategoryTheory.Cat.HasLimits.limitCone_π_app {J : Type v} [SmallCategory J] (F : Functor J Cat) (j : J) : (limitCone F).π.app j = { obj := Limits.limit.π (F.comp objects) j, map := fun {X Y : Limits.limit (F.comp objects)} (f : X ⟶ Y) => Limits.limit.π (homDiagram X Y) j f, map_id := ⋯, map_comp := ⋯ }.toCatHom

def CategoryTheory.Cat.HasLimits.limitConeLift {J : Type v} [SmallCategory J] (F : Functor J Cat) (s : Limits.Cone F) : s.pt ⟶ 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.

@[simp]

theorem CategoryTheory.Cat.HasLimits.limitConeLift_toFunctor {J : Type v} [SmallCategory J] (F : Functor J Cat) (s : Limits.Cone F) : (limitConeLift F s).toFunctor = { obj := Limits.limit.lift (F.comp objects) { pt := ↑s.pt, π := { app := fun (j : J) => (s.π.app j).toFunctor.obj, naturality := ⋯ } }, map := fun {X Y : ↑s.1} (f : X ⟶ Y) => Limits.Types.Limit.mk (homDiagram (Limits.limit.lift (F.comp objects) { pt := ↑s.pt, π := { app := fun (j : J) => (s.π.app j).toFunctor.obj, naturality := ⋯ } } X) (Limits.limit.lift (F.comp objects) { pt := ↑s.pt, π := { app := fun (j : J) => (s.π.app j).toFunctor.obj, naturality := ⋯ } } Y)) (fun (j : J) => CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((s.π.app j).toFunctor.map f) (eqToHom ⋯))) ⋯, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Cat.HasLimits.limit_π_homDiagram_eqToHom {J : Type v} [SmallCategory J] {F : Functor J Cat} (X Y : Limits.limit (F.comp objects)) (j : J) (h : X = Y) : Limits.limit.π (homDiagram X Y) j (eqToHom h) = eqToHom ⋯

def CategoryTheory.Cat.HasLimits.limitConeIsLimit {J : Type v} [SmallCategory J] (F : Functor J Cat) : Limits.IsLimit (limitCone F)

Auxiliary definition: the proposed cone is a limit cone.

Equations

• CategoryTheory.Cat.HasLimits.limitConeIsLimit F = { lift := CategoryTheory.Cat.HasLimits.limitConeLift F, fac := ⋯, uniq := ⋯ }

instance CategoryTheory.Cat.instHasLimits : Limits.HasLimits Cat

The category of small categories has all small limits.

instance CategoryTheory.Cat.instPreservesLimitsObjects : Limits.PreservesLimits objects