Colimits on Grothendieck constructions preserving limits

We characterize the condition in which colimits on Grothendieck constructions preserve limits: By preserving limits on the Grothendieck construction's base category as well as on each of its fibers.

noncomputable def CategoryTheory.Limits.fiberwiseColimitLimitIso {C : Type u₁} [Category.{v₁, u₁} C] {H : Type u₂} [Category.{v₂, u₂} H] {J : Type u₃} [Category.{v₃, u₃} J] {F : Functor C Cat} (K : Functor J (Functor (Grothendieck F) H)) [∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H] [HasLimitsOfShape J H] [∀ (c : C), PreservesLimitsOfShape J colim] : fiberwiseColimit (limit K) ≅ limit (K.comp (fiberwiseColim F H))

If colim on each fiber F.obj c of a functor F : C ⥤ Cat preserves limits of shape J, then the fiberwise colimit of the limit of a functor K : J ⥤ Grothendieck F ⥤ H is naturally isomorphic to taking the limit of the composition K ⋙ fiberwiseColim F H.

@[simp]

theorem CategoryTheory.Limits.fiberwiseColimitLimitIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {H : Type u₂} [Category.{v₂, u₂} H] {J : Type u₃} [Category.{v₃, u₃} J] {F : Functor C Cat} (K : Functor J (Functor (Grothendieck F) H)) [∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H] [HasLimitsOfShape J H] [∀ (c : C), PreservesLimitsOfShape J colim] (X : C) : (fiberwiseColimitLimitIso K).inv.app X = CategoryStruct.comp (limitObjIsoLimitCompEvaluation (K.comp (fiberwiseColim F H)) X).hom (CategoryStruct.comp (HasLimit.isoOfNatIso (K.associator ((Functor.whiskeringLeft (↑(F.obj X)) (Grothendieck F) H).obj (Grothendieck.ι F X)) colim ≪≫ K.isoWhiskerLeft (fiberwiseColimCompEvaluationIso X).symm ≪≫ (K.associator (fiberwiseColim F H) ((evaluation C H).obj X)).symm)).inv (CategoryStruct.comp (preservesLimitIso colim (K.comp ((Functor.whiskeringLeft (↑(F.obj X)) (Grothendieck F) H).obj (Grothendieck.ι F X)))).inv (HasColimit.isoOfNatIso (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F X)).symm).inv))

@[simp]

theorem CategoryTheory.Limits.fiberwiseColimitLimitIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {H : Type u₂} [Category.{v₂, u₂} H] {J : Type u₃} [Category.{v₃, u₃} J] {F : Functor C Cat} (K : Functor J (Functor (Grothendieck F) H)) [∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H] [HasLimitsOfShape J H] [∀ (c : C), PreservesLimitsOfShape J colim] (X : C) : (fiberwiseColimitLimitIso K).hom.app X = CategoryStruct.comp (HasColimit.isoOfNatIso (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F X)).symm).hom (CategoryStruct.comp (preservesLimitIso colim (K.comp ((Functor.whiskeringLeft (↑(F.obj X)) (Grothendieck F) H).obj (Grothendieck.ι F X)))).hom (CategoryStruct.comp (HasLimit.isoOfNatIso (K.associator ((Functor.whiskeringLeft (↑(F.obj X)) (Grothendieck F) H).obj (Grothendieck.ι F X)) colim ≪≫ K.isoWhiskerLeft (fiberwiseColimCompEvaluationIso X).symm ≪≫ (K.associator (fiberwiseColim F H) ((evaluation C H).obj X)).symm)).hom (limitObjIsoLimitCompEvaluation (K.comp (fiberwiseColim F H)) X).inv))

instance CategoryTheory.Limits.preservesLimitsOfShape_colim_grothendieck (C : Type u₁) [Category.{v₁, u₁} C] {H : Type u₂} [Category.{v₂, u₂} H] {J : Type u₃} [Category.{v₃, u₃} J] (F : Functor C Cat) [HasColimitsOfShape C H] [HasLimitsOfShape J H] [∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H] [PreservesLimitsOfShape J colim] [∀ (c : C), PreservesLimitsOfShape J colim] : PreservesLimitsOfShape J colim

If colim on a category C preserves limits of shape J and if it does so for colim on every F.obj c for a functor F : C ⥤ Cat, then colim on Grothendieck F also preserves limits of shape J.