English
For a presheafed space X and an open embedding h, the inverse of restrictStalkIso equals the stalkMap of X restricted along h.
Русский
Для X и открытого встроенного отображения h обратная restrictStalkIso равна stalkMap, ограниченной до h.
LaTeX
$$$(X.restrictStalkIso\,h\,x)^{ -1} = (X.ofRestrict\,h).stalkMap\,x$$$
Lean4
@[elementwise, reassoc]
theorem restrictStalkIso_hom_eq_germ {U : TopCat} (X : PresheafedSpace.{_, _, v} C) {f : U ⟶ (X : TopCat.{v})}
(h : IsOpenEmbedding f) (V : Opens U) (x : U) (hx : x ∈ V) :
(X.restrict h).presheaf.germ _ x hx ≫ (restrictStalkIso X h x).hom =
X.presheaf.germ (h.isOpenMap.functor.obj V) (f x) ⟨x, hx, rfl⟩ :=
colimit.ι_pre ((OpenNhds.inclusion (f x)).op ⋙ X.presheaf) (h.isOpenMap.functorNhds x).op
(op ⟨V, hx⟩)
-- We intentionally leave `simp` off the lemmas generated by `elementwise` and `reassoc`,
-- as the simpNF linter claims they never apply.
