# mathlib3documentation

category_theory.category.Cat.limit

# The category of small categories has all small limits. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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?

@[protected, instance]
Equations

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

Equations
@[simp]
theorem category_theory.Cat.has_limits.hom_diagram_map {J : Type v} {F : J category_theory.Cat} (j j' : J) (f : j j')  :
= (F.map f).map g
@[simp]
@[protected, instance]
Equations
@[simp]

Auxiliary definition: the limit category.

Equations
@[simp]
@[simp]
@[simp]

Auxiliary definition: the cone over the limit category.

Equations
@[simp]
theorem category_theory.Cat.has_limits.limit_cone_lift_map {J : Type v} (F : J category_theory.Cat) (X Y : (s.X)) (f : X Y) :
= category_theory.limits.types.limit.mk (category_theory.Cat.has_limits.hom_diagram {X := (s.X), π := {app := λ (j : J), (s.π.app j).obj, naturality' := _}} X) {X := (s.X), π := {app := λ (j : J), (s.π.app j).obj, naturality' := _}} Y)) (λ (j : J), (s.π.app j).map f _

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

Equations
@[simp]
theorem category_theory.Cat.has_limits.limit_cone_lift_obj {J : Type v} (F : J category_theory.Cat) (ᾰ : {X := (s.X), π := {app := λ (j : J), (s.π.app j).obj, naturality' := _}}.X) :
= {X := (s.X), π := {app := λ (j : J), (s.π.app j).obj, naturality' := _}}

Auxiliary definition: the proposed cone is a limit cone.

Equations
@[protected, instance]

The category of small categories has all small limits.

@[protected, instance]
Equations