English
There is a natural isomorphism between restricting opens, forgetting the structure, and Γ that is compatible with the structure presheaf on X; i.e., a natural isomorphism of functors as stated.
Русский
Существует естественная изоморфизм между ограничением открытых подмножеств, забыванием структуры и Γ, совместимый с presheaf-структурой X.
LaTeX
$$$\\text{restrictFunctor}\\;:\\; X.\\text{restrictFunctor}^{op} \\Rightarrow X.\\text{presheaf}$ is isomorphic to the structure presheaf via a natural isomorphism.$$
Lean4
/-- The functor that restricts to open subschemes and then takes global section is
isomorphic to the structure sheaf. -/
@[simps!]
def restrictFunctorΓ : X.restrictFunctor.op ⋙ (Over.forget X).op ⋙ Scheme.Γ ≅ X.presheaf :=
NatIso.ofComponents (fun U => X.presheaf.mapIso ((eqToIso (unop U).isOpenEmbedding_obj_top).symm.op :))
(by
intro U V i
dsimp
rw [X.homOfLE_appTop, ← Functor.map_comp, ← Functor.map_comp]
congr 1)
