(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.obj j).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.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).obj k).mapCone 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.
Instances For
@[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).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).obj k))
{k₁ : K}
{k₂ : K}
(f : k₁ ⟶ k₂)
:
(CategoryTheory.Limits.combineCones F c).pt.map f = CategoryTheory.Limits.IsLimit.lift (c k₂).isLimit
{ pt := (c k₁).cone.pt,
π := CategoryTheory.CategoryStruct.comp (c k₁).cone.π ((CategoryTheory.Functor.flip F).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).obj k))
(k : K)
:
(CategoryTheory.Limits.combineCones F c).pt.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).obj k))
:
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.
Instances For
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).obj k))
(k : K)
:
((CategoryTheory.evaluation K C).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).
Instances For
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).obj k))
:
Stitching together limiting cones gives a limiting cone.
Instances For
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).obj k).mapCocone 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.
Instances For
@[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).obj k))
(k : K)
:
(CategoryTheory.Limits.combineCocones F c).pt.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).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).obj k))
{k₁ : K}
{k₂ : K}
(f : k₁ ⟶ k₂)
:
(CategoryTheory.Limits.combineCocones F c).pt.map f = CategoryTheory.Limits.IsColimit.desc (c k₁).isColimit
{ pt := (c k₂).cocone.pt,
ι := CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.flip F).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).obj k))
:
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.
Instances For
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).obj k))
(k : K)
:
((CategoryTheory.evaluation K C).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).
Instances For
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).obj k))
:
Stitching together colimiting cocones gives a colimiting cocone.
Instances For
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]
:
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]
:
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]
:
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]
:
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)
:
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).obj k ≅ CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F ((CategoryTheory.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.
Instances For
@[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.Functor.comp F ((CategoryTheory.evaluation K C).obj k)).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).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).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.obj j).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).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).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).obj j)) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit F).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).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).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).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).obj j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F i).inv
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit F).map f) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.limMap (CategoryTheory.whiskerLeft F ((CategoryTheory.evaluation K C).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).map f) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.limMap (CategoryTheory.whiskerLeft F ((CategoryTheory.evaluation K C).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).obj k}
{g : W ⟶ (CategoryTheory.Limits.limit H).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)
:
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).obj k ≅ CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp F ((CategoryTheory.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.
Instances For
@[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).obj k ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp F ((CategoryTheory.evaluation K C).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)
:
@[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).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).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)
:
@[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).obj j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F i).inv
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit F).map f) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.colimMap (CategoryTheory.whiskerLeft F ((CategoryTheory.evaluation K C).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).map f) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.colimMap (CategoryTheory.whiskerLeft F ((CategoryTheory.evaluation K C).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).obj j)) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit F).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).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).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).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).obj k ⟶ W}
{g : (CategoryTheory.Limits.colimit H).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)
:
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).obj k)))
:
F : D ⥤ K ⥤ C preserves the limit of some G : J ⥤ D if it does for each k : K.
Instances For
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).obj k))) →
CategoryTheory.Limits.PreservesLimitsOfShape J F
F : D ⥤ K ⥤ C preserves limits of shape J if it does for each k : K.
Instances For
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))
:
F : D ⥤ K ⥤ C preserves all limits if it does for each k : K.
Instances For
instance
CategoryTheory.Limits.preservesLimitsConst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
:
The constant functor C ⥤ (D ⥤ C) preserves limits.
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)
:
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).obj k)))
:
F : D ⥤ K ⥤ C preserves the colimit of some G : J ⥤ D if it does for each k : K.
Instances For
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).obj k))) →
CategoryTheory.Limits.PreservesColimitsOfShape J F
F : D ⥤ K ⥤ C preserves all colimits of shape J if it does for each k : K.
Instances For
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))
:
F : D ⥤ K ⥤ C preserves all colimits if it does for each k : K.
Instances For
instance
CategoryTheory.Limits.preservesColimitsConst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
:
The constant functor C ⥤ (D ⥤ C) preserves colimits.
@[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.
Instances For
@[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)
:
@[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)
:
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.
Instances For
@[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)
:
@[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)
:
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.obj
(CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) (CategoryTheory.uncurry.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.
Instances For
@[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.
Instances For
@[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)
:
@[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)
:
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.
Instances For
@[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)
:
@[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)
:
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.obj
(CategoryTheory.Functor.comp (CategoryTheory.Prod.swap K J) (CategoryTheory.uncurry.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.