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.

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 -.

Equations

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

@[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✝) : c.toStructuredArrow.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) : c.toStructuredArrow.obj j = CategoryTheory.StructuredArrow.mk (c.π.app j)

noncomputable def CategoryTheory.Limits.limit.toStructuredArrow {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.Functor J (CategoryTheory.StructuredArrow (CategoryTheory.Limits.limit F) 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.

@[simp]

theorem CategoryTheory.Limits.limit.toStructuredArrow_map {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] {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.limit.toStructuredArrow F).map f = CategoryTheory.StructuredArrow.homMk f ⋯

@[simp]

theorem CategoryTheory.Limits.limit.toStructuredArrow_obj {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] (j : J) : (CategoryTheory.Limits.limit.toStructuredArrow F).obj j = CategoryTheory.StructuredArrow.mk (CategoryTheory.Limits.limit.π F j)

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) : c.toStructuredArrow ≅ (CategoryTheory.Functor.id J).toStructuredArrow c.pt F c.π.app ⋯

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

Equations

• c.toStructuredArrowIsoToStructuredArrow = CategoryTheory.Iso.refl c.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) : 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

• G.toStructuredArrowIsoToStructuredArrow X F f h = CategoryTheory.Iso.refl (G.toStructuredArrow X F f ⋯)

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) : c.toStructuredArrow.comp (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.

Equations

• c.toStructuredArrowCompProj = CategoryTheory.Iso.refl (c.toStructuredArrow.comp (CategoryTheory.StructuredArrow.proj c.pt F))

@[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) : c.toStructuredArrowCompProj.inv.app X = CategoryTheory.CategoryStruct.id X

@[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) : c.toStructuredArrowCompProj.hom.app X = CategoryTheory.CategoryStruct.id X

@[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) : c.toStructuredArrow.comp (CategoryTheory.StructuredArrow.proj c.pt F) = CategoryTheory.Functor.id J

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) : c.toStructuredArrow.comp ((CategoryTheory.StructuredArrow.toUnder c.pt F).comp (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.

Equations

• c.toStructuredArrowCompToUnderCompForget = CategoryTheory.Iso.refl (c.toStructuredArrow.comp ((CategoryTheory.StructuredArrow.toUnder c.pt F).comp (CategoryTheory.Under.forget c.pt)))

@[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) : c.toStructuredArrowCompToUnderCompForget.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) : c.toStructuredArrowCompToUnderCompForget.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)

@[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) : c.toStructuredArrow.comp ((CategoryTheory.StructuredArrow.toUnder c.pt F).comp (CategoryTheory.Under.forget c.pt)) = F

def CategoryTheory.Limits.Cone.toUnder {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 (c.toStructuredArrow.comp (CategoryTheory.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.

Equations

• c.toUnder = { pt := CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.id c.pt), π := { app := fun (j : J) => CategoryTheory.Under.homMk (c.π.app j) ⋯, naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Limits.Cone.toUnder_pt {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) : c.toUnder.pt = CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.id c.pt)

@[simp]

theorem CategoryTheory.Limits.Cone.toUnder_π_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) (j : J) : c.toUnder.π.app j = CategoryTheory.Under.homMk (c.π.app j) ⋯

noncomputable def CategoryTheory.Limits.limit.toUnder {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.Cone ((CategoryTheory.Limits.limit.toStructuredArrow F).comp (CategoryTheory.StructuredArrow.toUnder (CategoryTheory.Limits.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.

Equations

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

def CategoryTheory.Limits.Cone.mapConeToUnder {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.Under.forget c.pt).mapCone c.toUnder ≅ c

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

Equations

• c.mapConeToUnder = CategoryTheory.Iso.refl ((CategoryTheory.Under.forget c.pt).mapCone c.toUnder)

@[simp]

theorem CategoryTheory.Limits.Cone.mapConeToUnder_inv_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) : c.mapConeToUnder.inv.hom = CategoryTheory.CategoryStruct.id c.pt

@[simp]

theorem CategoryTheory.Limits.Cone.mapConeToUnder_hom_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) : c.mapConeToUnder.hom.hom = CategoryTheory.CategoryStruct.id c.pt

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 (G.comp ((CategoryTheory.StructuredArrow.proj X F).comp F))

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

Equations

• CategoryTheory.Limits.Cone.fromStructuredArrow F G = { pt := X, π := { app := fun (j : J) => (G.obj j).hom, naturality := ⋯ } }

@[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

@[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

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 ((F.mapCone c).toStructuredArrow.comp ((CategoryTheory.StructuredArrow.map f).comp (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.

Equations

• c.toStructuredArrowCone F f = { pt := CategoryTheory.StructuredArrow.mk f, π := { app := fun (j : J) => CategoryTheory.StructuredArrow.homMk (c.π.app j) ⋯, naturality := ⋯ } }

@[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) : (c.toStructuredArrowCone F f).π.app j = CategoryTheory.StructuredArrow.homMk (c.π.app j) ⋯

@[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) : (c.toStructuredArrowCone F f).pt = CategoryTheory.StructuredArrow.mk f

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.

Equations

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

@[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 ⋯

@[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.π

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.

Equations

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

@[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_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_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.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.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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.

Equations

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

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 ↔ (CategoryTheory.Functor.const J).IsLeftAdjoint

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) : hc.liftConeMorphism s = (c.isLimitEquivIsTerminal hc).from 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) : hc.from s = (c.isLimitEquivIsTerminal.symm hc).liftConeMorphism s

noncomputable 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.

Equations

• CategoryTheory.Limits.IsLimit.ofPreservesConeTerminal G hc = (G.obj c).isLimitEquivIsTerminal.symm (CategoryTheory.Limits.IsTerminal.isTerminalObj G c (c.isLimitEquivIsTerminal hc))

noncomputable 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.

Equations

• CategoryTheory.Limits.IsLimit.ofReflectsConeTerminal G hc = c.isLimitEquivIsTerminal.symm (CategoryTheory.Limits.IsTerminal.isTerminalOfObj G c ((G.obj c).isLimitEquivIsTerminal hc))

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.

Equations

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

@[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✝) : c.toCostructuredArrow.map f = CategoryTheory.CostructuredArrow.homMk f ⋯

@[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) : c.toCostructuredArrow.obj j = CategoryTheory.CostructuredArrow.mk (c.ι.app j)

noncomputable def CategoryTheory.Limits.colimit.toCostructuredArrow {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.Functor J (CategoryTheory.CostructuredArrow F (CategoryTheory.Limits.colimit 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.

@[simp]

theorem CategoryTheory.Limits.colimit.toCostructuredArrow_obj {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] (j : J) : (CategoryTheory.Limits.colimit.toCostructuredArrow F).obj j = CategoryTheory.CostructuredArrow.mk (CategoryTheory.Limits.colimit.ι F j)

@[simp]

theorem CategoryTheory.Limits.colimit.toCostructuredArrow_map {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] {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.colimit.toCostructuredArrow F).map f = CategoryTheory.CostructuredArrow.homMk f ⋯

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) : c.toCostructuredArrow ≅ (CategoryTheory.Functor.id J).toCostructuredArrow F c.pt c.ι.app ⋯

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

Equations

• c.toCostructuredArrowIsoToCostructuredArrow = CategoryTheory.Iso.refl c.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) : 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

• G.toCostructuredArrowIsoToCostructuredArrow F X f h = CategoryTheory.Iso.refl (G.toCostructuredArrow F X f ⋯)

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) : c.toCostructuredArrow.comp (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.

Equations

• c.toCostructuredArrowCompProj = CategoryTheory.Iso.refl (c.toCostructuredArrow.comp (CategoryTheory.CostructuredArrow.proj F c.pt))

@[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) : c.toCostructuredArrowCompProj.hom.app X = CategoryTheory.CategoryStruct.id X

@[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) : c.toCostructuredArrowCompProj.inv.app X = CategoryTheory.CategoryStruct.id X

@[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) : c.toCostructuredArrow.comp (CategoryTheory.CostructuredArrow.proj F c.pt) = CategoryTheory.Functor.id J

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) : c.toCostructuredArrow.comp ((CategoryTheory.CostructuredArrow.toOver F c.pt).comp (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.

Equations

• c.toCostructuredArrowCompToOverCompForget = CategoryTheory.Iso.refl (c.toCostructuredArrow.comp ((CategoryTheory.CostructuredArrow.toOver F c.pt).comp (CategoryTheory.Over.forget c.pt)))

@[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) : c.toCostructuredArrowCompToOverCompForget.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) : c.toCostructuredArrowCompToOverCompForget.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)

@[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) : c.toCostructuredArrow.comp ((CategoryTheory.CostructuredArrow.toOver F c.pt).comp (CategoryTheory.Over.forget c.pt)) = F

def CategoryTheory.Limits.Cocone.toOver {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 (c.toCostructuredArrow.comp (CategoryTheory.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.

Equations

• c.toOver = { pt := CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id c.pt), ι := { app := fun (j : J) => CategoryTheory.Over.homMk (c.ι.app j) ⋯, naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Limits.Cocone.toOver_ι_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) (j : J) : c.toOver.ι.app j = CategoryTheory.Over.homMk (c.ι.app j) ⋯

@[simp]

theorem CategoryTheory.Limits.Cocone.toOver_pt {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) : c.toOver.pt = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id c.pt)

noncomputable def CategoryTheory.Limits.colimit.toOver {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.Cocone ((CategoryTheory.Limits.colimit.toCostructuredArrow F).comp (CategoryTheory.CostructuredArrow.toOver F (CategoryTheory.Limits.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.

Equations

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

@[simp]

theorem CategoryTheory.Limits.colimit.toOver_ι_app {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] (j : J) : (CategoryTheory.Limits.colimit.toOver F).ι.app j = CategoryTheory.Over.homMk (CategoryTheory.Limits.colimit.ι F j) ⋯

@[simp]

theorem CategoryTheory.Limits.colimit.toOver_pt {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.colimit.toOver F).pt = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit F))

def CategoryTheory.Limits.Cocone.mapCoconeToOver {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.Over.forget c.pt).mapCocone c.toOver ≅ c

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

Equations

• c.mapCoconeToOver = CategoryTheory.Iso.refl ((CategoryTheory.Over.forget c.pt).mapCocone c.toOver)

@[simp]

theorem CategoryTheory.Limits.Cocone.mapCoconeToOver_inv_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) : c.mapCoconeToOver.inv.hom = CategoryTheory.CategoryStruct.id c.pt

@[simp]

theorem CategoryTheory.Limits.Cocone.mapCoconeToOver_hom_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) : c.mapCoconeToOver.hom.hom = CategoryTheory.CategoryStruct.id c.pt

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 (G.comp ((CategoryTheory.CostructuredArrow.proj F X).comp F))

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

Equations

• CategoryTheory.Limits.Cocone.fromCostructuredArrow F G = { pt := X, ι := { app := fun (j : J) => (G.obj j).hom, naturality := ⋯ } }

@[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

@[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

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 ((F.mapCocone c).toCostructuredArrow.comp ((CategoryTheory.CostructuredArrow.map f).comp (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.

Equations

• c.toCostructuredArrowCocone F f = { pt := CategoryTheory.CostructuredArrow.mk f, ι := { app := fun (j : J) => CategoryTheory.CostructuredArrow.homMk (c.ι.app j) ⋯, naturality := ⋯ } }

@[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) : (c.toCostructuredArrowCocone 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) : (c.toCostructuredArrowCocone F f).ι.app j = CategoryTheory.CostructuredArrow.homMk (c.ι.app j) ⋯

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.

Equations

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

@[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.ι

@[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 ⋯

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.

Equations

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

@[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

@[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_ι {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

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.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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.

Equations

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

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 ↔ (CategoryTheory.Functor.const J).IsRightAdjoint

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) : hc.descCoconeMorphism s = (c.isColimitEquivIsInitial hc).to 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) : hc.to s = (c.isColimitEquivIsInitial.symm hc).descCoconeMorphism s

noncomputable 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.

Equations

• CategoryTheory.Limits.IsColimit.ofPreservesCoconeInitial G hc = (G.obj c).isColimitEquivIsInitial.symm (CategoryTheory.Limits.IsInitial.isInitialObj G c (c.isColimitEquivIsInitial hc))

noncomputable 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.

Equations

• CategoryTheory.Limits.IsColimit.ofReflectsCoconeInitial G hc = c.isColimitEquivIsInitial.symm (CategoryTheory.Limits.IsInitial.isInitialOfObj G c ((G.obj c).isColimitEquivIsInitial hc))