# mathlibdocumentation

category_theory.limits.over

# Limits and colimits in the over and under categories

Show that the forgetful functor forget X : over X ⥤ C creates colimits, and hence over X has any colimits that C has (as well as the dual that forget X : under X ⟶ C creates limits).

Note that the folder category_theory.limits.shapes.constructions.over further shows that forget X : over X ⥤ C creates connected limits (so over X has connected limits), and that over X has J-indexed products if C has J-indexed wide pullbacks.

TODO: If C has binary products, then forget X : over X ⥤ C has a right adjoint.

@[simp]
theorem category_theory.functor.to_cocone_ι_app {J : Type v} {C : Type u} {X : C} (F : J ) (j : J) :
F.to_cocone.ι.app j = (F.obj j).hom

@[simp]
theorem category_theory.functor.to_cocone_X {J : Type v} {C : Type u} {X : C} (F : J ) :

def category_theory.functor.to_cocone {J : Type v} {C : Type u} {X : C} (F : J ) :

We can interpret a functor F into the category of arrows with codomain X as a cocone over the diagram given by the domains of the arrows in the image of F such that the apex of the cocone is X.

Equations
def category_theory.functor.to_cone {J : Type v} {C : Type u} {X : C} (F : J ) :

We can interpret a functor F into the category of arrows with domain X as a cone over the diagram given by the codomains of the arrows in the image of F such that the apex of the cone is X.

Equations
@[simp]
theorem category_theory.functor.to_cone_π_app {J : Type v} {C : Type u} {X : C} (F : J ) (j : J) :
F.to_cone.π.app j = (F.obj j).hom

@[simp]
theorem category_theory.functor.to_cone_X {J : Type v} {C : Type u} {X : C} (F : J ) :
F.to_cone.X = X

@[instance]

Equations
@[instance]

Equations
@[instance]
def category_theory.over.has_colimit {J : Type v} {C : Type u} {X : C} {F : J }  :

@[instance]
def category_theory.over.has_colimits_of_shape {J : Type v} {C : Type u} {X : C}  :

@[instance]

@[instance]

Equations
@[instance]

Equations
@[instance]
def category_theory.under.has_limit {J : Type v} {C : Type u} {X : C} {F : J }  :

@[instance]
def category_theory.under.has_limits_of_shape {J : Type v} {C : Type u} {X : C}  :

@[instance]
def category_theory.under.has_limits {C : Type u} {X : C}  :