mathlib documentation


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.

When C has pushouts, a morphism f : X ⟶ Y induces a functor under X ⥤ under Y, by pushing a morphism forward along f.