English
The restriction of a morphism f: X → Y to an open U ⊆ Y is the morphism from the restricted scheme X|_{f^{-1}(U)} to U obtained by restricting along U and composing with the projection from the pullback.
Русский
Ограничение морфизма f: X → Y до открытого множества U ⊆ Y представляет собой морфизм из ограниченного схемы X|_{f^{-1}(U)} в U, получаемый ограничением через U и композицией с проекцией из произведения.
LaTeX
$$$\mathrm{morphismRestrict}(f,U) = (\mathrm{pullbackRestrictIsoRestrict}(f,U))^{-1} \;\circ \; \mathrm{pullback.snd}.$$$
Lean4
/-- The restriction of a morphism `X ⟶ Y` onto `X |_{f ⁻¹ U} ⟶ Y |_ U`. -/
def morphismRestrict {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) : (f ⁻¹ᵁ U).toScheme ⟶ U :=
(pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd _ _
