# mathlibdocumentation

category_theory.limits.shapes.constructions.over.connected

# forget : over B ⥤ C creates connected limits.

def category_theory.over.creates_connected.nat_trans_in_over {J : Type v} {C : Type u} {B : C} (F : J ) :

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

Equations
def category_theory.over.creates_connected.raise_cone {J : Type v} {C : Type u} {B : C} {F : J } :

(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
@[simp]
theorem category_theory.over.creates_connected.raise_cone_π_app {J : Type v} {C : Type u} {B : C} {F : J } (j : J) :

@[simp]
theorem category_theory.over.creates_connected.raise_cone_X {J : Type v} {C : Type u} {B : C} {F : J }  :

theorem category_theory.over.creates_connected.raised_cone_lowers_to_original {J : Type v} {C : Type u} {B : C} {F : J }  :

def category_theory.over.creates_connected.raised_cone_is_limit {J : Type v} {C : Type u} {B : C} {F : J }  :

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

Equations
@[instance]
def category_theory.over.forget_creates_connected_limits {J : Type v} {C : Type u} {B : C} :

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

Equations
@[instance]
def category_theory.over.has_connected_limits {J : Type v} {C : Type u} {B : C}  :

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