preservesLimitsOfShape_colim_grothendieck

English

There is an instance that the functor colim in the Grothendieck construction preserves limits of shape J, provided fiberwise conditions hold and base colimits/limits exist.

Русский

Существует экземпляр, утверждающий, что колимит в конструировании Гротендика сохраняет пределы формы J при выполнении необходимых условий на волокна и базовые пределы/колимиты.

LaTeX

$$$\\operatorname{PreservesLimitsOfShape}\\;J\\;\\big(\\mathrm{colim}\\;\\mathrm{Grothendieck}\\;F\\big)$$$

Lean4

/-- 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`. -/
instance preservesLimitsOfShape_colim_grothendieck [HasColimitsOfShape C H] [HasLimitsOfShape J H]
    [∀ c, HasColimitsOfShape (↑(F.obj c)) H] [PreservesLimitsOfShape J (colim (J := C) (C := H))]
    [∀ c, PreservesLimitsOfShape J (colim (J := F.obj c) (C := H))] :
    PreservesLimitsOfShape J (colim (J := Grothendieck F) (C := H)) :=
  by
  constructor
  intro K
  let i₂ :=
    calc
      colimit (limit K)
      _ ≅ colimit (fiberwiseColimit (limit K)) := (colimitFiberwiseColimitIso _).symm
      _ ≅ colimit (limit (K ⋙ fiberwiseColim _ _)) := (HasColimit.isoOfNatIso (fiberwiseColimitLimitIso _))
      _ ≅ limit ((K ⋙ fiberwiseColim _ _) ⋙ colim) := (preservesLimitIso colim (K ⋙ fiberwiseColim _ _))
      _ ≅ limit (K ⋙ colim) := HasLimit.isoOfNatIso (associator _ _ _ ≪≫ isoWhiskerLeft _ fiberwiseColimCompColimIso)
  haveI : IsIso (limit.post K colim) := by
    convert Iso.isIso_hom i₂
    ext
    simp only [colim_obj, Functor.comp_obj, limit.post_π, colim_map, Iso.trans_def, Iso.trans_assoc, Iso.trans_hom,
      Category.assoc, HasLimit.isoOfNatIso_hom_π, fiberwiseColim_obj, isoWhiskerLeft_hom, NatTrans.comp_app,
      Functor.associator_hom_app, whiskerLeft_app, fiberwiseColimCompColimIso_hom_app, Category.id_comp,
      preservesLimitIso_hom_π_assoc, i₂]
    ext
    simp only [ι_colimMap, Trans.trans, Iso.symm_hom, ι_colimitFiberwiseColimitIso_inv_assoc,
      HasColimit.isoOfNatIso_ι_hom_assoc, fiberwiseColimit_obj, fiberwiseColimitLimitIso_hom_app, ι_colimMap_assoc,
      Category.assoc, limitObjIsoLimitCompEvaluation_inv_π_app_assoc, Functor.comp_obj, fiberwiseColim_obj,
      HasLimit.isoOfNatIso_hom_π_assoc, whiskeringLeft_obj_obj, colim_obj, evaluation_obj_obj, Iso.trans_hom,
      isoWhiskerLeft_hom, NatTrans.comp_app, Functor.associator_hom_app, whiskerLeft_app,
      fiberwiseColimCompEvaluationIso_inv_app, Functor.associator_inv_app, Category.comp_id, Category.id_comp,
      preservesLimitIso_hom_π_assoc, colim_map, Grothendieck.ι_obj, ι_colimitFiberwiseColimitIso_hom]
    simp [← Category.assoc, ← NatTrans.comp_app]
  apply preservesLimit_of_isIso_post

Похожие утверждения