restrictStalkIso_inv_eq_ofRestrict

English

Let X be a Locally Ringed Space and h an open immersion of X into Y along with a point x lying in the open subset. The inverse of the stalk isomorphism induced by restriction equals the stalk map of the restricted object at x.

Русский

Пусть X—локально кольцевое пространство и h—открытое вложение X в некоторый X, обладающее точкой x внутри открытого подпространства. Обратное отображение стakit-изоморфизма, индуцированного ограничением, равно stalkMap ограниченного объекта в точке x.

LaTeX

$$$ (X.restrictStalkIso\ h\ x)^{-1} = (X.ofRestrict\ h).stalkMap\ x $$$

Lean4

theorem restrictStalkIso_inv_eq_ofRestrict : (X.restrictStalkIso h x).inv = (X.ofRestrict h).stalkMap x :=
  PresheafedSpace.restrictStalkIso_inv_eq_ofRestrict X.toPresheafedSpace h x

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