Restricting a scheme morphism to opens

Stream: Is there code for X?

[Kenny Lau]

import Mathlib

universe u

namespace AlgebraicGeometry.Scheme

open CategoryTheory

noncomputable def Hom.restrict {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Opens X) (V : Opens Y)
    (huv : U ≤ V.comap f.base.hom) : U.toScheme ⟶ V.toScheme :=
  IsOpenImmersion.lift V.ι (U.ι ≫ f) (by simpa [Set.range_comp] using huv)

end AlgebraicGeometry.Scheme

[Kenny Lau]

do we have this?

[Kenny Lau]

I can accept the answer "just use open immersion lift as you did, this doesn't need a separate definition"

[Christian Merten]

docs#AlgebraicGeometry.Scheme.Hom.resLE

[Kenny Lau]

nice, thanks