mathlib documentation

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} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} (F : J category_theory.over X) (j : J) :
F.to_cocone.ι.app j = (F.obj j).hom

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

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} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} (F : J category_theory.under X) (j : J) :
F.to_cone.π.app j = (F.obj j).hom
@[simp]