(Co)limits in functor categories.

We show that if D has limits, then the functor category C ⥤ D also has limits (CategoryTheory.Limits.functorCategoryHasLimits), and the evaluation functors preserve limits (CategoryTheory.Limits.evaluation_preservesLimits) (and similarly for colimits).

We also show that F : D ⥤ K ⥤ C preserves (co)limits if it does so for each k : K (CategoryTheory.Limits.preservesLimits_of_evaluation and CategoryTheory.Limits.preservesColimits_of_evaluation).

@[simp]

theorem CategoryTheory.Limits.limit.lift_π_app {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (H : Functor J (Functor K C)) [HasLimit H] (c : Cone H) (j : J) (k : K) : CategoryStruct.comp ((lift H c).app k) ((π H j).app k) = (c.π.app j).app k

@[simp]

theorem CategoryTheory.Limits.limit.lift_π_app_assoc {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (H : Functor J (Functor K C)) [HasLimit H] (c : Cone H) (j : J) (k : K) {Z : C} (h : (H.obj j).obj k ⟶ Z) : CategoryStruct.comp ((lift H c).app k) (CategoryStruct.comp ((π H j).app k) h) = CategoryStruct.comp ((c.π.app j).app k) h

@[simp]

theorem CategoryTheory.Limits.colimit.ι_desc_app {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (H : Functor J (Functor K C)) [HasColimit H] (c : Cocone H) (j : J) (k : K) : CategoryStruct.comp ((ι H j).app k) ((desc H c).app k) = (c.ι.app j).app k

@[simp]

theorem CategoryTheory.Limits.colimit.ι_desc_app_assoc {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (H : Functor J (Functor K C)) [HasColimit H] (c : Cocone H) (j : J) (k : K) {Z : C} (h : c.pt.obj k ⟶ Z) : CategoryStruct.comp ((ι H j).app k) (CategoryStruct.comp ((desc H c).app k) h) = CategoryStruct.comp ((c.ι.app j).app k) h

def CategoryTheory.Limits.evaluationJointlyReflectsLimits {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {F : Functor J (Functor K C)} (c : Cone F) (t : (k : K) → IsLimit (((evaluation K C).obj k).mapCone c)) : IsLimit c

The evaluation functors jointly reflect limits: that is, to show a cone is a limit of F it suffices to show that each evaluation cone is a limit. In other words, to prove a cone is limiting you can show it's pointwise limiting.

Equations

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

def CategoryTheory.Limits.combineCones {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (c : (k : K) → LimitCone (F.flip.obj k)) : Cone F

Given a functor F and a collection of limit cones for each diagram X ↦ F X k, we can stitch them together to give a cone for the diagram F. combinedIsLimit shows that the new cone is limiting, and evalCombined shows it is (essentially) made up of the original cones.

Equations

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

@[simp]

theorem CategoryTheory.Limits.combineCones_pt_obj {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (c : (k : K) → LimitCone (F.flip.obj k)) (k : K) : (combineCones F c).pt.obj k = (c k).cone.pt

@[simp]

theorem CategoryTheory.Limits.combineCones_pt_map {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (c : (k : K) → LimitCone (F.flip.obj k)) {k₁ k₂ : K} (f : k₁ ⟶ k₂) : (combineCones F c).pt.map f = (c k₂).isLimit.lift { pt := (c k₁).cone.pt, π := CategoryStruct.comp (c k₁).cone.π (F.flip.map f) }

@[simp]

theorem CategoryTheory.Limits.combineCones_π_app_app {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (c : (k : K) → LimitCone (F.flip.obj k)) (j : J) (k : K) : ((combineCones F c).π.app j).app k = (c k).cone.π.app j

def CategoryTheory.Limits.evaluateCombinedCones {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (c : (k : K) → LimitCone (F.flip.obj k)) (k : K) : ((evaluation K C).obj k).mapCone (combineCones F c) ≅ (c k).cone

The stitched together cones each project down to the original given cones (up to iso).

Equations

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

def CategoryTheory.Limits.combinedIsLimit {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (c : (k : K) → LimitCone (F.flip.obj k)) : IsLimit (combineCones F c)

Stitching together limiting cones gives a limiting cone.

Equations

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

def CategoryTheory.Limits.evaluationJointlyReflectsColimits {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {F : Functor J (Functor K C)} (c : Cocone F) (t : (k : K) → IsColimit (((evaluation K C).obj k).mapCocone c)) : IsColimit c

The evaluation functors jointly reflect colimits: that is, to show a cocone is a colimit of F it suffices to show that each evaluation cocone is a colimit. In other words, to prove a cocone is colimiting you can show it's pointwise colimiting.

Equations

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

def CategoryTheory.Limits.combineCocones {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (c : (k : K) → ColimitCocone (F.flip.obj k)) : Cocone F

Given a functor F and a collection of colimit cocones for each diagram X ↦ F X k, we can stitch them together to give a cocone for the diagram F. combinedIsColimit shows that the new cocone is colimiting, and evalCombined shows it is (essentially) made up of the original cocones.

Equations

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

@[simp]

theorem CategoryTheory.Limits.combineCocones_pt_map {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (c : (k : K) → ColimitCocone (F.flip.obj k)) {k₁ k₂ : K} (f : k₁ ⟶ k₂) : (combineCocones F c).pt.map f = (c k₁).isColimit.desc { pt := (c k₂).cocone.pt, ι := CategoryStruct.comp (F.flip.map f) (c k₂).cocone.ι }

@[simp]

theorem CategoryTheory.Limits.combineCocones_pt_obj {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (c : (k : K) → ColimitCocone (F.flip.obj k)) (k : K) : (combineCocones F c).pt.obj k = (c k).cocone.pt

@[simp]

theorem CategoryTheory.Limits.combineCocones_ι_app_app {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (c : (k : K) → ColimitCocone (F.flip.obj k)) (j : J) (k : K) : ((combineCocones F c).ι.app j).app k = (c k).cocone.ι.app j

def CategoryTheory.Limits.evaluateCombinedCocones {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (c : (k : K) → ColimitCocone (F.flip.obj k)) (k : K) : ((evaluation K C).obj k).mapCocone (combineCocones F c) ≅ (c k).cocone

The stitched together cocones each project down to the original given cocones (up to iso).

Equations

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

def CategoryTheory.Limits.combinedIsColimit {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (c : (k : K) → ColimitCocone (F.flip.obj k)) : IsColimit (combineCocones F c)

Stitching together colimiting cocones gives a colimiting cocone.

Equations

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

noncomputable def CategoryTheory.Limits.pointwiseCocone {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor J (Functor K C)) : Cocone F

An alternative colimit cocone in the functor category K ⥤ C in the case where C has J-shaped colimits, with cocone point F.flip ⋙ colim.

Equations

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

@[simp]

theorem CategoryTheory.Limits.pointwiseCocone_pt {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor J (Functor K C)) : (pointwiseCocone F).pt = F.flip.comp colim

@[simp]

theorem CategoryTheory.Limits.pointwiseCocone_ι_app_app {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor J (Functor K C)) (X : J) (Y : K) : ((pointwiseCocone F).ι.app X).app Y = colimit.ι (F.flip.obj Y) X

noncomputable def CategoryTheory.Limits.pointwiseIsColimit {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor J (Functor K C)) : IsColimit (pointwiseCocone F)

pointwiseCocone is indeed a colimit cocone.

Equations

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

instance CategoryTheory.Limits.functorCategoryHasLimit {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) [∀ (k : K), HasLimit (F.flip.obj k)] : HasLimit F

instance CategoryTheory.Limits.functorCategoryHasLimitsOfShape {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] : HasLimitsOfShape J (Functor K C)

instance CategoryTheory.Limits.functorCategoryHasColimit {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) [∀ (k : K), HasColimit (F.flip.obj k)] : HasColimit F

instance CategoryTheory.Limits.functorCategoryHasColimitsOfShape {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] : HasColimitsOfShape J (Functor K C)

instance CategoryTheory.Limits.functorCategoryHasLimitsOfSize {C : Type u} [Category.{v, u} C] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfSize.{v₁, u₁, v, u} C] : HasLimitsOfSize.{v₁, u₁, max u₂ v, max (max (max u u₂) v) v₂} (Functor K C)

instance CategoryTheory.Limits.functorCategoryHasColimitsOfSize {C : Type u} [Category.{v, u} C] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfSize.{v₁, u₁, v, u} C] : HasColimitsOfSize.{v₁, u₁, max u₂ v, max (max (max u u₂) v) v₂} (Functor K C)

instance CategoryTheory.Limits.hasLimitCompEvaluation {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (k : K) [HasLimit (F.flip.obj k)] : HasLimit (F.comp ((evaluation K C).obj k))

instance CategoryTheory.Limits.evaluation_preservesLimit {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) [∀ (k : K), HasLimit (F.flip.obj k)] (k : K) : PreservesLimit F ((evaluation K C).obj k)

instance CategoryTheory.Limits.evaluation_preservesLimitsOfShape {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] (k : K) : PreservesLimitsOfShape J ((evaluation K C).obj k)

def CategoryTheory.Limits.limitObjIsoLimitCompEvaluation {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] (F : Functor J (Functor K C)) (k : K) : (limit F).obj k ≅ limit (F.comp ((evaluation K C).obj k))

If F : J ⥤ K ⥤ C is a functor into a functor category which has a limit, then the evaluation of that limit at k is the limit of the evaluations of F.obj j at k.

Equations

• CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F k = CategoryTheory.preservesLimitIso ((CategoryTheory.evaluation K C).obj k) F

@[simp]

theorem CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_hom_π {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] (F : Functor J (Functor K C)) (j : J) (k : K) : CategoryStruct.comp (limitObjIsoLimitCompEvaluation F k).hom (limit.π (F.comp ((evaluation K C).obj k)) j) = (limit.π F j).app k

@[simp]

theorem CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_hom_π_assoc {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] (F : Functor J (Functor K C)) (j : J) (k : K) {Z : C} (h : ((evaluation K C).obj k).obj (F.obj j) ⟶ Z) : CategoryStruct.comp (limitObjIsoLimitCompEvaluation F k).hom (CategoryStruct.comp (limit.π (F.comp ((evaluation K C).obj k)) j) h) = CategoryStruct.comp ((limit.π F j).app k) h

@[simp]

theorem CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_inv_π_app {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] (F : Functor J (Functor K C)) (j : J) (k : K) : CategoryStruct.comp (limitObjIsoLimitCompEvaluation F k).inv ((limit.π F j).app k) = limit.π (F.comp ((evaluation K C).obj k)) j

@[simp]

theorem CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_inv_π_app_assoc {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] (F : Functor J (Functor K C)) (j : J) (k : K) {Z : C} (h : (F.obj j).obj k ⟶ Z) : CategoryStruct.comp (limitObjIsoLimitCompEvaluation F k).inv (CategoryStruct.comp ((limit.π F j).app k) h) = CategoryStruct.comp (limit.π (F.comp ((evaluation K C).obj k)) j) h

@[simp]

theorem CategoryTheory.Limits.limit_map_limitObjIsoLimitCompEvaluation_hom {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] {i j : K} (F : Functor J (Functor K C)) (f : i ⟶ j) : CategoryStruct.comp ((limit F).map f) (limitObjIsoLimitCompEvaluation F j).hom = CategoryStruct.comp (limitObjIsoLimitCompEvaluation F i).hom (limMap (whiskerLeft F ((evaluation K C).map f)))

@[simp]

theorem CategoryTheory.Limits.limit_map_limitObjIsoLimitCompEvaluation_hom_assoc {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] {i j : K} (F : Functor J (Functor K C)) (f : i ⟶ j) {Z : C} (h : limit (F.comp ((evaluation K C).obj j)) ⟶ Z) : CategoryStruct.comp ((limit F).map f) (CategoryStruct.comp (limitObjIsoLimitCompEvaluation F j).hom h) = CategoryStruct.comp (limitObjIsoLimitCompEvaluation F i).hom (CategoryStruct.comp (limMap (whiskerLeft F ((evaluation K C).map f))) h)

@[simp]

theorem CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_inv_limit_map {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] {i j : K} (F : Functor J (Functor K C)) (f : i ⟶ j) : CategoryStruct.comp (limitObjIsoLimitCompEvaluation F i).inv ((limit F).map f) = CategoryStruct.comp (limMap (whiskerLeft F ((evaluation K C).map f))) (limitObjIsoLimitCompEvaluation F j).inv

@[simp]

theorem CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_inv_limit_map_assoc {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] {i j : K} (F : Functor J (Functor K C)) (f : i ⟶ j) {Z : C} (h : (limit F).obj j ⟶ Z) : CategoryStruct.comp (limitObjIsoLimitCompEvaluation F i).inv (CategoryStruct.comp ((limit F).map f) h) = CategoryStruct.comp (limMap (whiskerLeft F ((evaluation K C).map f))) (CategoryStruct.comp (limitObjIsoLimitCompEvaluation F j).inv h)

theorem CategoryTheory.Limits.limit_obj_ext {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {H : Functor J (Functor K C)} [HasLimitsOfShape J C] {k : K} {W : C} {f g : W ⟶ (limit H).obj k} (w : ∀ (j : J), CategoryStruct.comp f ((limit.π H j).app k) = CategoryStruct.comp g ((limit.π H j).app k)) : f = g

def CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (G : Functor D K) [HasLimitsOfShape J C] : limit (F.comp ((whiskeringLeft D K C).obj G)) ≅ G.comp (limit F)

Taking a limit after whiskering by G is the same as using G and then taking a limit.

Equations

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

@[simp]

theorem CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit_hom_whiskerLeft_π {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (G : Functor D K) [HasLimitsOfShape J C] (j : J) : CategoryStruct.comp (limitCompWhiskeringLeftIsoCompLimit F G).hom (whiskerLeft G (limit.π F j)) = limit.π (F.comp ((whiskeringLeft D K C).obj G)) j

@[simp]

theorem CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit_hom_whiskerLeft_π_assoc {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (G : Functor D K) [HasLimitsOfShape J C] (j : J) {Z : Functor D C} (h : G.comp (F.obj j) ⟶ Z) : CategoryStruct.comp (limitCompWhiskeringLeftIsoCompLimit F G).hom (CategoryStruct.comp (whiskerLeft G (limit.π F j)) h) = CategoryStruct.comp (limit.π (F.comp ((whiskeringLeft D K C).obj G)) j) h

@[simp]

theorem CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit_inv_π {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (G : Functor D K) [HasLimitsOfShape J C] (j : J) : CategoryStruct.comp (limitCompWhiskeringLeftIsoCompLimit F G).inv (limit.π (F.comp ((whiskeringLeft D K C).obj G)) j) = whiskerLeft G (limit.π F j)

@[simp]

theorem CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit_inv_π_assoc {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (G : Functor D K) [HasLimitsOfShape J C] (j : J) {Z : Functor D C} (h : ((whiskeringLeft D K C).obj G).obj (F.obj j) ⟶ Z) : CategoryStruct.comp (limitCompWhiskeringLeftIsoCompLimit F G).inv (CategoryStruct.comp (limit.π (F.comp ((whiskeringLeft D K C).obj G)) j) h) = CategoryStruct.comp (whiskerLeft G (limit.π F j)) h

instance CategoryTheory.Limits.hasColimitCompEvaluation {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (k : K) [HasColimit (F.flip.obj k)] : HasColimit (F.comp ((evaluation K C).obj k))

instance CategoryTheory.Limits.evaluation_preservesColimit {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) [∀ (k : K), HasColimit (F.flip.obj k)] (k : K) : PreservesColimit F ((evaluation K C).obj k)

instance CategoryTheory.Limits.evaluation_preservesColimitsOfShape {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (k : K) : PreservesColimitsOfShape J ((evaluation K C).obj k)

def CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor J (Functor K C)) (k : K) : (colimit F).obj k ≅ colimit (F.comp ((evaluation K C).obj k))

If F : J ⥤ K ⥤ C is a functor into a functor category which has a colimit, then the evaluation of that colimit at k is the colimit of the evaluations of F.obj j at k.

Equations

• CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F k = CategoryTheory.preservesColimitIso ((CategoryTheory.evaluation K C).obj k) F

@[simp]

theorem CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_ι_inv {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor J (Functor K C)) (j : J) (k : K) : CategoryStruct.comp (colimit.ι (F.comp ((evaluation K C).obj k)) j) (colimitObjIsoColimitCompEvaluation F k).inv = (colimit.ι F j).app k

@[simp]

theorem CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_ι_inv_assoc {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor J (Functor K C)) (j : J) (k : K) {Z : C} (h : (colimit F).obj k ⟶ Z) : CategoryStruct.comp (colimit.ι (F.comp ((evaluation K C).obj k)) j) (CategoryStruct.comp (colimitObjIsoColimitCompEvaluation F k).inv h) = CategoryStruct.comp ((colimit.ι F j).app k) h

@[simp]

theorem CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_ι_app_hom {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor J (Functor K C)) (j : J) (k : K) : CategoryStruct.comp ((colimit.ι F j).app k) (colimitObjIsoColimitCompEvaluation F k).hom = colimit.ι (F.comp ((evaluation K C).obj k)) j

@[simp]

theorem CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_ι_app_hom_assoc {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor J (Functor K C)) (j : J) (k : K) {Z : C} (h : colimit (F.comp ((evaluation K C).obj k)) ⟶ Z) : CategoryStruct.comp ((colimit.ι F j).app k) (CategoryStruct.comp (colimitObjIsoColimitCompEvaluation F k).hom h) = CategoryStruct.comp (colimit.ι (F.comp ((evaluation K C).obj k)) j) h

@[simp]

theorem CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_inv_colimit_map {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor J (Functor K C)) {i j : K} (f : i ⟶ j) : CategoryStruct.comp (colimitObjIsoColimitCompEvaluation F i).inv ((colimit F).map f) = CategoryStruct.comp (colimMap (whiskerLeft F ((evaluation K C).map f))) (colimitObjIsoColimitCompEvaluation F j).inv

@[simp]

theorem CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_inv_colimit_map_assoc {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor J (Functor K C)) {i j : K} (f : i ⟶ j) {Z : C} (h : (colimit F).obj j ⟶ Z) : CategoryStruct.comp (colimitObjIsoColimitCompEvaluation F i).inv (CategoryStruct.comp ((colimit F).map f) h) = CategoryStruct.comp (colimMap (whiskerLeft F ((evaluation K C).map f))) (CategoryStruct.comp (colimitObjIsoColimitCompEvaluation F j).inv h)

@[simp]

theorem CategoryTheory.Limits.colimit_map_colimitObjIsoColimitCompEvaluation_hom {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor J (Functor K C)) {i j : K} (f : i ⟶ j) : CategoryStruct.comp ((colimit F).map f) (colimitObjIsoColimitCompEvaluation F j).hom = CategoryStruct.comp (colimitObjIsoColimitCompEvaluation F i).hom (colimMap (whiskerLeft F ((evaluation K C).map f)))

@[simp]

theorem CategoryTheory.Limits.colimit_map_colimitObjIsoColimitCompEvaluation_hom_assoc {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor J (Functor K C)) {i j : K} (f : i ⟶ j) {Z : C} (h : colimit (F.comp ((evaluation K C).obj j)) ⟶ Z) : CategoryStruct.comp ((colimit F).map f) (CategoryStruct.comp (colimitObjIsoColimitCompEvaluation F j).hom h) = CategoryStruct.comp (colimitObjIsoColimitCompEvaluation F i).hom (CategoryStruct.comp (colimMap (whiskerLeft F ((evaluation K C).map f))) h)

theorem CategoryTheory.Limits.colimit_obj_ext {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {H : Functor J (Functor K C)} [HasColimitsOfShape J C] {k : K} {W : C} {f g : (colimit H).obj k ⟶ W} (w : ∀ (j : J), CategoryStruct.comp ((colimit.ι H j).app k) f = CategoryStruct.comp ((colimit.ι H j).app k) g) : f = g

def CategoryTheory.Limits.colimitCompWhiskeringLeftIsoCompColimit {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (G : Functor D K) [HasColimitsOfShape J C] : colimit (F.comp ((whiskeringLeft D K C).obj G)) ≅ G.comp (colimit F)

Taking a colimit after whiskering by G is the same as using G and then taking a colimit.

Equations

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

@[simp]

theorem CategoryTheory.Limits.ι_colimitCompWhiskeringLeftIsoCompColimit_hom {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (G : Functor D K) [HasColimitsOfShape J C] (j : J) : CategoryStruct.comp (colimit.ι (F.comp ((whiskeringLeft D K C).obj G)) j) (colimitCompWhiskeringLeftIsoCompColimit F G).hom = whiskerLeft G (colimit.ι F j)

@[simp]

theorem CategoryTheory.Limits.ι_colimitCompWhiskeringLeftIsoCompColimit_hom_assoc {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (G : Functor D K) [HasColimitsOfShape J C] (j : J) {Z : Functor D C} (h : G.comp (colimit F) ⟶ Z) : CategoryStruct.comp (colimit.ι (F.comp ((whiskeringLeft D K C).obj G)) j) (CategoryStruct.comp (colimitCompWhiskeringLeftIsoCompColimit F G).hom h) = CategoryStruct.comp (whiskerLeft G (colimit.ι F j)) h

@[simp]

theorem CategoryTheory.Limits.whiskerLeft_ι_colimitCompWhiskeringLeftIsoCompColimit_inv {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (G : Functor D K) [HasColimitsOfShape J C] (j : J) : CategoryStruct.comp (whiskerLeft G (colimit.ι F j)) (colimitCompWhiskeringLeftIsoCompColimit F G).inv = colimit.ι (F.comp ((whiskeringLeft D K C).obj G)) j

@[simp]

theorem CategoryTheory.Limits.whiskerLeft_ι_colimitCompWhiskeringLeftIsoCompColimit_inv_assoc {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor J (Functor K C)) (G : Functor D K) [HasColimitsOfShape J C] (j : J) {Z : Functor D C} (h : colimit (F.comp ((whiskeringLeft D K C).obj G)) ⟶ Z) : CategoryStruct.comp (whiskerLeft G (colimit.ι F j)) (CategoryStruct.comp (colimitCompWhiskeringLeftIsoCompColimit F G).inv h) = CategoryStruct.comp (colimit.ι (F.comp ((whiskeringLeft D K C).obj G)) j) h

instance CategoryTheory.Limits.evaluationPreservesLimits {C : Type u} [Category.{v, u} C] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimits C] (k : K) : PreservesLimits ((evaluation K C).obj k)

theorem CategoryTheory.Limits.preservesLimit_of_evaluation {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor D (Functor K C)) (G : Functor J D) (H : ∀ (k : K), PreservesLimit G (F.comp ((evaluation K C).obj k))) : PreservesLimit G F

F : D ⥤ K ⥤ C preserves the limit of some G : J ⥤ D if it does for each k : K.

@[deprecated "No deprecation message was provided." (since := "2024-11-19")]

theorem CategoryTheory.Limits.preservesLimitOfEvaluation {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor D (Functor K C)) (G : Functor J D) (H : ∀ (k : K), PreservesLimit G (F.comp ((evaluation K C).obj k))) : PreservesLimit G F

theorem CategoryTheory.Limits.preservesLimitsOfShape_of_evaluation {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor D (Functor K C)) (J : Type u_1) [Category.{u_2, u_1} J] : (∀ (k : K), PreservesLimitsOfShape J (F.comp ((evaluation K C).obj k))) → PreservesLimitsOfShape J F

F : D ⥤ K ⥤ C preserves limits of shape J if it does for each k : K.

@[deprecated "No deprecation message was provided." (since := "2024-11-19")]

theorem CategoryTheory.Limits.preservesLimitsOfShapeOfEvaluation {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor D (Functor K C)) (J : Type u_1) [Category.{u_2, u_1} J] (H : ∀ (k : K), PreservesLimitsOfShape J (F.comp ((evaluation K C).obj k))) : PreservesLimitsOfShape J F

theorem CategoryTheory.Limits.preservesLimits_of_evaluation {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor D (Functor K C)) : (∀ (k : K), PreservesLimitsOfSize.{w', w, v', v, u', u} (F.comp ((evaluation K C).obj k))) → PreservesLimitsOfSize.{w', w, v', max u₂ v, u', max (max (max u u₂) v) v₂} F

F : D ⥤ K ⥤ C preserves all limits if it does for each k : K.

@[deprecated "No deprecation message was provided." (since := "2024-11-19")]

theorem CategoryTheory.Limits.preservesLimitsOfEvaluation {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor D (Functor K C)) (H : ∀ (k : K), PreservesLimitsOfSize.{w', w, v', v, u', u} (F.comp ((evaluation K C).obj k))) : PreservesLimitsOfSize.{w', w, v', max u₂ v, u', max (max (max u u₂) v) v₂} F

instance CategoryTheory.Limits.preservesLimits_const {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] : PreservesLimitsOfSize.{w', w, v, max u' v, u, max (max (max u u') v) v'} (Functor.const D)

The constant functor C ⥤ (D ⥤ C) preserves limits.

instance CategoryTheory.Limits.evaluation_preservesColimits {C : Type u} [Category.{v, u} C] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimits C] (k : K) : PreservesColimits ((evaluation K C).obj k)

theorem CategoryTheory.Limits.preservesColimit_of_evaluation {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor D (Functor K C)) (G : Functor J D) (H : ∀ (k : K), PreservesColimit G (F.comp ((evaluation K C).obj k))) : PreservesColimit G F

F : D ⥤ K ⥤ C preserves the colimit of some G : J ⥤ D if it does for each k : K.

@[deprecated "No deprecation message was provided." (since := "2024-11-19")]

theorem CategoryTheory.Limits.preservesColimitOfEvaluation {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor D (Functor K C)) (G : Functor J D) (H : ∀ (k : K), PreservesColimit G (F.comp ((evaluation K C).obj k))) : PreservesColimit G F

theorem CategoryTheory.Limits.preservesColimitsOfShape_of_evaluation {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor D (Functor K C)) (J : Type u_1) [Category.{u_2, u_1} J] : (∀ (k : K), PreservesColimitsOfShape J (F.comp ((evaluation K C).obj k))) → PreservesColimitsOfShape J F

F : D ⥤ K ⥤ C preserves all colimits of shape J if it does for each k : K.

theorem CategoryTheory.Limits.preservesColimits_of_evaluation {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {K : Type u₂} [Category.{v₂, u₂} K] (F : Functor D (Functor K C)) : (∀ (k : K), PreservesColimitsOfSize.{w', w, v', v, u', u} (F.comp ((evaluation K C).obj k))) → PreservesColimitsOfSize.{w', w, v', max u₂ v, u', max (max (max u u₂) v) v₂} F

F : D ⥤ K ⥤ C preserves all colimits if it does for each k : K.

instance CategoryTheory.Limits.preservesColimits_const {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] : PreservesColimitsOfSize.{w', w, v, max u' v, u, max (max (max u u') v) v'} (Functor.const D)

The constant functor C ⥤ (D ⥤ C) preserves colimits.

def CategoryTheory.Limits.limitIsoFlipCompLim {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] (F : Functor J (Functor K C)) : limit F ≅ F.flip.comp lim

The limit of a diagram F : J ⥤ K ⥤ C is isomorphic to the functor given by the individual limits on objects.

Equations

• CategoryTheory.Limits.limitIsoFlipCompLim F = CategoryTheory.NatIso.ofComponents (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F) ⋯

@[simp]

theorem CategoryTheory.Limits.limitIsoFlipCompLim_inv_app {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] (F : Functor J (Functor K C)) (X : K) : (limitIsoFlipCompLim F).inv.app X = (limitObjIsoLimitCompEvaluation F X).inv

@[simp]

theorem CategoryTheory.Limits.limitIsoFlipCompLim_hom_app {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] (F : Functor J (Functor K C)) (X : K) : (limitIsoFlipCompLim F).hom.app X = (limitObjIsoLimitCompEvaluation F X).hom

def CategoryTheory.Limits.limitFlipIsoCompLim {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] (F : Functor K (Functor J C)) : limit F.flip ≅ F.comp lim

A variant of limitIsoFlipCompLim where the arguments of F are flipped.

Equations

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

@[simp]

theorem CategoryTheory.Limits.limitFlipIsoCompLim_hom_app {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] (F : Functor K (Functor J C)) (X : K) : (limitFlipIsoCompLim F).hom.app X = CategoryStruct.comp (limitObjIsoLimitCompEvaluation F.flip X).hom (HasLimit.isoOfNatIso (flipCompEvaluation F X)).hom

@[simp]

theorem CategoryTheory.Limits.limitFlipIsoCompLim_inv_app {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] (F : Functor K (Functor J C)) (X : K) : (limitFlipIsoCompLim F).inv.app X = CategoryStruct.comp (HasLimit.isoOfNatIso (flipCompEvaluation F X)).inv (limitObjIsoLimitCompEvaluation F.flip X).inv

def CategoryTheory.Limits.limitIsoSwapCompLim {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] (G : Functor J (Functor K C)) : limit G ≅ (curry.obj ((Prod.swap K J).comp (uncurry.obj G))).comp lim

For a functor G : J ⥤ K ⥤ C, its limit K ⥤ C is given by (G' : K ⥤ J ⥤ C) ⋙ lim. Note that this does not require K to be small.

Equations

• CategoryTheory.Limits.limitIsoSwapCompLim G = CategoryTheory.Limits.limitIsoFlipCompLim G ≪≫ CategoryTheory.isoWhiskerRight (CategoryTheory.flipIsoCurrySwapUncurry G) CategoryTheory.Limits.lim

@[simp]

theorem CategoryTheory.Limits.limitIsoSwapCompLim_hom_app {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] (G : Functor J (Functor K C)) (X : K) : (limitIsoSwapCompLim G).hom.app X = CategoryStruct.comp (limitObjIsoLimitCompEvaluation G X).hom (limMap ((flipIsoCurrySwapUncurry G).hom.app X))

@[simp]

theorem CategoryTheory.Limits.limitIsoSwapCompLim_inv_app {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasLimitsOfShape J C] (G : Functor J (Functor K C)) (X : K) : (limitIsoSwapCompLim G).inv.app X = CategoryStruct.comp (limMap ((flipIsoCurrySwapUncurry G).inv.app X)) (limitObjIsoLimitCompEvaluation G X).inv

def CategoryTheory.Limits.colimitIsoFlipCompColim {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor J (Functor K C)) : colimit F ≅ F.flip.comp colim

The colimit of a diagram F : J ⥤ K ⥤ C is isomorphic to the functor given by the individual colimits on objects.

Equations

• CategoryTheory.Limits.colimitIsoFlipCompColim F = CategoryTheory.NatIso.ofComponents (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F) ⋯

@[simp]

theorem CategoryTheory.Limits.colimitIsoFlipCompColim_inv_app {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor J (Functor K C)) (X : K) : (colimitIsoFlipCompColim F).inv.app X = (colimitObjIsoColimitCompEvaluation F X).inv

@[simp]

theorem CategoryTheory.Limits.colimitIsoFlipCompColim_hom_app {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor J (Functor K C)) (X : K) : (colimitIsoFlipCompColim F).hom.app X = (colimitObjIsoColimitCompEvaluation F X).hom

def CategoryTheory.Limits.colimitFlipIsoCompColim {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor K (Functor J C)) : colimit F.flip ≅ F.comp colim

A variant of colimit_iso_flip_comp_colim where the arguments of F are flipped.

Equations

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

@[simp]

theorem CategoryTheory.Limits.colimitFlipIsoCompColim_hom_app {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor K (Functor J C)) (X : K) : (colimitFlipIsoCompColim F).hom.app X = CategoryStruct.comp (colimitObjIsoColimitCompEvaluation F.flip X).hom (HasColimit.isoOfNatIso (flipCompEvaluation F X)).hom

@[simp]

theorem CategoryTheory.Limits.colimitFlipIsoCompColim_inv_app {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (F : Functor K (Functor J C)) (X : K) : (colimitFlipIsoCompColim F).inv.app X = CategoryStruct.comp (HasColimit.isoOfNatIso (flipCompEvaluation F X)).inv (colimitObjIsoColimitCompEvaluation F.flip X).inv

def CategoryTheory.Limits.colimitIsoSwapCompColim {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (G : Functor J (Functor K C)) : colimit G ≅ (curry.obj ((Prod.swap K J).comp (uncurry.obj G))).comp colim

For a functor G : J ⥤ K ⥤ C, its colimit K ⥤ C is given by (G' : K ⥤ J ⥤ C) ⋙ colim. Note that this does not require K to be small.

Equations

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

@[simp]

theorem CategoryTheory.Limits.colimitIsoSwapCompColim_inv_app {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (G : Functor J (Functor K C)) (X : K) : (colimitIsoSwapCompColim G).inv.app X = CategoryStruct.comp (colimMap ((flipIsoCurrySwapUncurry G).inv.app X)) (colimitObjIsoColimitCompEvaluation G X).inv

@[simp]

theorem CategoryTheory.Limits.colimitIsoSwapCompColim_hom_app {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] [HasColimitsOfShape J C] (G : Functor J (Functor K C)) (X : K) : (colimitIsoSwapCompColim G).hom.app X = CategoryStruct.comp (colimitObjIsoColimitCompEvaluation G X).hom (colimMap ((flipIsoCurrySwapUncurry G).hom.app X))