English
A compatibility relation: the germ of the restricted presheaf along V maps to the germ of X after transporting by the open embedding, via the stalkIso hom.
Русский
Совместимость: образующая картина грема ограниченного предшаблонного вдоль V равна грему X после транспортирования через открытое вложение.
LaTeX
$$$\forall U,\ X,\ f,\ h,\ V,\ x,\ hx,\; (X.restrict h).presheaf.germ V x hx \;\circ\; (restrictStalkIso\,h\,x).hom = X.presheaf.germ ((h.isOpenMap.functor.obj V)) (f x) \; \langle x, hx, rfl \rangle$$$
Lean4
@[simp, elementwise, reassoc]
theorem restrictStalkIso_inv_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.presheaf.germ (h.isOpenMap.functor.obj V) (f x) ⟨x, hx, rfl⟩ ≫ (restrictStalkIso X h x).inv =
(X.restrict h).presheaf.germ _ x hx :=
by rw [← restrictStalkIso_hom_eq_germ, Category.assoc, Iso.hom_inv_id, Category.comp_id]
