English
There is a natural isomorphism between restricting opens and then taking global sections and the presheaf giving global sections on X. In other words, restricting opens and then forgetting to presheaves, followed by taking Γ, is naturally isomorphic to the structure presheaf of X.
Русский
Существуют естественные изоморфизмы между ограничением открытых подмножеств и глобальными секциями и самой структурной пешеобразной функцией схемы X.
LaTeX
$$$\\mathrm{restrictFunctor}\\,\\colon X.\\mathrm{opens} \\to \\mathrm{Over}\\,X$ induces a natural isomorphism $X.\\mathrm{restrictFunctor}^{op} \\circ (\\mathrm{Over.forget}\\,X)^{op} \\circ \\Gamma \\cong X.\\mathrm{presheaf}$.$$
Lean4
/-- The functor taking open subsets of `X` to open subschemes of `X`. -/
@[simps! obj_left obj_hom map_left]
def restrictFunctor : X.Opens ⥤ Over X where
obj U := Over.mk U.ι
map {U V} i := Over.homMk (X.homOfLE i.le) (by simp)
map_id
U := by
ext1
exact Scheme.homOfLE_rfl _ _
map_comp {U V W} i
j := by
ext1
exact (X.homOfLE_homOfLE i.le j.le).symm
