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} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (F : CategoryTheory.Functor J (CategoryTheory.Over X)) [i : CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F (CategoryTheory.Over.forget X))] : CategoryTheory.Limits.HasColimit F

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

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

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

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

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

Equations

• CategoryTheory.Over.createsColimitsOfSizeMapCompForget f = let_fun this := inferInstance; this

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

Equations

• CategoryTheory.Over.preservesColimitsOfSizeMap f = CategoryTheory.Limits.preservesColimitsOfReflectsOfPreserves (CategoryTheory.Over.map f) (CategoryTheory.Over.forget Y)

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

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.

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

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

Equations

• CategoryTheory.Limits.colimit.isColimitToOver F = CategoryTheory.Over.isColimitToOver (CategoryTheory.Limits.colimit.isColimit F)

@[simp]

theorem CategoryTheory.Over.pullback_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X ⟶ Y) (g : CategoryTheory.Over Y) {h : CategoryTheory.Over Y} {k : g ⟶ h} : (CategoryTheory.Over.pullback f).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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X ⟶ Y) (g : CategoryTheory.Over Y) : (CategoryTheory.Over.pullback f).obj g = CategoryTheory.Over.mk CategoryTheory.Limits.pullback.snd

def CategoryTheory.Over.pullback {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over X)

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.

def CategoryTheory.Over.mapPullbackAdj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {A : C} {B : C} (f : A ⟶ B) : CategoryTheory.Over.map f ⊣ CategoryTheory.Over.pullback f

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

Equations

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

def CategoryTheory.Over.pullbackId {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {A : C} : CategoryTheory.Over.pullback (CategoryTheory.CategoryStruct.id A) ≅ CategoryTheory.Functor.id (CategoryTheory.Over A)

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

Equations

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

def CategoryTheory.Over.pullbackComp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.Over.pullback (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.Functor.comp (CategoryTheory.Over.pullback g) (CategoryTheory.Over.pullback f)

pullback commutes with composition (up to natural isomorphism).

Equations

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

instance CategoryTheory.Over.pullbackIsRightAdjoint {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {A : C} {B : C} (f : A ⟶ B) : CategoryTheory.IsRightAdjoint (CategoryTheory.Over.pullback f)

Equations

• CategoryTheory.Over.pullbackIsRightAdjoint f = { left := CategoryTheory.Over.map f, adj := CategoryTheory.Over.mapPullbackAdj f }

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• CategoryTheory.Under.createsLimitsOfSize = CategoryTheory.StructuredArrow.createsLimitsOfSize

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

Equations

• CategoryTheory.Under.createLimitsOfSizeMapCompForget f = let_fun this := inferInstance; this

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

Equations

• CategoryTheory.Under.preservesLimitsOfSizeMap f = CategoryTheory.Limits.preservesLimitsOfReflectsOfPreserves (CategoryTheory.Under.map f) (CategoryTheory.Under.forget X)

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

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

Equations

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

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

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

Equations

• CategoryTheory.Limits.limit.isLimitToOver F = CategoryTheory.Under.isLimitToUnder (CategoryTheory.Limits.limit.isLimit F)

@[simp]

theorem CategoryTheory.Under.pushout_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] {X : C} {Y : C} (f : X ⟶ Y) (g : CategoryTheory.Under X) {h : CategoryTheory.Under X} {k : g ⟶ h} : (CategoryTheory.Under.pushout f).map k = CategoryTheory.Under.homMk (CategoryTheory.Limits.pushout.desc (CategoryTheory.CategoryStruct.comp k.right CategoryTheory.Limits.pushout.inl) CategoryTheory.Limits.pushout.inr ⋯) ⋯

@[simp]

theorem CategoryTheory.Under.pushout_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] {X : C} {Y : C} (f : X ⟶ Y) (g : CategoryTheory.Under X) : (CategoryTheory.Under.pushout f).obj g = CategoryTheory.Under.mk CategoryTheory.Limits.pushout.inr

def CategoryTheory.Under.pushout {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.Functor (CategoryTheory.Under X) (CategoryTheory.Under 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.