# 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₁} [] {C : Type u₃} [] {F : } (c : ) :
∀ {X Y : J} (f : X Y), c.toStructuredArrow.map f =
@[simp]
theorem CategoryTheory.Limits.Cone.toStructuredArrow_obj {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) (j : J) :
c.toStructuredArrow.obj j = CategoryTheory.StructuredArrow.mk (c.app j)
def CategoryTheory.Limits.Cone.toStructuredArrow {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.limit.toStructuredArrow_map {J : Type u₁} [] {C : Type u₃} [] (F : ) :
∀ {X Y : J} (f : X Y),
@[simp]
theorem CategoryTheory.Limits.limit.toStructuredArrow_obj {J : Type u₁} [] {C : Type u₃} [] (F : ) (j : J) :
noncomputable def CategoryTheory.Limits.limit.toStructuredArrow {J : Type u₁} [] {C : Type u₃} [] (F : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.Cone.toStructuredArrowIsoToStructuredArrow {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.toStructuredArrow .toStructuredArrow c.pt F c.app

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

Equations
Instances For
def CategoryTheory.Functor.toStructuredArrowIsoToStructuredArrow {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] (G : ) (X : C) (F : ) (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) :
G.toStructuredArrow X F f { pt := X, π := { app := f, naturality := } }.toStructuredArrow.comp (CategoryTheory.StructuredArrow.pre { pt := X, π := { app := f, naturality := } }.pt G F)

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cone.toStructuredArrowCompProj_hom_app {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) (X : J) :
c.toStructuredArrowCompProj.hom.app X =
@[simp]
theorem CategoryTheory.Limits.Cone.toStructuredArrowCompProj_inv_app {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) (X : J) :
c.toStructuredArrowCompProj.inv.app X =
def CategoryTheory.Limits.Cone.toStructuredArrowCompProj {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.toStructuredArrow.comp ()

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cone.toStructuredArrow_comp_proj {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.toStructuredArrow.comp () =
@[simp]
theorem CategoryTheory.Limits.Cone.toStructuredArrowCompToUnderCompForget_inv_app {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) (X : J) :
c.toStructuredArrowCompToUnderCompForget.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
@[simp]
theorem CategoryTheory.Limits.Cone.toStructuredArrowCompToUnderCompForget_hom_app {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) (X : J) :
c.toStructuredArrowCompToUnderCompForget.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
def CategoryTheory.Limits.Cone.toStructuredArrowCompToUnderCompForget {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.toStructuredArrow.comp (.comp ()) 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.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cone.toStructuredArrow_comp_toUnder_comp_forget {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.toStructuredArrow.comp (.comp ()) = F
@[simp]
theorem CategoryTheory.Limits.Cone.toUnder_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.toUnder.pt =
@[simp]
theorem CategoryTheory.Limits.Cone.toUnder_π_app {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) (j : J) :
c.toUnder.app j = CategoryTheory.Under.homMk (c.app j)
def CategoryTheory.Limits.Cone.toUnder {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
CategoryTheory.Limits.Cone (c.toStructuredArrow.comp )

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

Equations
Instances For
noncomputable def CategoryTheory.Limits.limit.toUnder {J : Type u₁} [] {C : Type u₃} [] (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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cone.mapConeToUnder_hom_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.mapConeToUnder.hom.hom =
@[simp]
theorem CategoryTheory.Limits.Cone.mapConeToUnder_inv_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.mapConeToUnder.inv.hom =
def CategoryTheory.Limits.Cone.mapConeToUnder {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
().mapCone c.toUnder c

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cone.fromStructuredArrow_pt {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) {X : D} (G : ) :
@[simp]
theorem CategoryTheory.Limits.Cone.fromStructuredArrow_π_app {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) {X : D} (G : ) (j : J) :
.app j = (G.obj j).hom
def CategoryTheory.Limits.Cone.fromStructuredArrow {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) {X : D} (G : ) :
CategoryTheory.Limits.Cone (G.comp (.comp F))

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

Equations
• = { pt := X, π := { app := fun (j : J) => (G.obj j).hom, naturality := } }
Instances For
@[simp]
theorem CategoryTheory.Limits.Cone.toStructuredArrowCone_pt {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {K : } (c : ) (F : ) {X : D} (f : X F.obj c.pt) :
(c.toStructuredArrowCone F f).pt =
@[simp]
theorem CategoryTheory.Limits.Cone.toStructuredArrowCone_π_app {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {K : } (c : ) (F : ) {X : D} (f : X F.obj c.pt) (j : J) :
(c.toStructuredArrowCone F f).app j = CategoryTheory.StructuredArrow.homMk (c.app j)
def CategoryTheory.Limits.Cone.toStructuredArrowCone {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {K : } (c : ) (F : ) {X : D} (f : X F.obj c.pt) :
CategoryTheory.Limits.Cone ((F.mapCone c).toStructuredArrow.comp (.comp ))

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.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cone.toCostructuredArrow_obj {J : Type u₁} [] {C : Type u₃} [] (F : ) (c : ) :
@[simp]
theorem CategoryTheory.Limits.Cone.toCostructuredArrow_map {J : Type u₁} [] {C : Type u₃} [] (F : ) :
∀ {X Y : } (f : X Y),
def CategoryTheory.Limits.Cone.toCostructuredArrow {J : Type u₁} [] {C : Type u₃} [] (F : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cone.fromCostructuredArrow_map_hom {J : Type u₁} [] {C : Type u₃} [] (F : ) :
∀ {X Y : } (f : X Y), ().hom = f.left
@[simp]
theorem CategoryTheory.Limits.Cone.fromCostructuredArrow_obj_π {J : Type u₁} [] {C : Type u₃} [] (F : ) :
() = c.hom
@[simp]
theorem CategoryTheory.Limits.Cone.fromCostructuredArrow_obj_pt {J : Type u₁} [] {C : Type u₃} [] (F : ) :
().pt = c.left
def CategoryTheory.Limits.Cone.fromCostructuredArrow {J : Type u₁} [] {C : Type u₃} [] (F : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_unitIso_inv_app_hom {J : Type u₁} [] {C : Type u₃} [] (F : ) (X : ) :
(.inv.app X).hom =
@[simp]
theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_functor_obj_right_as {J : Type u₁} [] {C : Type u₃} [] (F : ) (c : ) :
(.obj c).right.as = PUnit.unit
@[simp]
theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_counitIso_hom_app_right {J : Type u₁} [] {C : Type u₃} [] (F : ) :
(.counitIso.hom.app X).right =
@[simp]
theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_functor_map_left {J : Type u₁} [] {C : Type u₃} [] (F : ) :
∀ {X Y : } (f : X Y), (.map f).left = f.hom
@[simp]
theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_functor_map_right {J : Type u₁} [] {C : Type u₃} [] (F : ) :
∀ {X Y : } (f : X Y), (.map f).right =
@[simp]
theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_inverse_obj_pt {J : Type u₁} [] {C : Type u₃} [] (F : ) :
(.obj c).pt = c.left
@[simp]
theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_counitIso_hom_app_left {J : Type u₁} [] {C : Type u₃} [] (F : ) :
(.counitIso.hom.app X).left =
@[simp]
theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_inverse_obj_π {J : Type u₁} [] {C : Type u₃} [] (F : ) :
(.obj c) = c.hom
@[simp]
theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_functor_obj_left {J : Type u₁} [] {C : Type u₃} [] (F : ) (c : ) :
(.obj c).left = c.pt
@[simp]
theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_counitIso_inv_app_left {J : Type u₁} [] {C : Type u₃} [] (F : ) :
(.counitIso.inv.app X).left =
@[simp]
theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_functor_obj_hom {J : Type u₁} [] {C : Type u₃} [] (F : ) (c : ) :
(.obj c).hom = c
@[simp]
theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_inverse_map_hom {J : Type u₁} [] {C : Type u₃} [] (F : ) :
∀ {X Y : } (f : X Y), (.map f).hom = f.left
@[simp]
theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_counitIso_inv_app_right {J : Type u₁} [] {C : Type u₃} [] (F : ) :
(.counitIso.inv.app X).right =
@[simp]
theorem CategoryTheory.Limits.Cone.equivCostructuredArrow_unitIso_hom_app_hom {J : Type u₁} [] {C : Type u₃} [] (F : ) (X : ) :
(.hom.app X).hom =
def CategoryTheory.Limits.Cone.equivCostructuredArrow {J : Type u₁} [] {C : Type u₃} [] (F : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.Cone.isLimitEquivIsTerminal {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :

A cone is a limit cone iff it is terminal.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.hasLimit_iff_hasTerminal_cone {J : Type u₁} [] {C : Type u₃} [] (F : ) :
theorem CategoryTheory.Limits.hasLimitsOfShape_iff_isLeftAdjoint_const {J : Type u₁} [] {C : Type u₃} [] :
theorem CategoryTheory.Limits.IsLimit.liftConeMorphism_eq_isTerminal_from {J : Type u₁} [] {C : Type u₃} [] {F : } {c : } (hc : ) (s : ) :
hc.liftConeMorphism s = (c.isLimitEquivIsTerminal hc).from s
theorem CategoryTheory.Limits.IsTerminal.from_eq_liftConeMorphism {J : Type u₁} [] {C : Type u₃} [] {F : } {c : } (hc : ) (s : ) :
hc.from s = (c.isLimitEquivIsTerminal.symm hc).liftConeMorphism s
def CategoryTheory.Limits.IsLimit.ofPreservesConeTerminal {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {F' : } {c : } (hc : ) :

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

Equations
Instances For
def CategoryTheory.Limits.IsLimit.ofReflectsConeTerminal {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {F' : } {c : } (hc : CategoryTheory.Limits.IsLimit (G.obj c)) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocone.toCostructuredArrow_map {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
∀ {X Y : J} (f : X Y), c.toCostructuredArrow.map f =
@[simp]
theorem CategoryTheory.Limits.Cocone.toCostructuredArrow_obj {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) (j : J) :
c.toCostructuredArrow.obj j = CategoryTheory.CostructuredArrow.mk (c.app j)
def CategoryTheory.Limits.Cocone.toCostructuredArrow {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.colimit.toCostructuredArrow_obj {J : Type u₁} [] {C : Type u₃} [] (F : ) (j : J) :
@[simp]
theorem CategoryTheory.Limits.colimit.toCostructuredArrow_map {J : Type u₁} [] {C : Type u₃} [] (F : ) :
∀ {X Y : J} (f : X Y),
noncomputable def CategoryTheory.Limits.colimit.toCostructuredArrow {J : Type u₁} [] {C : Type u₃} [] (F : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.Cocone.toCostructuredArrowIsoToCostructuredArrow {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.toCostructuredArrow .toCostructuredArrow F c.pt c.app

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

Equations
Instances For
def CategoryTheory.Functor.toCostructuredArrowIsoToCostructuredArrow {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] (G : ) (F : ) (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) :
G.toCostructuredArrow F X f { pt := X, ι := { app := f, naturality := } }.toCostructuredArrow.comp (CategoryTheory.CostructuredArrow.pre G F { pt := X, ι := { app := f, naturality := } }.pt)

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocone.toCostructuredArrowCompProj_inv_app {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) (X : J) :
c.toCostructuredArrowCompProj.inv.app X =
@[simp]
theorem CategoryTheory.Limits.Cocone.toCostructuredArrowCompProj_hom_app {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) (X : J) :
c.toCostructuredArrowCompProj.hom.app X =
def CategoryTheory.Limits.Cocone.toCostructuredArrowCompProj {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.toCostructuredArrow.comp

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocone.toCostructuredArrow_comp_proj {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.toCostructuredArrow.comp =
@[simp]
theorem CategoryTheory.Limits.Cocone.toCostructuredArrowCompToOverCompForget_hom_app {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) (X : J) :
c.toCostructuredArrowCompToOverCompForget.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
@[simp]
theorem CategoryTheory.Limits.Cocone.toCostructuredArrowCompToOverCompForget_inv_app {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) (X : J) :
c.toCostructuredArrowCompToOverCompForget.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
def CategoryTheory.Limits.Cocone.toCostructuredArrowCompToOverCompForget {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.toCostructuredArrow.comp (.comp ()) 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.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocone.toCostructuredArrow_comp_toOver_comp_forget {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.toCostructuredArrow.comp (.comp ()) = F
@[simp]
theorem CategoryTheory.Limits.Cocone.toOver_pt {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.toOver.pt =
@[simp]
theorem CategoryTheory.Limits.Cocone.toOver_ι_app {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) (j : J) :
c.toOver.app j = CategoryTheory.Over.homMk (c.app j)
def CategoryTheory.Limits.Cocone.toOver {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
CategoryTheory.Limits.Cocone (c.toCostructuredArrow.comp )

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.colimit.toOver_pt {J : Type u₁} [] {C : Type u₃} [] (F : ) :
@[simp]
theorem CategoryTheory.Limits.colimit.toOver_ι_app {J : Type u₁} [] {C : Type u₃} [] (F : ) (j : J) :
noncomputable def CategoryTheory.Limits.colimit.toOver {J : Type u₁} [] {C : Type u₃} [] (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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocone.mapCoconeToOver_hom_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.mapCoconeToOver.hom.hom =
@[simp]
theorem CategoryTheory.Limits.Cocone.mapCoconeToOver_inv_hom {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
c.mapCoconeToOver.inv.hom =
def CategoryTheory.Limits.Cocone.mapCoconeToOver {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :
().mapCocone c.toOver c

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocone.fromCostructuredArrow_pt {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) {X : D} (G : ) :
@[simp]
theorem CategoryTheory.Limits.Cocone.fromCostructuredArrow_ι_app {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) {X : D} (G : ) (j : J) :
j = (G.obj j).hom
def CategoryTheory.Limits.Cocone.fromCostructuredArrow {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] (F : ) {X : D} (G : ) :
CategoryTheory.Limits.Cocone (G.comp (.comp F))

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

Equations
• = { pt := X, ι := { app := fun (j : J) => (G.obj j).hom, naturality := } }
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocone.toCostructuredArrowCocone_ι_app {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {K : } (c : ) (F : ) {X : D} (f : F.obj c.pt X) (j : J) :
(c.toCostructuredArrowCocone F f).app j = CategoryTheory.CostructuredArrow.homMk (c.app j)
@[simp]
theorem CategoryTheory.Limits.Cocone.toCostructuredArrowCocone_pt {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {K : } (c : ) (F : ) {X : D} (f : F.obj c.pt X) :
(c.toCostructuredArrowCocone F f).pt =
def CategoryTheory.Limits.Cocone.toCostructuredArrowCocone {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {K : } (c : ) (F : ) {X : D} (f : F.obj c.pt X) :
CategoryTheory.Limits.Cocone ((F.mapCocone c).toCostructuredArrow.comp ())

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.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocone.toStructuredArrow_map {J : Type u₁} [] {C : Type u₃} [] (F : ) :
∀ {X Y : } (f : X Y),
@[simp]
theorem CategoryTheory.Limits.Cocone.toStructuredArrow_obj {J : Type u₁} [] {C : Type u₃} [] (F : ) (c : ) :
def CategoryTheory.Limits.Cocone.toStructuredArrow {J : Type u₁} [] {C : Type u₃} [] (F : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocone.fromStructuredArrow_obj_pt {J : Type u₁} [] {C : Type u₃} [] (F : ) :
().pt = c.right
@[simp]
theorem CategoryTheory.Limits.Cocone.fromStructuredArrow_map_hom {J : Type u₁} [] {C : Type u₃} [] (F : ) :
∀ {X Y : } (f : X Y), ().hom = f.right
@[simp]
theorem CategoryTheory.Limits.Cocone.fromStructuredArrow_obj_ι {J : Type u₁} [] {C : Type u₃} [] (F : ) :
() = c.hom
def CategoryTheory.Limits.Cocone.fromStructuredArrow {J : Type u₁} [] {C : Type u₃} [] (F : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_counitIso_hom_app_left {J : Type u₁} [] {C : Type u₃} [] (F : ) :
(.counitIso.hom.app X).left =
@[simp]
theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_functor_obj_right {J : Type u₁} [] {C : Type u₃} [] (F : ) (c : ) :
(.obj c).right = c.pt
@[simp]
theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_unitIso_inv_app_hom {J : Type u₁} [] {C : Type u₃} [] (F : ) (X : ) :
(.inv.app X).hom =
@[simp]
theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_functor_map_right {J : Type u₁} [] {C : Type u₃} [] (F : ) :
∀ {X Y : } (f : X Y), (.map f).right = f.hom
@[simp]
theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_counitIso_inv_app_right {J : Type u₁} [] {C : Type u₃} [] (F : ) :
(.counitIso.inv.app X).right =
@[simp]
theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_inverse_obj_ι {J : Type u₁} [] {C : Type u₃} [] (F : ) :
(.obj c) = c.hom
@[simp]
theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_unitIso_hom_app_hom {J : Type u₁} [] {C : Type u₃} [] (F : ) (X : ) :
(.hom.app X).hom =
@[simp]
theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_inverse_map_hom {J : Type u₁} [] {C : Type u₃} [] (F : ) :
∀ {X Y : } (f : X Y), (.map f).hom = f.right
@[simp]
theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_functor_obj_hom {J : Type u₁} [] {C : Type u₃} [] (F : ) (c : ) :
(.obj c).hom = c
@[simp]
theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_counitIso_hom_app_right {J : Type u₁} [] {C : Type u₃} [] (F : ) :
(.counitIso.hom.app X).right =
@[simp]
theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_counitIso_inv_app_left {J : Type u₁} [] {C : Type u₃} [] (F : ) :
(.counitIso.inv.app X).left =
@[simp]
theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_inverse_obj_pt {J : Type u₁} [] {C : Type u₃} [] (F : ) :
(.obj c).pt = c.right
@[simp]
theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_functor_obj_left_as {J : Type u₁} [] {C : Type u₃} [] (F : ) (c : ) :
(.obj c).left.as = PUnit.unit
@[simp]
theorem CategoryTheory.Limits.Cocone.equivStructuredArrow_functor_map_left {J : Type u₁} [] {C : Type u₃} [] (F : ) :
∀ {X Y : } (f : X Y), (.map f).left =
def CategoryTheory.Limits.Cocone.equivStructuredArrow {J : Type u₁} [] {C : Type u₃} [] (F : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.Cocone.isColimitEquivIsInitial {J : Type u₁} [] {C : Type u₃} [] {F : } (c : ) :

A cocone is a colimit cocone iff it is initial.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.hasColimit_iff_hasInitial_cocone {J : Type u₁} [] {C : Type u₃} [] (F : ) :
theorem CategoryTheory.Limits.hasColimitsOfShape_iff_isRightAdjoint_const {J : Type u₁} [] {C : Type u₃} [] :
theorem CategoryTheory.Limits.IsColimit.descCoconeMorphism_eq_isInitial_to {J : Type u₁} [] {C : Type u₃} [] {F : } {c : } (hc : ) (s : ) :
hc.descCoconeMorphism s = (c.isColimitEquivIsInitial hc).to s
theorem CategoryTheory.Limits.IsInitial.to_eq_descCoconeMorphism {J : Type u₁} [] {C : Type u₃} [] {F : } {c : } (hc : ) (s : ) :
hc.to s = (c.isColimitEquivIsInitial.symm hc).descCoconeMorphism s
def CategoryTheory.Limits.IsColimit.ofPreservesCoconeInitial {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {F' : } {c : } (hc : ) :

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

Equations
Instances For
def CategoryTheory.Limits.IsColimit.ofReflectsCoconeInitial {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {D : Type u₄} [] {F : } {F' : } {c : } (hc : CategoryTheory.Limits.IsColimit (G.obj c)) :

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

Equations
Instances For