English
Inverse of the stalk-isomorphism for the restrict is equal to the stalkMap of the restricted presheaf.
Русский
Обратная связка restrictStalkIso равна stalkMap у ограниченного предшаблона.
LaTeX
$$$(X.restrictStalkIso\,h\,x).inv = (X.ofRestrict\,h).stalkMap\,x$$$
Lean4
theorem restrictStalkIso_inv_eq_ofRestrict {U : TopCat} (X : PresheafedSpace.{_, _, v} C) {f : U ⟶ (X : TopCat.{v})}
(h : IsOpenEmbedding f) (x : U) : (X.restrictStalkIso h x).inv = (X.ofRestrict h).stalkMap x := by
-- We can't use `ext` here because it would call `stalk_hom_ext` instead.
refine colimit.hom_ext fun V => ?_
induction V with
| op V => ?_
let i : (h.isOpenMap.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE (Set.image_preimage_subset f _)
erw [Iso.comp_inv_eq, colimit.ι_map_assoc, colimit.ι_map_assoc, colimit.ι_pre]
simp_rw [Category.assoc]
erw [colimit.ι_pre ((OpenNhds.inclusion (f x)).op ⋙ X.presheaf) (h.isOpenMap.functorNhds x).op]
erw [← X.presheaf.map_comp_assoc]
exact (colimit.w ((OpenNhds.inclusion (f x)).op ⋙ X.presheaf) i.op).symm
