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 v} {C : Type u} {B : C} (F : ) :
F.comp .obj B

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

Equations
• = { app := fun (j : J) => (F.obj j).hom, naturality := }
Instances For
@[simp]
@[simp]
theorem CategoryTheory.Over.CreatesConnected.raiseCone_π_app {J : Type v} {C : Type u} {B : C} {F : } (c : CategoryTheory.Limits.Cone (F.comp )) (j : J) :
= CategoryTheory.Over.homMk (c.app j)
def CategoryTheory.Over.CreatesConnected.raiseCone {J : Type v} {C : Type u} {B : C} {F : } (c : CategoryTheory.Limits.Cone (F.comp )) :

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

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

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

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

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

Equations
• One or more equations did not get rendered due to their size.
instance CategoryTheory.Over.has_connected_limits {J : Type v} {C : Type u} {B : C} :

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

Equations
• =