# 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.

instance CategoryTheory.Over.hasColimit_of_hasColimit_comp_forget {J : Type w} {C : Type u} {X : C} (F : ) [i : ] :
Equations
• =
instance CategoryTheory.Over.instHasColimitsOfShape {J : Type w} {C : Type u} {X : C} :
Equations
• =
instance CategoryTheory.Over.instHasColimits {C : Type u} {X : C} :
Equations
• =
Equations
• CategoryTheory.Over.createsColimitsOfSize = CategoryTheory.CostructuredArrow.createsColimitsOfSize
theorem CategoryTheory.Over.epi_left_of_epi {C : Type u} {X : C} {f : } {g : } (h : f g) :
theorem CategoryTheory.Over.epi_iff_epi_left {C : Type u} {X : C} {f : } {g : } (h : f g) :
instance CategoryTheory.Over.createsColimitsOfSizeMapCompForget {C : Type u} {X : C} {Y : C} (f : X Y) :
Equations
• = let_fun this := inferInstance; this
instance CategoryTheory.Over.preservesColimitsOfSizeMap {C : Type u} {X : C} [] {Y : C} (f : X Y) :
Equations
def CategoryTheory.Over.isColimitToOver {J : Type w} {C : Type u} {F : } {c : } (hc : ) :

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

If F has a colimit, then the cocone colimit.toOver F with cocone point 𝟙 (colimit F) is also a colimit cocone.

Equations
Instances For
@[simp]
theorem CategoryTheory.Over.pullback_map {C : Type u} {X : C} {Y : C} (f : X Y) (g : ) {h : } {k : g h} :
.map k = CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst k.left) CategoryTheory.Limits.pullback.snd )
@[simp]
theorem CategoryTheory.Over.pullback_obj {C : Type u} {X : C} {Y : C} (f : X Y) (g : ) :
.obj g = CategoryTheory.Over.mk CategoryTheory.Limits.pullback.snd
def CategoryTheory.Over.pullback {C : Type u} {X : C} {Y : C} (f : X Y) :

When C has pullbacks, a morphism f : X ⟶ Y induces a functor Over Y ⥤ Over X, by pulling back a morphism along f.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Over.mapPullbackAdj {C : Type u} {A : C} {B : C} (f : A B) :

Over.map f is left adjoint to Over.pullback f.

Equations
• One or more equations did not get rendered due to their size.
Instances For

pullback (𝟙 A) : Over A ⥤ Over A is the identity functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Over.pullbackComp {C : Type u} {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :

pullback commutes with composition (up to natural isomorphism).

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Over.pullbackIsRightAdjoint {C : Type u} {A : C} {B : C} (f : A B) :
Equations
• =
instance CategoryTheory.Under.hasLimit_of_hasLimit_comp_forget {J : Type w} {C : Type u} {X : C} (F : ) [i : ] :
Equations
• =
instance CategoryTheory.Under.instHasLimitsOfShape {J : Type w} {C : Type u} {X : C} :
Equations
• =
instance CategoryTheory.Under.instHasLimits {C : Type u} {X : C} :
Equations
• =
theorem CategoryTheory.Under.mono_right_of_mono {C : Type u} {X : C} {f : } {g : } (h : f g) :
theorem CategoryTheory.Under.mono_iff_mono_right {C : Type u} {X : C} {f : } {g : } (h : f g) :
Equations
• CategoryTheory.Under.createsLimitsOfSize = CategoryTheory.StructuredArrow.createsLimitsOfSize
instance CategoryTheory.Under.createLimitsOfSizeMapCompForget {C : Type u} {X : C} {Y : C} (f : X Y) :
Equations
• = let_fun this := inferInstance; this
instance CategoryTheory.Under.preservesLimitsOfSizeMap {C : Type u} {X : C} [] {Y : C} (f : X Y) :
Equations
def CategoryTheory.Under.isLimitToUnder {J : Type w} {C : Type u} {F : } {c : } (hc : ) :

If c is a limit cone, then so is the cone c.toUnder with cone point 𝟙 c.pt.

Equations
Instances For

If F has a limit, then the cone limit.toUnder F with cone point 𝟙 (limit F) is also a limit cone.

Equations
Instances For
@[simp]
theorem CategoryTheory.Under.pushout_obj {C : Type u} {X : C} {Y : C} (f : X Y) (g : ) :
.obj g = CategoryTheory.Under.mk CategoryTheory.Limits.pushout.inr
@[simp]
theorem CategoryTheory.Under.pushout_map {C : Type u} {X : C} {Y : C} (f : X Y) (g : ) {h : } {k : g h} :
.map k = CategoryTheory.Under.homMk (CategoryTheory.Limits.pushout.desc (CategoryTheory.CategoryStruct.comp k.right CategoryTheory.Limits.pushout.inl) CategoryTheory.Limits.pushout.inr )
def CategoryTheory.Under.pushout {C : Type u} {X : C} {Y : C} (f : X Y) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For