(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)
:
@[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)
:
@[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
Instances For
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
Instances For
@[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₂)
:
@[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)
:
@[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)
:
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)
:
The stitched together cones each project down to the original given cones (up to iso).
Equations
Instances For
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
Instances For
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))
:
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
Instances For
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
Instances For
@[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₂)
:
@[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)
:
@[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)
:
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)
:
The stitched together cocones each project down to the original given cocones (up to iso).
Equations
Instances For
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
Instances For
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
Instances For
@[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)
:
@[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))
:
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))
:
pointwiseCocone is indeed a colimit cocone.
Equations
Instances For
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)]
:
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]
:
instance
CategoryTheory.Limits.functorCategoryHasColimitsOfSize
{C : Type u}
[Category.{v, u} C]
{K : Type u₂}
[Category.{v₂, u₂} K]
[HasColimitsOfSize.{v₁, u₁, v, u} 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)
:
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
Instances For
@[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 (F.whiskerLeft ((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 (F.whiskerLeft ((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 (F.whiskerLeft ((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 (F.whiskerLeft ((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))
:
theorem
CategoryTheory.Limits.limit_obj_ext_iff
{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}
:
f = g ↔ ∀ (j : J), CategoryStruct.comp f ((limit.π H j).app k) = CategoryStruct.comp g ((limit.π H j).app k)
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]
:
Taking a limit after whiskering by G is the same as using G and then taking a limit.
Equations
Instances For
@[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 (G.whiskerLeft (limit.π F j)) = limit.π (F.comp ((Functor.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 (G.whiskerLeft (limit.π F j)) h) = CategoryStruct.comp (limit.π (F.comp ((Functor.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 ((Functor.whiskeringLeft D K C).obj G)) j) = G.whiskerLeft (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 : ((Functor.whiskeringLeft D K C).obj G).obj (F.obj j) ⟶ Z)
:
CategoryStruct.comp (limitCompWhiskeringLeftIsoCompLimit F G).inv
(CategoryStruct.comp (limit.π (F.comp ((Functor.whiskeringLeft D K C).obj G)) j) h) = CategoryStruct.comp (G.whiskerLeft (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)
:
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
Instances For
@[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 (F.whiskerLeft ((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 (F.whiskerLeft ((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 (F.whiskerLeft ((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 (F.whiskerLeft ((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)
:
theorem
CategoryTheory.Limits.colimit_obj_ext_iff
{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}
:
f = g ↔ ∀ (j : J), CategoryStruct.comp ((colimit.ι H j).app k) f = CategoryStruct.comp ((colimit.ι H j).app k) 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]
:
Taking a colimit after whiskering by G is the same as using G and then taking a colimit.
Equations
Instances For
@[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 ((Functor.whiskeringLeft D K C).obj G)) j)
(colimitCompWhiskeringLeftIsoCompColimit F G).hom = G.whiskerLeft (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 ((Functor.whiskeringLeft D K C).obj G)) j)
(CategoryStruct.comp (colimitCompWhiskeringLeftIsoCompColimit F G).hom h) = CategoryStruct.comp (G.whiskerLeft (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 (G.whiskerLeft (colimit.ι F j)) (colimitCompWhiskeringLeftIsoCompColimit F G).inv = colimit.ι (F.comp ((Functor.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 ((Functor.whiskeringLeft D K C).obj G)) ⟶ Z)
:
CategoryStruct.comp (G.whiskerLeft (colimit.ι F j))
(CategoryStruct.comp (colimitCompWhiskeringLeftIsoCompColimit F G).inv h) = CategoryStruct.comp (colimit.ι (F.comp ((Functor.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.
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.
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.
instance
CategoryTheory.Limits.preservesLimits_const
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} 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.
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]
:
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))
:
The limit of a diagram F : J ⥤ K ⥤ C is isomorphic to the functor given by
the individual limits on objects.
Equations
Instances For
@[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)
:
@[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)
:
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))
:
A variant of limitIsoFlipCompLim where the arguments of F are flipped.
Equations
Instances For
@[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)
:
@[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)
:
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))
:
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
Instances For
@[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 (G.flipIsoCurrySwapUncurry.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 (G.flipIsoCurrySwapUncurry.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))
:
The colimit of a diagram F : J ⥤ K ⥤ C is isomorphic to the functor given by
the individual colimits on objects.
Equations
Instances For
@[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)
:
@[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)
:
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))
:
A variant of colimit_iso_flip_comp_colim where the arguments of F are flipped.
Equations
Instances For
@[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)
:
@[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)
:
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))
:
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
Instances For
@[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)
:
@[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)
: