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.

instance CategoryTheory.Over.hasColimit_of_hasColimit_comp_forget {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {X : C} (F : Functor J (Over X)) [i : Limits.HasColimit (F.comp (forget X))] : Limits.HasColimit F

instance CategoryTheory.Over.instHasColimitsOfShape {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {X : C} [Limits.HasColimitsOfShape J C] : Limits.HasColimitsOfShape J (Over X)

instance CategoryTheory.Over.instHasFiniteColimits {C : Type u} [Category.{v, u} C] {X : C} [Limits.HasFiniteColimits C] : Limits.HasFiniteColimits (Over X)

instance CategoryTheory.Over.instHasColimits {C : Type u} [Category.{v, u} C] {X : C} [Limits.HasColimits C] : Limits.HasColimits (Over X)

instance CategoryTheory.Over.instHasFiniteCoproducts {C : Type u} [Category.{v, u} C] {X : C} [Limits.HasFiniteCoproducts C] : Limits.HasFiniteCoproducts (Over X)

instance CategoryTheory.Over.createsColimitsOfSize {C : Type u} [Category.{v, u} C] {X : C} : CreatesColimitsOfSize.{w, w', v, v, max u v, u} (forget X)

theorem CategoryTheory.Over.epi_left_of_epi {C : Type u} [Category.{v, u} C] {X : C} [Limits.HasPushouts C] {f g : Over X} (h : f ⟶ g) [Epi h] : Epi h.left

theorem CategoryTheory.Over.epi_iff_epi_left {C : Type u} [Category.{v, u} C] {X : C} [Limits.HasPushouts C] {f g : Over X} (h : f ⟶ g) : Epi h ↔ Epi h.left

instance CategoryTheory.Over.createsColimitsOfSizeMapCompForget {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : CreatesColimitsOfSize.{w, w', v, v, max u v, u} ((map f).comp (forget Y))

instance CategoryTheory.Over.preservesColimitsOfSize_map {C : Type u} [Category.{v, u} C] {X : C} [Limits.HasColimitsOfSize.{w, w', v, u} C] {Y : C} (f : X ⟶ Y) : Limits.PreservesColimitsOfSize.{w, w', v, v, max u v, max u v} (map f)

def CategoryTheory.Over.isColimitToOver {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} {c : Limits.Cocone F} (hc : Limits.IsColimit c) : Limits.IsColimit c.toOver

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

def CategoryTheory.Limits.colimit.isColimitToOver {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] : IsColimit (toOver F)

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

def CategoryTheory.Over.liftCocone {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} (c : Limits.Cocone F) {X : C} (f : c.pt ⟶ X) : Limits.Cocone (Over.lift F (CategoryStruct.comp c.ι ((Functor.const J).map f)))

Given an arrow c.pt ⟶ X, the diagram J ⥤ C can be lifted to Over X ⥤ C, and the cocone c also lifts to the diagram on Over.

@[simp]

theorem CategoryTheory.Over.liftCocone_ι_app {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} (c : Limits.Cocone F) {X : C} (f : c.pt ⟶ X) (j : J) : (liftCocone c f).ι.app j = homMk (c.ι.app j) ⋯

@[simp]

theorem CategoryTheory.Over.liftCocone_pt {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} (c : Limits.Cocone F) {X : C} (f : c.pt ⟶ X) : (liftCocone c f).pt = mk f

noncomputable def CategoryTheory.Over.isColimitLiftCocone {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} (c : Limits.Cocone F) {X : C} (f : c.pt ⟶ X) (hc : Limits.IsColimit c) : Limits.IsColimit (liftCocone c f)

Over.liftCocone is limiting if the original cocone is.

instance CategoryTheory.Under.hasLimit_of_hasLimit_comp_forget {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {X : C} (F : Functor J (Under X)) [i : Limits.HasLimit (F.comp (forget X))] : Limits.HasLimit F

instance CategoryTheory.Under.instHasLimitsOfShape {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {X : C} [Limits.HasLimitsOfShape J C] : Limits.HasLimitsOfShape J (Under X)

instance CategoryTheory.Under.instHasLimits {C : Type u} [Category.{v, u} C] {X : C} [Limits.HasLimits C] : Limits.HasLimits (Under X)

theorem CategoryTheory.Under.mono_right_of_mono {C : Type u} [Category.{v, u} C] {X : C} [Limits.HasPullbacks C] {f g : Under X} (h : f ⟶ g) [Mono h] : Mono h.right

theorem CategoryTheory.Under.mono_iff_mono_right {C : Type u} [Category.{v, u} C] {X : C} [Limits.HasPullbacks C] {f g : Under X} (h : f ⟶ g) : Mono h ↔ Mono h.right

instance CategoryTheory.Under.createsLimitsOfSize {C : Type u} [Category.{v, u} C] {X : C} : CreatesLimitsOfSize.{w, w', v, v, max u v, u} (forget X)

instance CategoryTheory.Under.createLimitsOfSizeMapCompForget {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : CreatesLimitsOfSize.{w, w', v, v, max u v, u} ((map f).comp (forget X))

instance CategoryTheory.Under.preservesLimitsOfSize_map {C : Type u} [Category.{v, u} C] {X : C} [Limits.HasLimitsOfSize.{w, w', v, u} C] {Y : C} (f : X ⟶ Y) : Limits.PreservesLimitsOfSize.{w, w', v, v, max u v, max u v} (map f)

def CategoryTheory.Under.isLimitToUnder {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} {c : Limits.Cone F} (hc : Limits.IsLimit c) : Limits.IsLimit c.toUnder

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

def CategoryTheory.Limits.limit.isLimitToOver {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] : IsLimit (toUnder F)

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

def CategoryTheory.Under.liftCone {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} (c : Limits.Cone F) {X : C} (f : X ⟶ c.pt) : Limits.Cone (Under.lift F (CategoryStruct.comp ((Functor.const J).map f) c.π))

Given an arrow X ⟶ c.pt, the diagram J ⥤ C can be lifted to Under X ⥤ C, and the cone c also lifts to the diagram on Under.

@[simp]

theorem CategoryTheory.Under.liftCone_π_app {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} (c : Limits.Cone F) {X : C} (f : X ⟶ c.pt) (j : J) : (liftCone c f).π.app j = homMk (c.π.app j) ⋯

@[simp]

theorem CategoryTheory.Under.liftCone_pt {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} (c : Limits.Cone F) {X : C} (f : X ⟶ c.pt) : (liftCone c f).pt = mk f

noncomputable def CategoryTheory.Under.isLimitLiftCone {J : Type w} [Category.{w', w} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} (c : Limits.Cone F) {X : C} (f : X ⟶ c.pt) (hc : Limits.IsLimit c) : Limits.IsLimit (liftCone c f)

Under.liftCone is limiting if the original cone is.