mathlib3documentation

category_theory.limits.constructions.over.connected

Connected limits in the over category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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
noncomputable 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 }  :
noncomputable 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
@[protected, instance]
noncomputable 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
@[protected, instance]

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