English
Given open immersion f: X → Z and g: Y → Z with the indicated range containment, there exists a morphism lift f g H': Y → X characterized by f ∘ lift = g.
Русский
При открытом вложении f: X → Z и г: Y → Z с условием включения образов, существует морфизм lift f g H': Y → X, который удовлетворяет f ∘ lift = g.
LaTeX
$$$\exists!\ \ell: Y \to X \text{ such that } \ell ; f = g$$$
Lean4
/-- The universal property of open immersions:
For an open immersion `f : X ⟶ Z`, given any morphism of schemes `g : Y ⟶ Z` whose topological
image is contained in the image of `f`, we can lift this morphism to a unique `Y ⟶ X` that
commutes with these maps.
-/
def lift (H' : Set.range g.base ⊆ Set.range f.base) : Y ⟶ X :=
⟨LocallyRingedSpace.IsOpenImmersion.lift f.toLRSHom g.toLRSHom H'⟩
