Connected limits in the over category

We show that the projection CostructuredArrow K B ⥤ C creates and preserves connected limits, without assuming that C has any limits. In particular, CostructuredArrow K B has any connected limit which C has.

From this we deduce the corresponding results for the over category.

def CategoryTheory.CostructuredArrow.CreatesConnected.natTransInCostructuredArrow {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {K : Functor C D} {B : D} (F : Functor J (CostructuredArrow K B)) : F.comp ((proj K B).comp K) ⟶ (Functor.const J).obj B

(Implementation) Given a diagram in CostructuredArrow K B, produce a natural transformation from the diagram legs to the specific object.

@[simp]

theorem CategoryTheory.CostructuredArrow.CreatesConnected.natTransInCostructuredArrow_app {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {K : Functor C D} {B : D} (F : Functor J (CostructuredArrow K B)) (j : J) : (natTransInCostructuredArrow F).app j = (F.obj j).hom

def CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {K : Functor C D} [IsConnected J] {B : D} {F : Functor J (CostructuredArrow K B)} (c : Limits.Cone (F.comp (proj K B))) : Limits.Cone F

(Implementation) Given a cone in the base category, raise it to a cone in CostructuredArrow K B. Note this is where the connected assumption is used.

@[simp]

theorem CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone_π_app {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {K : Functor C D} [IsConnected J] {B : D} {F : Functor J (CostructuredArrow K B)} (c : Limits.Cone (F.comp (proj K B))) (j : J) : (raiseCone c).π.app j = homMk (c.π.app j) ⋯

@[simp]

theorem CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone_pt {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {K : Functor C D} [IsConnected J] {B : D} {F : Functor J (CostructuredArrow K B)} (c : Limits.Cone (F.comp (proj K B))) : (raiseCone c).pt = mk (CategoryStruct.comp (K.map (c.π.app (Classical.arbitrary J))) (F.obj (Classical.arbitrary J)).hom)

theorem CategoryTheory.CostructuredArrow.CreatesConnected.mapCone_raiseCone {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {K : Functor C D} [IsConnected J] {B : D} {F : Functor J (CostructuredArrow K B)} (c : Limits.Cone (F.comp (proj K B))) : (proj K B).mapCone (raiseCone c) = c

def CategoryTheory.CostructuredArrow.CreatesConnected.isLimitRaiseCone {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {K : Functor C D} [IsConnected J] {B : D} {F : Functor J (CostructuredArrow K B)} {c : Limits.Cone (F.comp (proj K B))} (t : Limits.IsLimit c) : Limits.IsLimit (raiseCone c)

(Implementation) Show that the raised cone is a limit.

instance CategoryTheory.CostructuredArrow.instCreatesLimitsOfShapeProjOfIsConnected {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {K : Functor C D} [IsConnected J] {B : D} : CreatesLimitsOfShape J (proj K B)

The projection from CostructuredArrow K B to C creates any connected limit.

instance CategoryTheory.CostructuredArrow.instPreservesLimitsOfShapeProjOfIsConnected {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {K : Functor C D} [IsConnected J] {B : D} : Limits.PreservesLimitsOfShape J (proj K B)

The forgetful functor from CostructuredArrow K B preserves any connected limit.

instance CategoryTheory.CostructuredArrow.hasLimitsOfShape_of_isConnected {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {K : Functor C D} {B : D} [IsConnected J] [Limits.HasLimitsOfShape J C] : Limits.HasLimitsOfShape J (CostructuredArrow K B)

The over category has any connected limit which the original category has.

instance CategoryTheory.Over.createsLimitsOfShapeForgetOfIsConnected {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] [IsConnected J] {B : C} : CreatesLimitsOfShape J (forget B)

The forgetful functor from the over category creates any connected limit.

@[deprecated CategoryTheory.Over.createsLimitsOfShapeForgetOfIsConnected (since := "2025-09-29")]

def CategoryTheory.Over.forgetCreatesConnectedLimits {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] [IsConnected J] {B : C} : CreatesLimitsOfShape J (forget B)

Alias of CategoryTheory.Over.createsLimitsOfShapeForgetOfIsConnected.

---

The forgetful functor from the over category creates any connected limit.

instance CategoryTheory.Over.preservesLimitsOfShape_forget_of_isConnected {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] [IsConnected J] {B : C} : Limits.PreservesLimitsOfShape J (forget B)

The forgetful functor from the over category preserves any connected limit.

@[deprecated CategoryTheory.Over.preservesLimitsOfShape_forget_of_isConnected (since := "2025-09-29")]

theorem CategoryTheory.Over.forgetPreservesConnectedLimits {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] [IsConnected J] {B : C} : Limits.PreservesLimitsOfShape J (forget B)

Alias of CategoryTheory.Over.preservesLimitsOfShape_forget_of_isConnected.

---

The forgetful functor from the over category preserves any connected limit.

instance CategoryTheory.Over.hasLimitsOfShape_of_isConnected {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] {B : C} [IsConnected J] [Limits.HasLimitsOfShape J C] : Limits.HasLimitsOfShape J (Over B)

The over category has any connected limit which the original category has.

def CategoryTheory.Over.conePost {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (i : J) : Functor (Limits.Cone F) (Limits.Cone (post F))

The functor taking a cone over F to a cone over Over.post F : Over i ⥤ Over (F.obj i). This takes limit cones to limit cones when J is cofiltered. See isLimitConePost

@[simp]

theorem CategoryTheory.Over.conePost_map_hom {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (i : J) {X✝ Y✝ : Limits.Cone F} (f : X✝ ⟶ Y✝) : ((conePost F i).map f).hom = homMk f.hom ⋯

@[simp]

theorem CategoryTheory.Over.conePost_obj_pt {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (i : J) (c : Limits.Cone F) : ((conePost F i).obj c).pt = mk (c.π.app i)

@[simp]

theorem CategoryTheory.Over.conePost_obj_π_app {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (i : J) (c : Limits.Cone F) (X : Over i) : ((conePost F i).obj c).π.app X = homMk (c.π.app X.left) ⋯

def CategoryTheory.Over.conePostIso {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (i : J) : (conePost F i).comp (Limits.Cones.functoriality (post F) (forget (F.obj i))) ≅ Limits.Cones.whiskering (forget i)

conePost is compatible with the forgetful functors on over categories.

@[simp]

theorem CategoryTheory.Over.conePostIso_hom_app_hom {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (i : J) (X : Limits.Cone F) : ((conePostIso F i).hom.app X).hom = CategoryStruct.id X.pt

@[simp]

theorem CategoryTheory.Over.conePostIso_inv_app_hom {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (i : J) (X : Limits.Cone F) : ((conePostIso F i).inv.app X).hom = CategoryStruct.id X.pt

noncomputable def CategoryTheory.Over.isLimitConePost {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] [IsCofilteredOrEmpty J] {F : Functor J C} {c : Limits.Cone F} (i : J) (hc : Limits.IsLimit c) : Limits.IsLimit ((conePost F i).obj c)

The functor taking a cone over F to a cone over Over.post F : Over i ⥤ Over (F.obj i) preserves limit cones