(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.evaluationPreservesLimits) (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.preservesLimitsOfEvaluation and CategoryTheory.Limits.preservesColimitsOfEvaluation).

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.evaluationJointlyReflectsLimits {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} (c : CategoryTheory.Limits.Cone F) (t : (k : K) → CategoryTheory.Limits.IsLimit (((CategoryTheory.evaluation K C).toPrefunctor.obj k).mapCone c)) : CategoryTheory.Limits.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.

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.combineCones {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.LimitCone ((CategoryTheory.Functor.flip F).toPrefunctor.obj k)) : CategoryTheory.Limits.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.

def CategoryTheory.Limits.evaluateCombinedCones {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.LimitCone ((CategoryTheory.Functor.flip F).toPrefunctor.obj k)) (k : K) : ((CategoryTheory.evaluation K C).toPrefunctor.obj k).mapCone (CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.LimitCone ((CategoryTheory.Functor.flip F).toPrefunctor.obj k)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} (c : CategoryTheory.Limits.Cocone F) (t : (k : K) → CategoryTheory.Limits.IsColimit (((CategoryTheory.evaluation K C).toPrefunctor.obj k).mapCocone c)) : CategoryTheory.Limits.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.

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.combineCocones {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.ColimitCocone ((CategoryTheory.Functor.flip F).toPrefunctor.obj k)) : CategoryTheory.Limits.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.

def CategoryTheory.Limits.evaluateCombinedCocones {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.ColimitCocone ((CategoryTheory.Functor.flip F).toPrefunctor.obj k)) (k : K) : ((CategoryTheory.evaluation K C).toPrefunctor.obj k).mapCocone (CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.ColimitCocone ((CategoryTheory.Functor.flip F).toPrefunctor.obj k)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.combineCocones F c)

Stitching together colimiting cocones gives a colimiting cocone.

Equations

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

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

Equations

• (_ : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Functor K C)) = (_ : CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Functor K C))

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

Equations

• (_ : CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.Functor K C)) = (_ : CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.Functor K C))

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

Equations

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

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

Equations

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

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

Equations

• CategoryTheory.Limits.evaluationPreservesLimitsOfShape k = CategoryTheory.Limits.PreservesLimitsOfShape.mk

def CategoryTheory.Limits.limitObjIsoLimitCompEvaluation {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (k : K) : (CategoryTheory.Limits.limit F).toPrefunctor.obj k ≅ CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F ((CategoryTheory.evaluation K C).toPrefunctor.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).toPrefunctor.obj k) F

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.evaluationPreservesColimitsOfShape k = CategoryTheory.Limits.PreservesColimitsOfShape.mk

def CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (k : K) : (CategoryTheory.Limits.colimit F).toPrefunctor.obj k ≅ CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp F ((CategoryTheory.evaluation K C).toPrefunctor.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).toPrefunctor.obj k) F

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.evaluationPreservesLimits k = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

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

Equations

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

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

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

Equations

• CategoryTheory.Limits.preservesLimitsOfShapeOfEvaluation F J x = CategoryTheory.Limits.PreservesLimitsOfShape.mk

def CategoryTheory.Limits.preservesLimitsOfEvaluation {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor D (CategoryTheory.Functor K C)) : ((k : K) → CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v', v, u', u} (CategoryTheory.Functor.comp F ((CategoryTheory.evaluation K C).toPrefunctor.obj k))) → CategoryTheory.Limits.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.

Equations

• CategoryTheory.Limits.preservesLimitsOfEvaluation F x = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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

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

Equations

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

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

Equations

• CategoryTheory.Limits.evaluationPreservesColimits k = CategoryTheory.Limits.PreservesColimitsOfSize.mk

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

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

Equations

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

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

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

Equations

• CategoryTheory.Limits.preservesColimitsOfShapeOfEvaluation F J x = CategoryTheory.Limits.PreservesColimitsOfShape.mk

def CategoryTheory.Limits.preservesColimitsOfEvaluation {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor D (CategoryTheory.Functor K C)) : ((k : K) → CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v', v, u', u} (CategoryTheory.Functor.comp F ((CategoryTheory.evaluation K C).toPrefunctor.obj k))) → CategoryTheory.Limits.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.

Equations

• CategoryTheory.Limits.preservesColimitsOfEvaluation F x = CategoryTheory.Limits.PreservesColimitsOfSize.mk

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

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

Equations

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.limitIsoFlipCompLim {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) : CategoryTheory.Limits.limit F ≅ CategoryTheory.Functor.comp (CategoryTheory.Functor.flip F) CategoryTheory.Limits.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.limitFlipIsoCompLim_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (F : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X : K) : (CategoryTheory.Limits.limitFlipIsoCompLim F).inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasLimit.isoOfNatIso (CategoryTheory.flipCompEvaluation F X)).inv (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation (CategoryTheory.Functor.flip F) X).inv

@[simp]

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

def CategoryTheory.Limits.limitFlipIsoCompLim {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (F : CategoryTheory.Functor K (CategoryTheory.Functor J C)) : CategoryTheory.Limits.limit (CategoryTheory.Functor.flip F) ≅ CategoryTheory.Functor.comp F CategoryTheory.Limits.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.limitIsoSwapCompLim_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K) : (CategoryTheory.Limits.limitIsoSwapCompLim G).inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limMap ((CategoryTheory.flipIsoCurrySwapUncurry G).inv.app X)) (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation G X).inv

@[simp]

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

def CategoryTheory.Limits.limitIsoSwapCompLim {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) : CategoryTheory.Limits.limit G ≅ CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) (CategoryTheory.uncurry.toPrefunctor.obj G))) CategoryTheory.Limits.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.colimitIsoFlipCompColim_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K) : (CategoryTheory.Limits.colimitIsoFlipCompColim F).hom.app X = (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F X).hom

@[simp]

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

def CategoryTheory.Limits.colimitIsoFlipCompColim {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) : CategoryTheory.Limits.colimit F ≅ CategoryTheory.Functor.comp (CategoryTheory.Functor.flip F) CategoryTheory.Limits.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.colimitFlipIsoCompColim_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X : K) : (CategoryTheory.Limits.colimitFlipIsoCompColim F).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation (CategoryTheory.Functor.flip F) X).hom (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.flipCompEvaluation F X)).hom

@[simp]

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

def CategoryTheory.Limits.colimitFlipIsoCompColim {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor K (CategoryTheory.Functor J C)) : CategoryTheory.Limits.colimit (CategoryTheory.Functor.flip F) ≅ CategoryTheory.Functor.comp F CategoryTheory.Limits.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.colimitIsoSwapCompColim_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasColimitsOfShape J C] (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K) : (CategoryTheory.Limits.colimitIsoSwapCompColim G).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation G X).hom (CategoryTheory.Limits.colimMap ((CategoryTheory.flipIsoCurrySwapUncurry G).hom.app X))

@[simp]

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

def CategoryTheory.Limits.colimitIsoSwapCompColim {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasColimitsOfShape J C] (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) : CategoryTheory.Limits.colimit G ≅ CategoryTheory.Functor.comp (CategoryTheory.curry.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) (CategoryTheory.uncurry.toPrefunctor.obj G))) CategoryTheory.Limits.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.