English
The universal property of closed immersions: given f: X → Z closed immersion and g: Y → Z with ker f ≤ ker g, there exists a unique lift Y → X commuting with the maps.
Русский
Универсальная характеристика замкнутого вложения: для f: X → Z (замкнутое вложение) и g: Y → Z с ker f ≤ ker g существует единственный подъём Y → X, который делает диаграмму commuting.
LaTeX
$$$lift(f,g,H): Y \\to X, \\ H: f.ker \\le g.ker, \\ g^{\\text{toImage}} \\circ lift(f,g,H) = g$$$
Lean4
/-- The universal property of closed immersions:
For a closed immersion `f : X ⟶ Z`, given any morphism of schemes `g : Y ⟶ Z` whose kernel
contains the kernel of `X` in `Z`, we can lift this morphism to a unique `Y ⟶ X` that
commutes with these maps.
-/
noncomputable def lift {X Y Z : Scheme.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) [IsClosedImmersion f] (H : f.ker ≤ g.ker) : Y ⟶ X :=
g.toImage ≫ Scheme.IdealSheafData.inclusion H ≫ inv f.toImage
