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}
[Category.{v₁, u} C]
{D : Type u₂}
[Category.{u, u₂} D]
[Limits.HasBinaryProducts D]
[Limits.HasColimits D]
[∀ (X : D), Limits.PreservesColimits (Limits.prod.functor.obj X)]
(F : Functor C D)
:
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₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(J : Type u)
[Category.{v, u} J]
[Limits.HasLimitsOfShape J D]
(F : Functor C E)
:
Limits.PreservesLimitsOfShape J ((whiskeringLeft C E D).obj F)
instance
CategoryTheory.whiskeringLeft_preservesColimitsOfShape
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(J : Type u)
[Category.{v, u} J]
[Limits.HasColimitsOfShape J D]
(F : Functor C E)
:
Limits.PreservesColimitsOfShape J ((whiskeringLeft C E D).obj F)
instance
CategoryTheory.whiskeringLeft_preservesLimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[Limits.HasLimitsOfSize.{w, w', v₂, u₂} D]
(F : Functor C E)
:
instance
CategoryTheory.whiskeringLeft_preservesColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[Limits.HasColimitsOfSize.{w, w', v₂, u₂} D]
(F : Functor C E)
:
instance
CategoryTheory.whiskeringRight_preservesLimitsOfShape
{C : Type u_1}
[Category.{u_5, u_1} C]
{D : Type u_2}
[Category.{u_6, u_2} D]
{E : Type u_3}
[Category.{u_7, u_3} E]
{J : Type u_4}
[Category.{u_8, u_4} J]
[Limits.HasLimitsOfShape J D]
(F : Functor D E)
[Limits.PreservesLimitsOfShape J F]
:
Limits.PreservesLimitsOfShape J ((whiskeringRight C D E).obj F)
def
CategoryTheory.limitCompWhiskeringRightIsoLimitComp
{C : Type u_1}
[Category.{u_5, u_1} C]
{D : Type u_2}
[Category.{u_6, u_2} D]
{E : Type u_3}
[Category.{u_7, u_3} E]
{J : Type u_4}
[Category.{u_8, u_4} J]
[Limits.HasLimitsOfShape J D]
(F : Functor D E)
[Limits.PreservesLimitsOfShape J F]
(G : Functor J (Functor C D))
:
Limits.limit (G.comp ((whiskeringRight C D E).obj F)) ≅ (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}
[Category.{u_5, u_1} C]
{D : Type u_2}
[Category.{u_6, u_2} D]
{E : Type u_3}
[Category.{u_7, u_3} E]
{J : Type u_4}
[Category.{u_8, u_4} J]
[Limits.HasLimitsOfShape J D]
(F : Functor D E)
[Limits.PreservesLimitsOfShape J F]
(G : Functor J (Functor C D))
(j : J)
:
CategoryStruct.comp (limitCompWhiskeringRightIsoLimitComp F G).inv
(Limits.limit.π (G.comp ((whiskeringRight C D E).obj F)) j) = whiskerRight (Limits.limit.π G j) F
@[simp]
theorem
CategoryTheory.limitCompWhiskeringRightIsoLimitComp_inv_π_assoc
{C : Type u_1}
[Category.{u_5, u_1} C]
{D : Type u_2}
[Category.{u_6, u_2} D]
{E : Type u_3}
[Category.{u_7, u_3} E]
{J : Type u_4}
[Category.{u_8, u_4} J]
[Limits.HasLimitsOfShape J D]
(F : Functor D E)
[Limits.PreservesLimitsOfShape J F]
(G : Functor J (Functor C D))
(j : J)
{Z : Functor C E}
(h : ((whiskeringRight C D E).obj F).obj (G.obj j) ⟶ Z)
:
CategoryStruct.comp (limitCompWhiskeringRightIsoLimitComp F G).inv
(CategoryStruct.comp (Limits.limit.π (G.comp ((whiskeringRight C D E).obj F)) j) h) = CategoryStruct.comp (whiskerRight (Limits.limit.π G j) F) h
@[simp]
theorem
CategoryTheory.limitCompWhiskeringRightIsoLimitComp_hom_whiskerRight_π
{C : Type u_1}
[Category.{u_5, u_1} C]
{D : Type u_2}
[Category.{u_6, u_2} D]
{E : Type u_3}
[Category.{u_7, u_3} E]
{J : Type u_4}
[Category.{u_8, u_4} J]
[Limits.HasLimitsOfShape J D]
(F : Functor D E)
[Limits.PreservesLimitsOfShape J F]
(G : Functor J (Functor C D))
(j : J)
:
CategoryStruct.comp (limitCompWhiskeringRightIsoLimitComp F G).hom (whiskerRight (Limits.limit.π G j) F) = Limits.limit.π (G.comp ((whiskeringRight C D E).obj F)) j
@[simp]
theorem
CategoryTheory.limitCompWhiskeringRightIsoLimitComp_hom_whiskerRight_π_assoc
{C : Type u_1}
[Category.{u_5, u_1} C]
{D : Type u_2}
[Category.{u_6, u_2} D]
{E : Type u_3}
[Category.{u_7, u_3} E]
{J : Type u_4}
[Category.{u_8, u_4} J]
[Limits.HasLimitsOfShape J D]
(F : Functor D E)
[Limits.PreservesLimitsOfShape J F]
(G : Functor J (Functor C D))
(j : J)
{Z : Functor C E}
(h : (G.obj j).comp F ⟶ Z)
:
CategoryStruct.comp (limitCompWhiskeringRightIsoLimitComp F G).hom
(CategoryStruct.comp (whiskerRight (Limits.limit.π G j) F) h) = CategoryStruct.comp (Limits.limit.π (G.comp ((whiskeringRight C D E).obj F)) j) h
instance
CategoryTheory.whiskeringRight_preservesColimitsOfShape
{C : Type u_1}
[Category.{u_5, u_1} C]
{D : Type u_2}
[Category.{u_6, u_2} D]
{E : Type u_3}
[Category.{u_7, u_3} E]
{J : Type u_4}
[Category.{u_8, u_4} J]
[Limits.HasColimitsOfShape J D]
(F : Functor D E)
[Limits.PreservesColimitsOfShape J F]
:
Limits.PreservesColimitsOfShape J ((whiskeringRight C D E).obj F)
def
CategoryTheory.colimitCompWhiskeringRightIsoColimitComp
{C : Type u_1}
[Category.{u_5, u_1} C]
{D : Type u_2}
[Category.{u_6, u_2} D]
{E : Type u_3}
[Category.{u_7, u_3} E]
{J : Type u_4}
[Category.{u_8, u_4} J]
[Limits.HasColimitsOfShape J D]
(F : Functor D E)
[Limits.PreservesColimitsOfShape J F]
(G : Functor J (Functor C D))
:
Limits.colimit (G.comp ((whiskeringRight C D E).obj F)) ≅ (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}
[Category.{u_5, u_1} C]
{D : Type u_2}
[Category.{u_6, u_2} D]
{E : Type u_3}
[Category.{u_7, u_3} E]
{J : Type u_4}
[Category.{u_8, u_4} J]
[Limits.HasColimitsOfShape J D]
(F : Functor D E)
[Limits.PreservesColimitsOfShape J F]
(G : Functor J (Functor C D))
(j : J)
:
CategoryStruct.comp (Limits.colimit.ι (G.comp ((whiskeringRight C D E).obj F)) j)
(colimitCompWhiskeringRightIsoColimitComp F G).hom = whiskerRight (Limits.colimit.ι G j) F
@[simp]
theorem
CategoryTheory.ι_colimitCompWhiskeringRightIsoColimitComp_hom_assoc
{C : Type u_1}
[Category.{u_5, u_1} C]
{D : Type u_2}
[Category.{u_6, u_2} D]
{E : Type u_3}
[Category.{u_7, u_3} E]
{J : Type u_4}
[Category.{u_8, u_4} J]
[Limits.HasColimitsOfShape J D]
(F : Functor D E)
[Limits.PreservesColimitsOfShape J F]
(G : Functor J (Functor C D))
(j : J)
{Z : Functor C E}
(h : (Limits.colimit G).comp F ⟶ Z)
:
CategoryStruct.comp (Limits.colimit.ι (G.comp ((whiskeringRight C D E).obj F)) j)
(CategoryStruct.comp (colimitCompWhiskeringRightIsoColimitComp F G).hom h) = CategoryStruct.comp (whiskerRight (Limits.colimit.ι G j) F) h
@[simp]
theorem
CategoryTheory.whiskerRight_ι_colimitCompWhiskeringRightIsoColimitComp_inv
{C : Type u_1}
[Category.{u_5, u_1} C]
{D : Type u_2}
[Category.{u_6, u_2} D]
{E : Type u_3}
[Category.{u_7, u_3} E]
{J : Type u_4}
[Category.{u_8, u_4} J]
[Limits.HasColimitsOfShape J D]
(F : Functor D E)
[Limits.PreservesColimitsOfShape J F]
(G : Functor J (Functor C D))
(j : J)
:
CategoryStruct.comp (whiskerRight (Limits.colimit.ι G j) F) (colimitCompWhiskeringRightIsoColimitComp F G).inv = Limits.colimit.ι (G.comp ((whiskeringRight C D E).obj F)) j
@[simp]
theorem
CategoryTheory.whiskerRight_ι_colimitCompWhiskeringRightIsoColimitComp_inv_assoc
{C : Type u_1}
[Category.{u_5, u_1} C]
{D : Type u_2}
[Category.{u_6, u_2} D]
{E : Type u_3}
[Category.{u_7, u_3} E]
{J : Type u_4}
[Category.{u_8, u_4} J]
[Limits.HasColimitsOfShape J D]
(F : Functor D E)
[Limits.PreservesColimitsOfShape J F]
(G : Functor J (Functor C D))
(j : J)
{Z : Functor C E}
(h : Limits.colimit (G.comp ((whiskeringRight C D E).obj F)) ⟶ Z)
:
CategoryStruct.comp (whiskerRight (Limits.colimit.ι G j) F)
(CategoryStruct.comp (colimitCompWhiskeringRightIsoColimitComp F G).inv h) = CategoryStruct.comp (Limits.colimit.ι (G.comp ((whiskeringRight C D E).obj F)) j) h
instance
CategoryTheory.whiskeringRightPreservesLimits
{C : Type u_1}
[Category.{u_4, u_1} C]
{D : Type u_2}
[Category.{u_5, u_2} D]
{E : Type u_3}
[Category.{u_6, u_3} E]
(F : Functor D E)
[Limits.HasLimitsOfSize.{w, w', u_5, u_2} D]
[Limits.PreservesLimitsOfSize.{w, w', u_5, u_6, u_2, u_3} F]
:
instance
CategoryTheory.whiskeringRightPreservesColimits
{C : Type u_1}
[Category.{u_4, u_1} C]
{D : Type u_2}
[Category.{u_5, u_2} D]
{E : Type u_3}
[Category.{u_6, u_3} E]
(F : Functor D E)
[Limits.HasColimitsOfSize.{w, w', u_5, u_2} D]
[Limits.PreservesColimitsOfSize.{w, w', u_5, u_6, u_2, u_3} F]
:
theorem
CategoryTheory.preservesLimit_of_lan_preservesLimit
{C D : Type u}
[SmallCategory C]
[SmallCategory D]
(F : Functor C D)
(J : Type u)
[SmallCategory J]
[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₁}
[Category.{v₁, u₁} C]
{D : Type u_1}
[Category.{u_3, u_1} D]
{E : Type u_2}
[Category.{u_4, u_2} E]
(F : Functor C (Functor D E))
(h : ∀ (d : D), Limits.PreservesFiniteLimits (F.comp ((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₁}
[Category.{v₁, u₁} C]
{D : Type u_1}
[Category.{u_3, u_1} D]
{E : Type u_2}
[Category.{u_4, u_2} E]
(F : Functor C (Functor D E))
(h : ∀ (d : D), Limits.PreservesFiniteColimits (F.comp ((evaluation D E).obj d)))
:
F : C ⥤ D ⥤ E preserves finite limits if it does for each d : D.
instance
CategoryTheory.instPreservesLimitsOfShapeFunctorColim
{C : Type u}
[Category.{v, u} C]
{J : Type u₁}
[Category.{v₁, u₁} J]
{K : Type u₂}
[Category.{v₂, u₂} K]
{D : Type u₃}
[Category.{v₃, u₃} D]
[Limits.HasLimitsOfShape J C]
[Limits.HasColimitsOfShape K C]
[Limits.PreservesLimitsOfShape J Limits.colim]
:
instance
CategoryTheory.instPreservesColimitsOfShapeFunctorLim
{C : Type u}
[Category.{v, u} C]
{J : Type u₁}
[Category.{v₁, u₁} J]
{K : Type u₂}
[Category.{v₂, u₂} K]
{D : Type u₃}
[Category.{v₃, u₃} D]
[Limits.HasColimitsOfShape J C]
[Limits.HasLimitsOfShape K C]
[Limits.PreservesColimitsOfShape J Limits.lim]
: