English
The global sections functor commutes with restriction: the map on Γ of the restricted morphism factors through the corresponding maps on presheaves and the restriction morphisms.
Русский
Функтор глобальных секций коммутирует с ограничением: отображение на глобальных секциях ограниченного морфизма факторизуется через соответствующие отображения на предпись (presheaves) и ограничивающие морфизмы.
LaTeX
$$$\Gamma(map)(\mathrm{morphismRestrict}(f,U)) = Y.presheaf.map\circ f.app\circ X.presheaf.map$$$
Lean4
theorem Γ_map_morphismRestrict {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) :
Scheme.Γ.map (f ∣_ U).op =
Y.presheaf.map (eqToHom U.isOpenEmbedding_obj_top.symm).op ≫
f.app U ≫ X.presheaf.map (eqToHom (f ⁻¹ᵁ U).isOpenEmbedding_obj_top).op :=
by
rw [Scheme.Γ_map_op, morphismRestrict_appTop f U, f.naturality_assoc, ← X.presheaf.map_comp]
rfl
