English
Let f: X → Y be a morphism of schemes. For an open subset U ⊆ Y and an open subset V ⊆ U, the restriction f|_U: X|_{f^{-1}(U)} → U has components on V that agree with restricting f's component to the preimage of V. In particular, the V-th component of the restricted morphism equals the corresponding restricted component of f.
Русский
Пусть f: X → Y — морфизм схем. Пусть U ⊆ Y — открытое множество, V ⊆ U — открытое подмножество. Ограничение f к U, обозначаемое f|_U: X|_{f^{-1}(U)} → U, имеет на V компоненту, совпадающую с ограничением соответствующей компоненты f к f^{-1}(V).
LaTeX
$$$ (f|_U).\\mathrm{app}(V) = f.\\mathrm{appLE} \\_ \\_ (\\mathrm{image\\_morphismRestrict\\_preimage}(f,U,V).le)$$$
Lean4
@[simp]
theorem morphismRestrict_app' {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V : Opens U) :
(f ∣_ U).app V = f.appLE _ _ (image_morphismRestrict_preimage f U V).le :=
morphismRestrict_app f U V
