Limits and the category of (co)cones

This files contains results that stem from the limit API. For the definition and the category instance of Cone, please refer to CategoryTheory/Limits/Cones.lean.

Main results

• The category of cones on F : J ⥤ C is equivalent to the category CostructuredArrow (const J) F.
• A cone is limiting iff it is terminal in the category of cones. As a corollary, an equivalence of categories of cones preserves limiting properties.

@[simp]

theorem CategoryTheory.Limits.Cone.toStructuredArrow_map {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : ∀ {X Y : J} (f : X ⟶ Y), (CategoryTheory.Limits.Cone.toStructuredArrow c).map f = CategoryTheory.StructuredArrow.homMk f

@[simp]

theorem CategoryTheory.Limits.Cone.toStructuredArrow_obj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (j : J) : (CategoryTheory.Limits.Cone.toStructuredArrow c).obj j = CategoryTheory.StructuredArrow.mk (c.π.app j)

def CategoryTheory.Limits.Cone.toStructuredArrow {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Functor J (CategoryTheory.StructuredArrow c.pt F)

Given a cone c over F, we can interpret the legs of c as structured arrows c.pt ⟶ F.obj -.

def CategoryTheory.Limits.Cone.toStructuredArrowIsoToStructuredArrow {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Cone.toStructuredArrow c ≅ CategoryTheory.Functor.toStructuredArrow (CategoryTheory.Functor.id J) c.pt F c.π.app (_ : ∀ (a a_1 : J) (a_2 : a ⟶ a_1), CategoryTheory.CategoryStruct.comp (c.π.app a) (F.map a_2) = c.π.app a_1)

Cone.toStructuredArrow can be expressed in terms of Functor.toStructuredArrow.

def CategoryTheory.Functor.toStructuredArrowIsoToStructuredArrow {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (G : CategoryTheory.Functor J K) (X : C) (F : CategoryTheory.Functor K C) (f : (Y : J) → X ⟶ F.obj (G.obj Y)) (h : ∀ {Y Z : J} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z) : (CategoryTheory.Functor.toStructuredArrow G X F f fun {Y Z} => h Y Z) ≅ CategoryTheory.Functor.comp (CategoryTheory.Limits.Cone.toStructuredArrow { pt := X, π := CategoryTheory.NatTrans.mk f }) (CategoryTheory.StructuredArrow.pre { pt := X, π := CategoryTheory.NatTrans.mk f }.pt G F)

Functor.toStructuredArrow can be expressed in terms of Cone.toStructuredArrow.

@[simp]

theorem CategoryTheory.Limits.Cone.toStructuredArrowCompProj_hom_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (X : J) : (CategoryTheory.Limits.Cone.toStructuredArrowCompProj c).hom.app X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.Cone.toStructuredArrowCompProj_inv_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (X : J) : (CategoryTheory.Limits.Cone.toStructuredArrowCompProj c).inv.app X = CategoryTheory.CategoryStruct.id X

def CategoryTheory.Limits.Cone.toStructuredArrowCompProj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Functor.comp (CategoryTheory.Limits.Cone.toStructuredArrow c) (CategoryTheory.StructuredArrow.proj c.pt F) ≅ CategoryTheory.Functor.id J

Interpreting the legs of a cone as a structured arrow and then forgetting the arrow again does nothing.

@[simp]

theorem CategoryTheory.Limits.Cone.toStructuredArrow_comp_proj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Functor.comp (CategoryTheory.Limits.Cone.toStructuredArrow c) (CategoryTheory.StructuredArrow.proj c.pt F) = CategoryTheory.Functor.id J

@[simp]

theorem CategoryTheory.Limits.Cone.toStructuredArrowCompToUnderCompForget_hom_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (X : J) : (CategoryTheory.Limits.Cone.toStructuredArrowCompToUnderCompForget c).hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.Limits.Cone.toStructuredArrowCompToUnderCompForget_inv_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (X : J) : (CategoryTheory.Limits.Cone.toStructuredArrowCompToUnderCompForget c).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)

def CategoryTheory.Limits.Cone.toStructuredArrowCompToUnderCompForget {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Functor.comp (CategoryTheory.Limits.Cone.toStructuredArrow c) (CategoryTheory.Functor.comp (CategoryTheory.StructuredArrow.toUnder c.pt F) (CategoryTheory.Under.forget c.pt)) ≅ F

Interpreting the legs of a cone as a structured arrow, interpreting this arrow as an arrow over the cone point, and finally forgetting the arrow is the same as just applying the functor the cone was over.

@[simp]

theorem CategoryTheory.Limits.Cone.toStructuredArrow_comp_toUnder_comp_forget {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Functor.comp (CategoryTheory.Limits.Cone.toStructuredArrow c) (CategoryTheory.Functor.comp (CategoryTheory.StructuredArrow.toUnder c.pt F) (CategoryTheory.Under.forget c.pt)) = F

@[simp]

theorem CategoryTheory.Limits.Cone.fromStructuredArrow_π_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) {X : D} (G : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X F)) (j : J) : (CategoryTheory.Limits.Cone.fromStructuredArrow F G).π.app j = (G.obj j).hom

@[simp]

theorem CategoryTheory.Limits.Cone.fromStructuredArrow_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) {X : D} (G : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X F)) : (CategoryTheory.Limits.Cone.fromStructuredArrow F G).pt = X

def CategoryTheory.Limits.Cone.fromStructuredArrow {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) {X : D} (G : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X F)) : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp G (CategoryTheory.Functor.comp (CategoryTheory.StructuredArrow.proj X F) F))

Given a diagram of StructuredArrow X Fs, we may obtain a cone with cone point X.

@[simp]

theorem CategoryTheory.Limits.Cone.toStructuredArrowCone_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone K) (F : CategoryTheory.Functor C D) {X : D} (f : X ⟶ F.obj c.pt) : (CategoryTheory.Limits.Cone.toStructuredArrowCone c F f).pt = CategoryTheory.StructuredArrow.mk f

@[simp]

theorem CategoryTheory.Limits.Cone.toStructuredArrowCone_π_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone K) (F : CategoryTheory.Functor C D) {X : D} (f : X ⟶ F.obj c.pt) (j : J) : (CategoryTheory.Limits.Cone.toStructuredArrowCone c F f).π.app j = CategoryTheory.StructuredArrow.homMk (c.π.app j)

def CategoryTheory.Limits.Cone.toStructuredArrowCone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone K) (F : CategoryTheory.Functor C D) {X : D} (f : X ⟶ F.obj c.pt) : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp (CategoryTheory.Limits.Cone.toStructuredArrow (F.mapCone c)) (CategoryTheory.Functor.comp (CategoryTheory.StructuredArrow.map f) (CategoryTheory.StructuredArrow.pre X K F)))

Given a cone c : Cone K and a map f : X ⟶ F.obj c.X, we can construct a cone of structured arrows over X with f as the cone point.

@[simp]

theorem CategoryTheory.Limits.Cone.toCostructuredArrow_obj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cone.toCostructuredArrow F).obj c = CategoryTheory.CostructuredArrow.mk c.π

@[simp]

theorem CategoryTheory.Limits.Cone.toCostructuredArrow_map {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : ∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), (CategoryTheory.Limits.Cone.toCostructuredArrow F).map f = CategoryTheory.CostructuredArrow.homMk f.hom

def CategoryTheory.Limits.Cone.toCostructuredArrow {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F)

Construct an object of the category (Δ ↓ F) from a cone on F. This is part of an equivalence, see Cone.equivCostructuredArrow.

@[simp]

theorem CategoryTheory.Limits.Cone.fromCostructuredArrow_map_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : ∀ {X Y : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cone.fromCostructuredArrow F).map f).hom = f.left

@[simp]

theorem CategoryTheory.Limits.Cone.fromCostructuredArrow_obj_π {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F) : ((CategoryTheory.Limits.Cone.fromCostructuredArrow F).obj c).π = c.hom

@[simp]

theorem CategoryTheory.Limits.Cone.fromCostructuredArrow_obj_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F) : ((CategoryTheory.Limits.Cone.fromCostructuredArrow F).obj c).pt = c.left

def CategoryTheory.Limits.Cone.fromCostructuredArrow {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Functor (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F) (CategoryTheory.Limits.Cone F)

Construct a cone on F from an object of the category (Δ ↓ F). This is part of an equivalence, see Cone.equivCostructuredArrow.

@[simp]

theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_counitIso_hom_app_right {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F) : ((CategoryTheory.Limits.Cone.equivCostructuredArrow F).counitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_functor_map_right {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : ∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cone.equivCostructuredArrow F).functor.map f).right = CategoryTheory.CategoryStruct.id { as := PUnit.unit }

@[simp]

theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_functor_obj_right_as {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.Cone.equivCostructuredArrow F).functor.obj c).right.as = PUnit.unit

@[simp]

theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_inverse_obj_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F) : ((CategoryTheory.Limits.Cone.equivCostructuredArrow F).inverse.obj c).pt = c.left

@[simp]

theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_unitIso_inv_app_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.Cone.equivCostructuredArrow F).unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt

@[simp]

theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_functor_obj_left {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.Cone.equivCostructuredArrow F).functor.obj c).left = c.pt

@[simp]

theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_counitIso_hom_app_left {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F) : ((CategoryTheory.Limits.Cone.equivCostructuredArrow F).counitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_counitIso_inv_app_left {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F) : ((CategoryTheory.Limits.Cone.equivCostructuredArrow F).counitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_functor_map_left {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : ∀ {X Y : CategoryTheory.Limits.Cone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cone.equivCostructuredArrow F).functor.map f).left = f.hom

@[simp]

theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_functor_obj_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.Cone.equivCostructuredArrow F).functor.obj c).hom = c.π

@[simp]

theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_counitIso_inv_app_right {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F) : ((CategoryTheory.Limits.Cone.equivCostructuredArrow F).counitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_inverse_obj_π {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F) : ((CategoryTheory.Limits.Cone.equivCostructuredArrow F).inverse.obj c).π = c.hom

@[simp]

theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_inverse_map_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : ∀ {X Y : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cone.equivCostructuredArrow F).inverse.map f).hom = f.left

@[simp]

theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_unitIso_hom_app_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.Cone.equivCostructuredArrow F).unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt

def CategoryTheory.Limits.Cone.equivCostructuredArrow {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.Cone F ≌ CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F

The category of cones on F is just the comma category (Δ ↓ F), where Δ is the constant functor.

def CategoryTheory.Limits.Cone.isLimitEquivIsTerminal {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsTerminal c

A cone is a limit cone iff it is terminal.

theorem CategoryTheory.Limits.hasLimit_iff_hasTerminal_cone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.HasLimit F ↔ CategoryTheory.Limits.HasTerminal (CategoryTheory.Limits.Cone F)

theorem CategoryTheory.Limits.hasLimitsOfShape_iff_isLeftAdjoint_const {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] : CategoryTheory.Limits.HasLimitsOfShape J C ↔ Nonempty (CategoryTheory.IsLeftAdjoint (CategoryTheory.Functor.const J))

theorem CategoryTheory.Limits.IsLimit.liftConeMorphism_eq_isTerminal_from {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.IsLimit.liftConeMorphism hc s = CategoryTheory.Limits.IsTerminal.from (↑(CategoryTheory.Limits.Cone.isLimitEquivIsTerminal c) hc) s

theorem CategoryTheory.Limits.IsTerminal.from_eq_liftConeMorphism {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsTerminal c) (s : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.IsTerminal.from hc s = CategoryTheory.Limits.IsLimit.liftConeMorphism (↑(CategoryTheory.Limits.Cone.isLimitEquivIsTerminal c).symm hc) s

def CategoryTheory.Limits.IsLimit.ofPreservesConeTerminal {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {F' : CategoryTheory.Functor K D} (G : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone F')) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty (CategoryTheory.Limits.Cone F)) G] {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (G.obj c)

If G : Cone F ⥤ Cone F' preserves terminal objects, it preserves limit cones.

def CategoryTheory.Limits.IsLimit.ofReflectsConeTerminal {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {F' : CategoryTheory.Functor K D} (G : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone F')) [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Functor.empty (CategoryTheory.Limits.Cone F)) G] {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit (G.obj c)) : CategoryTheory.Limits.IsLimit c

If G : Cone F ⥤ Cone F' reflects terminal objects, it reflects limit cones.

@[simp]

theorem CategoryTheory.Limits.Cocone.toCostructuredArrow_obj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) (j : J) : (CategoryTheory.Limits.Cocone.toCostructuredArrow c).obj j = CategoryTheory.CostructuredArrow.mk (c.ι.app j)

@[simp]

theorem CategoryTheory.Limits.Cocone.toCostructuredArrow_map {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : ∀ {X Y : J} (f : X ⟶ Y), (CategoryTheory.Limits.Cocone.toCostructuredArrow c).map f = CategoryTheory.CostructuredArrow.homMk f

def CategoryTheory.Limits.Cocone.toCostructuredArrow {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow F c.pt)

Given a cocone c over F, we can interpret the legs of c as costructured arrows F.obj - ⟶ c.pt.

def CategoryTheory.Limits.Cocone.toCostructuredArrowIsoToCostructuredArrow {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.Cocone.toCostructuredArrow c ≅ CategoryTheory.Functor.toCostructuredArrow (CategoryTheory.Functor.id J) F c.pt c.ι.app (_ : ∀ (a a_1 : J) (a_2 : a ⟶ a_1), CategoryTheory.CategoryStruct.comp (F.map a_2) (c.ι.app a_1) = c.ι.app a)

Cocone.toCostructuredArrow can be expressed in terms of Functor.toCostructuredArrow.

def CategoryTheory.Functor.toCostructuredArrowIsoToCostructuredArrow {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (G : CategoryTheory.Functor J K) (F : CategoryTheory.Functor K C) (X : C) (f : (Y : J) → F.obj (G.obj Y) ⟶ X) (h : ∀ {Y Z : J} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y) : (CategoryTheory.Functor.toCostructuredArrow G F X f fun {Y Z} => h Y Z) ≅ CategoryTheory.Functor.comp (CategoryTheory.Limits.Cocone.toCostructuredArrow { pt := X, ι := CategoryTheory.NatTrans.mk f }) (CategoryTheory.CostructuredArrow.pre G F { pt := X, ι := CategoryTheory.NatTrans.mk f }.pt)

Functor.toCostructuredArrow can be expressed in terms of Cocone.toCostructuredArrow.

@[simp]

theorem CategoryTheory.Limits.Cocone.toCostructuredArrowCompProj_inv_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) (X : J) : (CategoryTheory.Limits.Cocone.toCostructuredArrowCompProj c).inv.app X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.Cocone.toCostructuredArrowCompProj_hom_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) (X : J) : (CategoryTheory.Limits.Cocone.toCostructuredArrowCompProj c).hom.app X = CategoryTheory.CategoryStruct.id X

def CategoryTheory.Limits.Cocone.toCostructuredArrowCompProj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Functor.comp (CategoryTheory.Limits.Cocone.toCostructuredArrow c) (CategoryTheory.CostructuredArrow.proj F c.pt) ≅ CategoryTheory.Functor.id J

Interpreting the legs of a cocone as a costructured arrow and then forgetting the arrow again does nothing.

@[simp]

theorem CategoryTheory.Limits.Cocone.toCostructuredArrow_comp_proj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Functor.comp (CategoryTheory.Limits.Cocone.toCostructuredArrow c) (CategoryTheory.CostructuredArrow.proj F c.pt) = CategoryTheory.Functor.id J

@[simp]

theorem CategoryTheory.Limits.Cocone.toCostructuredArrowCompToOverCompForget_inv_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) (X : J) : (CategoryTheory.Limits.Cocone.toCostructuredArrowCompToOverCompForget c).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.Limits.Cocone.toCostructuredArrowCompToOverCompForget_hom_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) (X : J) : (CategoryTheory.Limits.Cocone.toCostructuredArrowCompToOverCompForget c).hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)

def CategoryTheory.Limits.Cocone.toCostructuredArrowCompToOverCompForget {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Functor.comp (CategoryTheory.Limits.Cocone.toCostructuredArrow c) (CategoryTheory.Functor.comp (CategoryTheory.CostructuredArrow.toOver F c.pt) (CategoryTheory.Over.forget c.pt)) ≅ F

Interpreting the legs of a cocone as a costructured arrow, interpreting this arrow as an arrow over the cocone point, and finally forgetting the arrow is the same as just applying the functor the cocone was over.

@[simp]

theorem CategoryTheory.Limits.Cocone.toCostructuredArrow_comp_toOver_comp_forget {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Functor.comp (CategoryTheory.Limits.Cocone.toCostructuredArrow c) (CategoryTheory.Functor.comp (CategoryTheory.CostructuredArrow.toOver F c.pt) (CategoryTheory.Over.forget c.pt)) = F

@[simp]

theorem CategoryTheory.Limits.Cocone.fromCostructuredArrow_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) {X : D} (G : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow F X)) : (CategoryTheory.Limits.Cocone.fromCostructuredArrow F G).pt = X

@[simp]

theorem CategoryTheory.Limits.Cocone.fromCostructuredArrow_ι_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) {X : D} (G : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow F X)) (j : J) : (CategoryTheory.Limits.Cocone.fromCostructuredArrow F G).ι.app j = (G.obj j).hom

def CategoryTheory.Limits.Cocone.fromCostructuredArrow {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) {X : D} (G : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow F X)) : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp G (CategoryTheory.Functor.comp (CategoryTheory.CostructuredArrow.proj F X) F))

Given a diagram CostructuredArrow F Xs, we may obtain a cocone with cone point X.

@[simp]

theorem CategoryTheory.Limits.Cocone.toCostructuredArrowCocone_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone K) (F : CategoryTheory.Functor C D) {X : D} (f : F.obj c.pt ⟶ X) : (CategoryTheory.Limits.Cocone.toCostructuredArrowCocone c F f).pt = CategoryTheory.CostructuredArrow.mk f

@[simp]

theorem CategoryTheory.Limits.Cocone.toCostructuredArrowCocone_ι_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone K) (F : CategoryTheory.Functor C D) {X : D} (f : F.obj c.pt ⟶ X) (j : J) : (CategoryTheory.Limits.Cocone.toCostructuredArrowCocone c F f).ι.app j = CategoryTheory.CostructuredArrow.homMk (c.ι.app j)

def CategoryTheory.Limits.Cocone.toCostructuredArrowCocone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone K) (F : CategoryTheory.Functor C D) {X : D} (f : F.obj c.pt ⟶ X) : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp (CategoryTheory.Limits.Cocone.toCostructuredArrow (F.mapCocone c)) (CategoryTheory.Functor.comp (CategoryTheory.CostructuredArrow.map f) (CategoryTheory.CostructuredArrow.pre K F X)))

Given a cocone c : Cocone K and a map f : F.obj c.X ⟶ X, we can construct a cocone of costructured arrows over X with f as the cone point.

@[simp]

theorem CategoryTheory.Limits.Cocone.toStructuredArrow_map {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : ∀ {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y), (CategoryTheory.Limits.Cocone.toStructuredArrow F).map f = CategoryTheory.StructuredArrow.homMk f.hom

@[simp]

theorem CategoryTheory.Limits.Cocone.toStructuredArrow_obj {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.Cocone.toStructuredArrow F).obj c = CategoryTheory.StructuredArrow.mk c.ι

def CategoryTheory.Limits.Cocone.toStructuredArrow {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) (CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J))

Construct an object of the category (F ↓ Δ) from a cocone on F. This is part of an equivalence, see Cocone.equivStructuredArrow.

@[simp]

theorem CategoryTheory.Limits.Cocone.fromStructuredArrow_obj_ι {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)) : ((CategoryTheory.Limits.Cocone.fromStructuredArrow F).obj c).ι = c.hom

@[simp]

theorem CategoryTheory.Limits.Cocone.fromStructuredArrow_map_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : ∀ {X Y : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)} (f : X ⟶ Y), ((CategoryTheory.Limits.Cocone.fromStructuredArrow F).map f).hom = f.right

@[simp]

theorem CategoryTheory.Limits.Cocone.fromStructuredArrow_obj_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)) : ((CategoryTheory.Limits.Cocone.fromStructuredArrow F).obj c).pt = c.right

def CategoryTheory.Limits.Cocone.fromStructuredArrow {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Functor (CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)) (CategoryTheory.Limits.Cocone F)

Construct a cocone on F from an object of the category (F ↓ Δ). This is part of an equivalence, see Cocone.equivStructuredArrow.

@[simp]

theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_functor_map_right {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : ∀ {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cocone.equivStructuredArrow F).functor.map f).right = f.hom

@[simp]

theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_inverse_obj_pt {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)) : ((CategoryTheory.Limits.Cocone.equivStructuredArrow F).inverse.obj c).pt = c.right

@[simp]

theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_functor_obj_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cocone F) : ((CategoryTheory.Limits.Cocone.equivStructuredArrow F).functor.obj c).hom = c.ι

@[simp]

theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_functor_obj_right {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cocone F) : ((CategoryTheory.Limits.Cocone.equivStructuredArrow F).functor.obj c).right = c.pt

@[simp]

theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_counitIso_hom_app_right {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)) : ((CategoryTheory.Limits.Cocone.equivStructuredArrow F).counitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_unitIso_inv_app_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : CategoryTheory.Limits.Cocone F) : ((CategoryTheory.Limits.Cocone.equivStructuredArrow F).unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt

@[simp]

theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_inverse_map_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : ∀ {X Y : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)} (f : X ⟶ Y), ((CategoryTheory.Limits.Cocone.equivStructuredArrow F).inverse.map f).hom = f.right

@[simp]

theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_counitIso_hom_app_left {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)) : ((CategoryTheory.Limits.Cocone.equivStructuredArrow F).counitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_functor_map_left {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : ∀ {X Y : CategoryTheory.Limits.Cocone F} (f : X ⟶ Y), ((CategoryTheory.Limits.Cocone.equivStructuredArrow F).functor.map f).left = CategoryTheory.CategoryStruct.id { as := PUnit.unit }

@[simp]

theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_counitIso_inv_app_right {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)) : ((CategoryTheory.Limits.Cocone.equivStructuredArrow F).counitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_unitIso_hom_app_hom {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : CategoryTheory.Limits.Cocone F) : ((CategoryTheory.Limits.Cocone.equivStructuredArrow F).unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt

@[simp]

theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_counitIso_inv_app_left {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (X : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)) : ((CategoryTheory.Limits.Cocone.equivStructuredArrow F).counitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_inverse_obj_ι {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)) : ((CategoryTheory.Limits.Cocone.equivStructuredArrow F).inverse.obj c).ι = c.hom

@[simp]

theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_functor_obj_left_as {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cocone F) : ((CategoryTheory.Limits.Cocone.equivStructuredArrow F).functor.obj c).left.as = PUnit.unit

def CategoryTheory.Limits.Cocone.equivStructuredArrow {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.Cocone F ≌ CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)

The category of cocones on F is just the comma category (F ↓ Δ), where Δ is the constant functor.

def CategoryTheory.Limits.Cocone.isColimitEquivIsInitial {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.IsColimit c ≃ CategoryTheory.Limits.IsInitial c

A cocone is a colimit cocone iff it is initial.

theorem CategoryTheory.Limits.hasColimit_iff_hasInitial_cocone {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.HasColimit F ↔ CategoryTheory.Limits.HasInitial (CategoryTheory.Limits.Cocone F)

theorem CategoryTheory.Limits.hasColimitsOfShape_iff_isRightAdjoint_const {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] : CategoryTheory.Limits.HasColimitsOfShape J C ↔ Nonempty (CategoryTheory.IsRightAdjoint (CategoryTheory.Functor.const J))

theorem CategoryTheory.Limits.IsColimit.descCoconeMorphism_eq_isInitial_to {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.IsColimit.descCoconeMorphism hc s = CategoryTheory.Limits.IsInitial.to (↑(CategoryTheory.Limits.Cocone.isColimitEquivIsInitial c) hc) s

theorem CategoryTheory.Limits.IsInitial.to_eq_descCoconeMorphism {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsInitial c) (s : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.IsInitial.to hc s = CategoryTheory.Limits.IsColimit.descCoconeMorphism (↑(CategoryTheory.Limits.Cocone.isColimitEquivIsInitial c).symm hc) s

def CategoryTheory.Limits.IsColimit.ofPreservesCoconeInitial {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {F' : CategoryTheory.Functor K D} (G : CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) (CategoryTheory.Limits.Cocone F')) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty (CategoryTheory.Limits.Cocone F)) G] {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (G.obj c)

If G : Cocone F ⥤ Cocone F' preserves initial objects, it preserves colimit cocones.

def CategoryTheory.Limits.IsColimit.ofReflectsCoconeInitial {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {F' : CategoryTheory.Functor K D} (G : CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) (CategoryTheory.Limits.Cocone F')) [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.empty (CategoryTheory.Limits.Cocone F)) G] {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit (G.obj c)) : CategoryTheory.Limits.IsColimit c

If G : Cocone F ⥤ Cocone F' reflects initial objects, it reflects colimit cocones.