English
A morphism is an immersion iff it admits a factorization into a closed immersion followed by an open immersion.
Русский
Морфизм является вложением тогда и только тогда, когда он допускает факторизацию в виде замкнутого вложения, за которым следует открытое вложение.
LaTeX
$$$\\text{IsImmersion}(f) \\iff \\exists Z, g_1: X\\to Z, g_2: Z\\to Y, \\text{IsClosedImmersion}(g_1) \\land \\text{IsOpenImmersion}(g_2) \\land g_1 \\circ g_2 = f$$$
Lean4
/-- A morphism is a (locally-closed) immersion if and only if it can be factored into
a closed immersion followed by an open immersion.
-/
theorem isImmersion_iff_exists :
IsImmersion f ↔ ∃ (Z : Scheme) (g₁ : X ⟶ Z) (g₂ : Z ⟶ Y), IsClosedImmersion g₁ ∧ IsOpenImmersion g₂ ∧ g₁ ≫ g₂ = f :=
⟨fun _ ↦ ⟨_, f.liftCoborder, f.coborderRange.ι, inferInstance, inferInstance, f.liftCoborder_ι⟩,
fun ⟨_, _, _, _, _, e⟩ ↦ e ▸ inferInstance⟩
