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'} [CategoryTheory.Category.{v', u'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} (F : CategoryTheory.Functor J (CategoryTheory.Over B)) : F.comp (CategoryTheory.Over.forget B) ⟶ (CategoryTheory.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.

Equations

• CategoryTheory.Over.CreatesConnected.natTransInOver F = { app := fun (j : J) => (F.obj j).hom, naturality := ⋯ }

def CategoryTheory.Over.CreatesConnected.raiseCone {J : Type u'} [CategoryTheory.Category.{v', u'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsConnected J] {B : C} {F : CategoryTheory.Functor J (CategoryTheory.Over B)} (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Over.forget B))) : CategoryTheory.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.

Equations

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

@[simp]

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

@[simp]

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

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

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

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

Equations

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

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

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 u'} [CategoryTheory.Category.{v', u'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} [CategoryTheory.IsConnected J] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Over B)

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

Equations

• ⋯ = ⋯