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.whiskeringLeftPreservesLimitsOfShape {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

• 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.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₂, u₂} D] (F : CategoryTheory.Functor C E) : CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', max u₃ v₂, max u₁ v₂, max (max (max u₂ u₃) v₂) v₃, max (max (max u₁ u₂) v₁) v₂} ((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_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

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

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] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', max u_1 u_5, max u_1 u_6, max (max (max u_1 u_2) u_4) u_5, max (max (max u_1 u_3) u_4) u_6} ((CategoryTheory.whiskeringRight C D E).obj F)

Equations

• CategoryTheory.whiskeringRightPreservesLimits F = { preservesLimitsOfShape := fun {J : Type ?u.68} [CategoryTheory.Category.{?u.69, ?u.68} 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 F.op.lan] : 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

def CategoryTheory.preservesFiniteLimitsOfEvaluation {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))) : CategoryTheory.Limits.PreservesFiniteLimits F

F : C ⥤ D ⥤ E preserves finite limits if it does for each d : D.

Equations

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

def CategoryTheory.preservesFiniteColimitsOfEvaluation {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))) : CategoryTheory.Limits.PreservesFiniteColimits F

F : C ⥤ D ⥤ E preserves finite limits if it does for each d : D.

Equations

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