English
Let f: X → Y be a quasi-compact immersion. Then X is the pullback of the closed immersion im f → Y along an open immersion U → Y; in other words, there exists a cartesian square with X mapping to im f and to U, and Y receiving the two maps from im f and U through which f factors.
Русский
Пусть f: X → Y представляет собой ограниченное по плотности вложение. Тогда X является пуллбэком закрытого вложения im f → Y вдоль открытого вложения U → Y; то есть существует канонический квадрат, в котором X является произведением по f через im f и через U, и куда im f и U проецируются в Y.
LaTeX
$$$\exists i:\mathrm{im}(f)\hookrightarrow Y\quad\text{(закрытое вложение)},\quad j:\,U\hookrightarrow Y\quad\text{(открытое вложение)},\quad X\cong_Y \mathrm{im}(f)\times_Y U,\quad \text{пр projections coincide with } f^{\mathrm{toImage}}, f^{\mathrm{liftCoborder}}.$$$
Lean4
/-- If `f : X ⟶ Y` is a quasi-compact immersion, then `X` is the pullback of the
closed immersion `im f ⟶ Y` and an open immersion `U ⟶ Y`.
-/
theorem isPullback_toImage_liftCoborder [IsImmersion f] [QuasiCompact f] :
IsPullback f.toImage f.liftCoborder f.imageι f.coborderRange.ι :=
by
refine (isPullback_of_isClosedImmersion _ _ _ _ (by simp) ?_).flip
rw [Hom.imageι, IdealSheafData.ker_subschemeι]
ext U : 2
simp only [IdealSheafData.ideal_comap_of_isOpenImmersion, Opens.ι_appIso, Iso.refl_inv, Hom.ker_apply,
RingHom.comap_ker, ← CommRingCat.hom_comp, Opens.toScheme, restrict_presheaf_obj, Category.id_comp]
rw [liftCoborder_app, CommRingCat.hom_comp, RingHom.ker_comp_of_injective]
rw [← ConcreteCategory.mono_iff_injective_of_preservesPullback]
infer_instance
