mathlib3 documentation


Limits and colimits in the over and under categories #

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

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 pullbacks, a morphism f : X ⟶ Y induces a functor over Y ⥤ over X, by pulling back a morphism along f.

Instances for category_theory.over.pullback