Documentation

Mathlib.CategoryTheory.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 CategoryTheory.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.

Equations
  • CategoryTheory.Over.createsColimitsOfSize = CategoryTheory.CostructuredArrow.createsColimitsOfSize

If c is a colimit cocone, then so is the cocone c.toOver with cocone point 𝟙 c.pt.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    • CategoryTheory.Under.createsLimitsOfSize = CategoryTheory.StructuredArrow.createsLimitsOfSize