colimitPresheafObjIsoComponentwiseLimit

English

For a diagram F of presheafed spaces, the presheaf on the colimit is isomorphic componentwise to the limit of the componentwise diagrams.

Русский

Для диаграммы F прешефдов пространства, прешафатовое множество на колимите изоморфно по компонентам к пределу компонетных диаграмм.

LaTeX

$$$\big(\mathrm{Limits}.colimit F\big).\mathrm{presheaf}.obj(\mathrm{op}\;U) \cong \lim (\mathrm{componentwiseDiagram}\;F\;U)$$$

Lean4

/-- The components of the colimit of a diagram of `PresheafedSpace C` is obtained
via taking componentwise limits.
-/
def colimitPresheafObjIsoComponentwiseLimit (F : J ⥤ PresheafedSpace.{_, _, v} C) [HasColimit F]
    (U : Opens (Limits.colimit F).carrier) :
    (Limits.colimit F).presheaf.obj (op U) ≅ limit (componentwiseDiagram F U) :=
  by
  refine ((sheafIsoOfIso (colimit.isoColimitCocone ⟨_, colimitCoconeIsColimit F⟩).symm).app (op U)).trans ?_
  refine (limitObjIsoLimitCompEvaluation _ _).trans (Limits.lim.mapIso ?_)
  fapply NatIso.ofComponents
  · intro X
    refine (F.obj (unop X)).presheaf.mapIso (eqToIso ?_)
    simp only [Functor.op_obj, op_inj_iff, Opens.map_coe, SetLike.ext'_iff, Set.preimage_preimage]
    refine congr_arg (Set.preimage · U.1) (funext fun x => ?_)
    erw [← TopCat.comp_app]
    congr
    exact ι_preservesColimitIso_inv (forget C) F (unop X)
  · intro X Y f
    change ((F.map f.unop).c.app _ ≫ _ ≫ _) ≫ (F.obj (unop Y)).presheaf.map _ = _ ≫ _
    rw [TopCat.Presheaf.Pushforward.comp_inv_app]
    erw [Category.id_comp]
    rw [Category.assoc]
    erw [← (F.obj (unop Y)).presheaf.map_comp, (F.map f.unop).c.naturality_assoc, ← (F.obj (unop Y)).presheaf.map_comp]
    rfl

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