Limits and the category of (co)cones

This file contains results that stem from the limit API. For the definition and the category instance of Cone, please refer to Mathlib/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.

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

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

@[simp]

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

@[simp]

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

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

If F has a limit, then the limit projections can be interpreted as structured arrows limit F ⟶ F.obj -.

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.Cone.toStructuredArrowIsoToStructuredArrow {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cone F) : c.toStructuredArrow ≅ (Functor.id J).toStructuredArrow c.pt F c.π.app ⋯

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

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

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

def CategoryTheory.Limits.Cone.toStructuredArrowCompProj {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cone F) : c.toStructuredArrow.comp (StructuredArrow.proj c.pt F) ≅ 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.toStructuredArrowCompProj_hom_app {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cone F) (X : J) : c.toStructuredArrowCompProj.hom.app X = CategoryStruct.id X

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.Cone.toStructuredArrowCompToUnderCompForget {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cone F) : c.toStructuredArrow.comp ((StructuredArrow.toUnder c.pt F).comp (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.toStructuredArrowCompToUnderCompForget_hom_app {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cone F) (X : J) : c.toStructuredArrowCompToUnderCompForget.hom.app X = CategoryStruct.id (F.obj X)

@[simp]

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

@[simp]

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

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

A cone c on F : J ⥤ C lifts to a cone in Over c.pt with cone point 𝟙 c.pt.

@[simp]

theorem CategoryTheory.Limits.Cone.toUnder_pt {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cone F) : c.toUnder.pt = Under.mk (CategoryStruct.id c.pt)

@[simp]

theorem CategoryTheory.Limits.Cone.toUnder_π_app {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cone F) (j : J) : c.toUnder.π.app j = Under.homMk (c.π.app j) ⋯

noncomputable def CategoryTheory.Limits.limit.toUnder {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) [HasLimit F] : Cone ((toStructuredArrow F).comp (StructuredArrow.toUnder (limit F) F))

The limit cone for F : J ⥤ C lifts to a cocone in Under (limit F) with cone point 𝟙 (limit F). This is automatically also a limit cone.

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

c.toUnder is a lift of c under the forgetful functor.

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Cone.mapConeToUnder_inv_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cone F) : c.mapConeToUnder.inv.hom = CategoryStruct.id c.pt

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

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.Cone.toStructuredArrowCone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] {K : Functor J C} (c : Cone K) (F : Functor C D) {X : D} (f : X ⟶ F.obj c.pt) : Cone ((F.mapCone c).toStructuredArrow.comp ((StructuredArrow.map f).comp (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.toStructuredArrowCone_pt {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] {K : Functor J C} (c : Cone K) (F : Functor C D) {X : D} (f : X ⟶ F.obj c.pt) : (c.toStructuredArrowCone F f).pt = StructuredArrow.mk f

@[simp]

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

def CategoryTheory.Limits.Cone.toCostructuredArrow {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) : Functor (Cone F) (CostructuredArrow (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.toCostructuredArrow_obj {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) (c : Cone F) : (toCostructuredArrow F).obj c = CostructuredArrow.mk c.π

@[simp]

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

def CategoryTheory.Limits.Cone.fromCostructuredArrow {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) : Functor (CostructuredArrow (Functor.const J) F) (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.fromCostructuredArrow_obj_π {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) (c : CostructuredArrow (Functor.const J) F) : ((fromCostructuredArrow F).obj c).π = c.hom

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_inverse {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) : (equivCostructuredArrow F).inverse = fromCostructuredArrow F

@[simp]

theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_unitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) : (equivCostructuredArrow F).unitIso = NatIso.ofComponents eta ⋯

@[simp]

theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_counitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) : (equivCostructuredArrow F).counitIso = NatIso.ofComponents (fun (x : CostructuredArrow (Functor.const J) F) => x.eta.symm) ⋯

@[simp]

theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_functor {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) : (equivCostructuredArrow F).functor = toCostructuredArrow F

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

A cone is a limit cone iff it is terminal.

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

If F has a colimit, then the colimit inclusions can be interpreted as costructured arrows F.obj - ⟶ colimit F.

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.Cocone.toCostructuredArrowIsoToCostructuredArrow {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cocone F) : c.toCostructuredArrow ≅ (Functor.id J).toCostructuredArrow F c.pt c.ι.app ⋯

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

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

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

def CategoryTheory.Limits.Cocone.toCostructuredArrowCompProj {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cocone F) : c.toCostructuredArrow.comp (CostructuredArrow.proj F c.pt) ≅ 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.toCostructuredArrowCompProj_hom_app {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cocone F) (X : J) : c.toCostructuredArrowCompProj.hom.app X = CategoryStruct.id X

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.Cocone.toCostructuredArrowCompToOverCompForget {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cocone F) : c.toCostructuredArrow.comp ((CostructuredArrow.toOver F c.pt).comp (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.toCostructuredArrowCompToOverCompForget_inv_app {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cocone F) (X : J) : c.toCostructuredArrowCompToOverCompForget.inv.app X = CategoryStruct.id (F.obj X)

@[simp]

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

@[simp]

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

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

A cocone c on F : J ⥤ C lifts to a cocone in Over c.pt with cone point 𝟙 c.pt.

@[simp]

theorem CategoryTheory.Limits.Cocone.toOver_ι_app {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cocone F) (j : J) : c.toOver.ι.app j = Over.homMk (c.ι.app j) ⋯

@[simp]

theorem CategoryTheory.Limits.Cocone.toOver_pt {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cocone F) : c.toOver.pt = Over.mk (CategoryStruct.id c.pt)

noncomputable def CategoryTheory.Limits.colimit.toOver {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) [HasColimit F] : Cocone ((toCostructuredArrow F).comp (CostructuredArrow.toOver F (colimit F)))

The colimit cocone for F : J ⥤ C lifts to a cocone in Over (colimit F) with cone point 𝟙 (colimit F). This is automatically also a colimit cocone.

@[simp]

theorem CategoryTheory.Limits.colimit.toOver_pt {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) [HasColimit F] : (toOver F).pt = Over.mk (CategoryStruct.id (colimit F))

@[simp]

theorem CategoryTheory.Limits.colimit.toOver_ι_app {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) [HasColimit F] (j : J) : (toOver F).ι.app j = Over.homMk (ι F j) ⋯

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

c.toOver is a lift of c under the forgetful functor.

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Cocone.mapCoconeToOver_inv_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (c : Cocone F) : c.mapCoconeToOver.inv.hom = CategoryStruct.id c.pt

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

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.Cocone.toCostructuredArrowCocone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] {K : Functor J C} (c : Cocone K) (F : Functor C D) {X : D} (f : F.obj c.pt ⟶ X) : Cocone ((F.mapCocone c).toCostructuredArrow.comp ((CostructuredArrow.map f).comp (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.toCostructuredArrowCocone_pt {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] {K : Functor J C} (c : Cocone K) (F : Functor C D) {X : D} (f : F.obj c.pt ⟶ X) : (c.toCostructuredArrowCocone F f).pt = CostructuredArrow.mk f

@[simp]

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

def CategoryTheory.Limits.Cocone.toStructuredArrow {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) : Functor (Cocone F) (StructuredArrow F (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.toStructuredArrow_obj {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) (c : Cocone F) : (toStructuredArrow F).obj c = StructuredArrow.mk c.ι

@[simp]

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

def CategoryTheory.Limits.Cocone.fromStructuredArrow {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) : Functor (StructuredArrow F (Functor.const J)) (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.fromStructuredArrow_obj_ι {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) (c : StructuredArrow F (Functor.const J)) : ((fromStructuredArrow F).obj c).ι = c.hom

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_functor {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) : (equivStructuredArrow F).functor = toStructuredArrow F

@[simp]

theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_inverse {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) : (equivStructuredArrow F).inverse = fromStructuredArrow F

@[simp]

theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_counitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) : (equivStructuredArrow F).counitIso = NatIso.ofComponents (fun (x : StructuredArrow F (Functor.const J)) => x.eta.symm) ⋯

@[simp]

theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_unitIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J C) : (equivStructuredArrow F).unitIso = NatIso.ofComponents eta ⋯

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

A cocone is a colimit cocone iff it is initial.

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

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

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

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

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

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

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

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