Connected limits in the over category

Shows that the forgetful functor Over B ⥤ C creates connected limits, in particular Over B has any connected limit which C has.

def CategoryTheory.Over.CreatesConnected.natTransInOver {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] {B : C} (F : Functor J (Over B)) : F.comp (forget B) ⟶ (Functor.const J).obj B

(Impl) Given a diagram in the over category, produce a natural transformation from the diagram legs to the specific object.

def CategoryTheory.Over.CreatesConnected.raiseCone {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] [IsConnected J] {B : C} {F : Functor J (Over B)} (c : Limits.Cone (F.comp (forget B))) : Limits.Cone F

(Impl) Given a cone in the base category, raise it to a cone in the over category. Note this is where the connected assumption is used.

@[simp]

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

@[simp]

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

theorem CategoryTheory.Over.CreatesConnected.raised_cone_lowers_to_original {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] [IsConnected J] {B : C} {F : Functor J (Over B)} (c : Limits.Cone (F.comp (forget B))) : (forget B).mapCone (raiseCone c) = c

def CategoryTheory.Over.CreatesConnected.raisedConeIsLimit {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] [IsConnected J] {B : C} {F : Functor J (Over B)} {c : Limits.Cone (F.comp (forget B))} (t : Limits.IsLimit c) : Limits.IsLimit (raiseCone c)

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

instance 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)

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

instance CategoryTheory.Over.has_connected_limits {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.