Preservation of (co)limits in the functor category

• Show that if X ⨯ - preserves colimits in D for any X : D, then the product functor F ⨯ - for F : C ⥤ D preserves 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 ⥤ D preserves limits of a certain shape if Lan F.op : Cᵒᵖ ⥤ Type* preserves such limits.

References

https://ncatlab.org/nlab/show/commutativity+of+limits+and+colimits#preservation_by_functor_categories_and_localizations

def CategoryTheory.FunctorCategory.prodPreservesColimits {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

Equations

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

instance CategoryTheory.whiskeringLeftPreservesLimits {C : Type u} [CategoryTheory.Category.{v₁, u} C] {D : Type u₂} [CategoryTheory.Category.{u, u₂} D] {E : Type u} [CategoryTheory.Category.{v₂, u} E] [CategoryTheory.Limits.HasLimits D] (F : CategoryTheory.Functor C E) : CategoryTheory.Limits.PreservesLimits ((CategoryTheory.whiskeringLeft C E D).obj F)

Equations

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

instance CategoryTheory.whiskeringRightPreservesLimitsOfShape {C : Type u} [CategoryTheory.Category.{u_3, u} C] {D : Type u_1} [CategoryTheory.Category.{u, u_1} D] {E : Type u_2} [CategoryTheory.Category.{u, u_2} E] {J : Type u} [CategoryTheory.SmallCategory 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

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

instance CategoryTheory.whiskeringRightPreservesLimits {C : Type u} [CategoryTheory.Category.{u_3, u} C] {D : Type u_1} [CategoryTheory.Category.{u, u_1} D] {E : Type u_2} [CategoryTheory.Category.{u, u_2} E] (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.HasLimits D] [CategoryTheory.Limits.PreservesLimits F] : CategoryTheory.Limits.PreservesLimits ((CategoryTheory.whiskeringRight C D E).obj F)

Equations

• CategoryTheory.whiskeringRightPreservesLimits F = { preservesLimitsOfShape := fun {J : Type u} [CategoryTheory.Category.{u, u} J] => inferInstance }

noncomputable def CategoryTheory.preservesLimitOfLanPreservesLimit {C : Type u} {D : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] (F : CategoryTheory.Functor C D) (J : Type u) [CategoryTheory.SmallCategory J] [CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.lan F.op)] : CategoryTheory.Limits.PreservesLimitsOfShape J F

If Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*) preserves limits of shape J, so will F.

Equations

• CategoryTheory.preservesLimitOfLanPreservesLimit F J = CategoryTheory.Limits.preservesLimitsOfShapeOfReflectsOfPreserves F CategoryTheory.yoneda