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} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CategoryTheory.Cat} {j : J} : CategoryTheory.SmallCategory ((F.comp CategoryTheory.Cat.objects).obj j)

Equations

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

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

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.Cat.HasLimits.instCategoryLimitCompObjects F = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

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

@[simp]

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

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

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

@[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 (F.comp CategoryTheory.Cat.objects)

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

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.

@[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 (F.comp CategoryTheory.Cat.objects)), ((CategoryTheory.Cat.HasLimits.limitCone F).π.app j).obj a = CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) j a

@[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).obj (CategoryTheory.Cat.HasLimits.limitConeX F)).obj j)} (f : X ⟶ Y), ((CategoryTheory.Cat.HasLimits.limitCone F).π.app j).map f = CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram X Y) j f

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

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.

@[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, π := { app := fun (j : J) => (s.π.app j).obj, naturality := ⋯ } }.pt), (CategoryTheory.Cat.HasLimits.limitConeLift F s).obj a = CategoryTheory.Limits.limit.lift (F.comp CategoryTheory.Cat.objects) { pt := ↑s.pt, π := { app := fun (j : J) => (s.π.app j).obj, naturality := ⋯ } } a

@[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 (F.comp CategoryTheory.Cat.objects) { pt := ↑s.pt, π := { app := fun (j : J) => (s.π.app j).obj, naturality := ⋯ } } X) (CategoryTheory.Limits.limit.lift (F.comp CategoryTheory.Cat.objects) { pt := ↑s.pt, π := { app := fun (j : J) => (s.π.app j).obj, naturality := ⋯ } } Y)) (fun (j : J) => CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((s.π.app j).map f) (CategoryTheory.eqToHom ⋯))) ⋯

@[simp]

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

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

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

instance CategoryTheory.Cat.instHasLimits : CategoryTheory.Limits.HasLimits CategoryTheory.Cat

The category of small categories has all small limits.

Equations

• CategoryTheory.Cat.instHasLimits = ⋯

instance CategoryTheory.Cat.instPreservesLimitsObjects : CategoryTheory.Limits.PreservesLimits CategoryTheory.Cat.objects

Equations

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