Preservation of (co)limits in the functor category #
- Show that if
X ⨯ -preserves colimits inDfor anyX : D, then the product functorF ⨯ -forF : C ⥤ Dpreserves colimits.
The idea of the proof is simply that products and colimits in the functor category are computed pointwise, so pointwise preservation implies general preservation.
- Show that
F ⋙ -preserves limits if the target category has limits. - Show that
F : C ⥤ Dpreserves limits of a certain shape ifLan F.op : Cᵒᵖ ⥤ Type*preserves such limits.
References #
https://ncatlab.org/nlab/show/commutativity+of+limits+and+colimits#preservation_by_functor_categories_and_localizations
theorem
CategoryTheory.FunctorCategory.prod_preservesColimits
{C : Type u}
[CategoryTheory.Category.{v₁, u} C]
{D : Type u₂}
[CategoryTheory.Category.{u, u₂} D]
[CategoryTheory.Limits.HasBinaryProducts D]
[CategoryTheory.Limits.HasColimits D]
[∀ (X : D), CategoryTheory.Limits.PreservesColimits (CategoryTheory.Limits.prod.functor.obj X)]
(F : CategoryTheory.Functor C D)
:
CategoryTheory.Limits.PreservesColimits (CategoryTheory.Limits.prod.functor.obj F)
If X × - preserves colimits in D for any X : D, then the product functor F ⨯ - for
F : C ⥤ D also preserves colimits.
Note this is (mathematically) a special case of the statement that
"if limits commute with colimits in D, then they do as well in C ⥤ D"
but the story in Lean is a bit more complex, and this statement isn't directly a special case.
That is, even with a formalised proof of the general statement, there would still need to be some
work to convert to this version: namely, the natural isomorphism
(evaluation C D).obj k ⋙ prod.functor.obj (F.obj k) ≅ prod.functor.obj F ⋙ (evaluation C D).obj k
instance
CategoryTheory.whiskeringLeft_preservesLimitsOfShape
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(J : Type u)
[CategoryTheory.Category.{v, u} J]
[CategoryTheory.Limits.HasLimitsOfShape J D]
(F : CategoryTheory.Functor C E)
:
CategoryTheory.Limits.PreservesLimitsOfShape J ((CategoryTheory.whiskeringLeft C E D).obj F)
Equations
- ⋯ = ⋯
instance
CategoryTheory.whiskeringLeft_preservesColimitsOfShape
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(J : Type u)
[CategoryTheory.Category.{v, u} J]
[CategoryTheory.Limits.HasColimitsOfShape J D]
(F : CategoryTheory.Functor C E)
:
CategoryTheory.Limits.PreservesColimitsOfShape J ((CategoryTheory.whiskeringLeft C E D).obj F)
Equations
- ⋯ = ⋯
instance
CategoryTheory.whiskeringLeft_preservesLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
[CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₂, u₂} D]
(F : CategoryTheory.Functor C E)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.whiskeringLeft_preservesColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
[CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₂, u₂} D]
(F : CategoryTheory.Functor C E)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.whiskeringRight_preservesLimitsOfShape
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_2} D]
{E : Type u_3}
[CategoryTheory.Category.{u_7, u_3} E]
{J : Type u_4}
[CategoryTheory.Category.{u_8, u_4} J]
[CategoryTheory.Limits.HasLimitsOfShape J D]
(F : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesLimitsOfShape J F]
:
CategoryTheory.Limits.PreservesLimitsOfShape J ((CategoryTheory.whiskeringRight C D E).obj F)
Equations
- ⋯ = ⋯
def
CategoryTheory.limitCompWhiskeringRightIsoLimitComp
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_2} D]
{E : Type u_3}
[CategoryTheory.Category.{u_7, u_3} E]
{J : Type u_4}
[CategoryTheory.Category.{u_8, u_4} J]
[CategoryTheory.Limits.HasLimitsOfShape J D]
(F : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesLimitsOfShape J F]
(G : CategoryTheory.Functor J (CategoryTheory.Functor C D))
:
CategoryTheory.Limits.limit (G.comp ((CategoryTheory.whiskeringRight C D E).obj F)) ≅ (CategoryTheory.Limits.limit G).comp F
Whiskering right and then taking a limit is the same as taking the limit and applying the functor.
Equations
- CategoryTheory.limitCompWhiskeringRightIsoLimitComp F G = (CategoryTheory.preservesLimitIso ((CategoryTheory.whiskeringRight C D E).obj F) G).symm
Instances For
@[simp]
theorem
CategoryTheory.limitCompWhiskeringRightIsoLimitComp_inv_π
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_2} D]
{E : Type u_3}
[CategoryTheory.Category.{u_7, u_3} E]
{J : Type u_4}
[CategoryTheory.Category.{u_8, u_4} J]
[CategoryTheory.Limits.HasLimitsOfShape J D]
(F : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesLimitsOfShape J F]
(G : CategoryTheory.Functor J (CategoryTheory.Functor C D))
(j : J)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.limitCompWhiskeringRightIsoLimitComp F G).inv
(CategoryTheory.Limits.limit.π (G.comp ((CategoryTheory.whiskeringRight C D E).obj F)) j) = CategoryTheory.whiskerRight (CategoryTheory.Limits.limit.π G j) F
@[simp]
theorem
CategoryTheory.limitCompWhiskeringRightIsoLimitComp_inv_π_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_2} D]
{E : Type u_3}
[CategoryTheory.Category.{u_7, u_3} E]
{J : Type u_4}
[CategoryTheory.Category.{u_8, u_4} J]
[CategoryTheory.Limits.HasLimitsOfShape J D]
(F : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesLimitsOfShape J F]
(G : CategoryTheory.Functor J (CategoryTheory.Functor C D))
(j : J)
{Z : CategoryTheory.Functor C E}
(h : ((CategoryTheory.whiskeringRight C D E).obj F).obj (G.obj j) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.limitCompWhiskeringRightIsoLimitComp F G).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.limit.π (G.comp ((CategoryTheory.whiskeringRight C D E).obj F)) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.Limits.limit.π G j) F) h
@[simp]
theorem
CategoryTheory.limitCompWhiskeringRightIsoLimitComp_hom_whiskerRight_π
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_2} D]
{E : Type u_3}
[CategoryTheory.Category.{u_7, u_3} E]
{J : Type u_4}
[CategoryTheory.Category.{u_8, u_4} J]
[CategoryTheory.Limits.HasLimitsOfShape J D]
(F : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesLimitsOfShape J F]
(G : CategoryTheory.Functor J (CategoryTheory.Functor C D))
(j : J)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.limitCompWhiskeringRightIsoLimitComp F G).hom
(CategoryTheory.whiskerRight (CategoryTheory.Limits.limit.π G j) F) = CategoryTheory.Limits.limit.π (G.comp ((CategoryTheory.whiskeringRight C D E).obj F)) j
@[simp]
theorem
CategoryTheory.limitCompWhiskeringRightIsoLimitComp_hom_whiskerRight_π_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_2} D]
{E : Type u_3}
[CategoryTheory.Category.{u_7, u_3} E]
{J : Type u_4}
[CategoryTheory.Category.{u_8, u_4} J]
[CategoryTheory.Limits.HasLimitsOfShape J D]
(F : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesLimitsOfShape J F]
(G : CategoryTheory.Functor J (CategoryTheory.Functor C D))
(j : J)
{Z : CategoryTheory.Functor C E}
(h : (G.obj j).comp F ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.limitCompWhiskeringRightIsoLimitComp F G).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.Limits.limit.π G j) F) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.limit.π (G.comp ((CategoryTheory.whiskeringRight C D E).obj F)) j) h
instance
CategoryTheory.whiskeringRight_preservesColimitsOfShape
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_2} D]
{E : Type u_3}
[CategoryTheory.Category.{u_7, u_3} E]
{J : Type u_4}
[CategoryTheory.Category.{u_8, u_4} J]
[CategoryTheory.Limits.HasColimitsOfShape J D]
(F : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesColimitsOfShape J F]
:
CategoryTheory.Limits.PreservesColimitsOfShape J ((CategoryTheory.whiskeringRight C D E).obj F)
Equations
- ⋯ = ⋯
def
CategoryTheory.colimitCompWhiskeringRightIsoColimitComp
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_2} D]
{E : Type u_3}
[CategoryTheory.Category.{u_7, u_3} E]
{J : Type u_4}
[CategoryTheory.Category.{u_8, u_4} J]
[CategoryTheory.Limits.HasColimitsOfShape J D]
(F : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesColimitsOfShape J F]
(G : CategoryTheory.Functor J (CategoryTheory.Functor C D))
:
CategoryTheory.Limits.colimit (G.comp ((CategoryTheory.whiskeringRight C D E).obj F)) ≅ (CategoryTheory.Limits.colimit G).comp F
Whiskering right and then taking a colimit is the same as taking the colimit and applying the functor.
Equations
- CategoryTheory.colimitCompWhiskeringRightIsoColimitComp F G = (CategoryTheory.preservesColimitIso ((CategoryTheory.whiskeringRight C D E).obj F) G).symm
Instances For
@[simp]
theorem
CategoryTheory.ι_colimitCompWhiskeringRightIsoColimitComp_hom
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_2} D]
{E : Type u_3}
[CategoryTheory.Category.{u_7, u_3} E]
{J : Type u_4}
[CategoryTheory.Category.{u_8, u_4} J]
[CategoryTheory.Limits.HasColimitsOfShape J D]
(F : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesColimitsOfShape J F]
(G : CategoryTheory.Functor J (CategoryTheory.Functor C D))
(j : J)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.colimit.ι (G.comp ((CategoryTheory.whiskeringRight C D E).obj F)) j)
(CategoryTheory.colimitCompWhiskeringRightIsoColimitComp F G).hom = CategoryTheory.whiskerRight (CategoryTheory.Limits.colimit.ι G j) F
@[simp]
theorem
CategoryTheory.ι_colimitCompWhiskeringRightIsoColimitComp_hom_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_2} D]
{E : Type u_3}
[CategoryTheory.Category.{u_7, u_3} E]
{J : Type u_4}
[CategoryTheory.Category.{u_8, u_4} J]
[CategoryTheory.Limits.HasColimitsOfShape J D]
(F : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesColimitsOfShape J F]
(G : CategoryTheory.Functor J (CategoryTheory.Functor C D))
(j : J)
{Z : CategoryTheory.Functor C E}
(h : (CategoryTheory.Limits.colimit G).comp F ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.colimit.ι (G.comp ((CategoryTheory.whiskeringRight C D E).obj F)) j)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.colimitCompWhiskeringRightIsoColimitComp F G).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.Limits.colimit.ι G j) F) h
@[simp]
theorem
CategoryTheory.whiskerRight_ι_colimitCompWhiskeringRightIsoColimitComp_inv
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_2} D]
{E : Type u_3}
[CategoryTheory.Category.{u_7, u_3} E]
{J : Type u_4}
[CategoryTheory.Category.{u_8, u_4} J]
[CategoryTheory.Limits.HasColimitsOfShape J D]
(F : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesColimitsOfShape J F]
(G : CategoryTheory.Functor J (CategoryTheory.Functor C D))
(j : J)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.Limits.colimit.ι G j) F)
(CategoryTheory.colimitCompWhiskeringRightIsoColimitComp F G).inv = CategoryTheory.Limits.colimit.ι (G.comp ((CategoryTheory.whiskeringRight C D E).obj F)) j
@[simp]
theorem
CategoryTheory.whiskerRight_ι_colimitCompWhiskeringRightIsoColimitComp_inv_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_6, u_2} D]
{E : Type u_3}
[CategoryTheory.Category.{u_7, u_3} E]
{J : Type u_4}
[CategoryTheory.Category.{u_8, u_4} J]
[CategoryTheory.Limits.HasColimitsOfShape J D]
(F : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesColimitsOfShape J F]
(G : CategoryTheory.Functor J (CategoryTheory.Functor C D))
(j : J)
{Z : CategoryTheory.Functor C E}
(h : CategoryTheory.Limits.colimit (G.comp ((CategoryTheory.whiskeringRight C D E).obj F)) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.Limits.colimit.ι G j) F)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.colimitCompWhiskeringRightIsoColimitComp F G).inv h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.colimit.ι (G.comp ((CategoryTheory.whiskeringRight C D E).obj F)) j) h
instance
CategoryTheory.whiskeringRightPreservesLimits
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_5, u_2} D]
{E : Type u_3}
[CategoryTheory.Category.{u_6, u_3} E]
(F : CategoryTheory.Functor D E)
[CategoryTheory.Limits.HasLimitsOfSize.{w, w', u_5, u_2} D]
[CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', u_5, u_6, u_2, u_3} F]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.whiskeringRightPreservesColimits
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_5, u_2} D]
{E : Type u_3}
[CategoryTheory.Category.{u_6, u_3} E]
(F : CategoryTheory.Functor D E)
[CategoryTheory.Limits.HasColimitsOfSize.{w, w', u_5, u_2} D]
[CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', u_5, u_6, u_2, u_3} F]
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.preservesLimit_of_lan_preservesLimit
{C D : Type u}
[CategoryTheory.SmallCategory C]
[CategoryTheory.SmallCategory D]
(F : CategoryTheory.Functor C D)
(J : Type u)
[CategoryTheory.SmallCategory J]
[CategoryTheory.Limits.PreservesLimitsOfShape J F.op.lan]
:
If Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*) preserves limits of shape J, so will F.
theorem
CategoryTheory.preservesFiniteLimits_of_evaluation
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u_1}
[CategoryTheory.Category.{u_3, u_1} D]
{E : Type u_2}
[CategoryTheory.Category.{u_4, u_2} E]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D E))
(h : ∀ (d : D), CategoryTheory.Limits.PreservesFiniteLimits (F.comp ((CategoryTheory.evaluation D E).obj d)))
:
F : C ⥤ D ⥤ E preserves finite limits if it does for each d : D.
theorem
CategoryTheory.preservesFiniteColimits_of_evaluation
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u_1}
[CategoryTheory.Category.{u_3, u_1} D]
{E : Type u_2}
[CategoryTheory.Category.{u_4, u_2} E]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D E))
(h : ∀ (d : D), CategoryTheory.Limits.PreservesFiniteColimits (F.comp ((CategoryTheory.evaluation D E).obj d)))
:
F : C ⥤ D ⥤ E preserves finite limits if it does for each d : D.
noncomputable instance
CategoryTheory.instPreservesLimitsOfShapeFunctorColim
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{D : Type u₃}
[CategoryTheory.Category.{v₃, u₃} D]
[CategoryTheory.Limits.HasLimitsOfShape J C]
[CategoryTheory.Limits.HasColimitsOfShape K C]
[CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim]
:
CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim
Equations
- ⋯ = ⋯
noncomputable instance
CategoryTheory.instPreservesColimitsOfShapeFunctorLim
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{K : Type u₂}
[CategoryTheory.Category.{v₂, u₂} K]
{D : Type u₃}
[CategoryTheory.Category.{v₃, u₃} D]
[CategoryTheory.Limits.HasColimitsOfShape J C]
[CategoryTheory.Limits.HasLimitsOfShape K C]
[CategoryTheory.Limits.PreservesColimitsOfShape J CategoryTheory.Limits.lim]
:
CategoryTheory.Limits.PreservesColimitsOfShape J CategoryTheory.Limits.lim
Equations
- ⋯ = ⋯