Lean4
/-- 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`. -/
@[simps!]
def fiberwiseColimitLimitIso (K : J ⥤ Grothendieck F ⥤ H) [∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H]
[HasLimitsOfShape J H] [∀ c, PreservesLimitsOfShape J (colim (J := F.obj c) (C := H))] :
fiberwiseColimit (limit K) ≅ limit (K ⋙ fiberwiseColim F H) :=
NatIso.ofComponents
(fun c =>
HasColimit.isoOfNatIso (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F c)).symm ≪≫
preservesLimitIso colim _ ≪≫
HasLimit.isoOfNatIso
(associator _ _ _ ≪≫
isoWhiskerLeft _ (fiberwiseColimCompEvaluationIso _).symm ≪≫ (associator _ _ _).symm) ≪≫
(limitObjIsoLimitCompEvaluation _ c).symm)
fun {c₁ c₂} f =>
by
simp only [fiberwiseColimit_obj, fiberwiseColimit_map, Iso.trans_hom, Iso.symm_hom, Category.assoc,
limitObjIsoLimitCompEvaluation_inv_limit_map]
apply colimit.hom_ext
intro d
simp only [← Category.assoc]
congr 1
apply limit.hom_ext
intro e
simp [← NatTrans.comp_app_assoc]
