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.
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
Over.map f
is left adjoint to Over.pullback f
.
Instances For
pullback (𝟙 A) : over A ⥤ over A is the identity functor.
Instances For
pullback commutes with composition (up to natural isomorphism).
Instances For
When C
has pushouts, a morphism f : X ⟶ Y
induces a functor Under X ⥤ Under Y
,
by pushing a morphism forward along f
.