isImmersion_iff_exists_of_quasiCompact

English

A quasi-compact morphism f: X → Y is an immersion if and only if it can be factored as an open immersion g1: X → Z followed by a closed immersion g2: Z → Y, with g1 ≫ g2 = f.

Русский

Квазикоплектное отображение f: X → Y является вложением тогда и только тогда, когда его можно разложить на открытое вложение g1: X → Z и закрытое вложение g2: Z → Y, причём композиция g1 и g2 даёт f.

LaTeX

$$IsImmersion f \iff ∃ Z, g1: X → Z, g2: Z → Y, IsOpenImmersion g1 ∧ IsClosedImmersion g2 ∧ g1 ≫ g2 = f$$

Lean4

/-- A quasi-compact morphism is a (locally-closed) immersion if and only if it can be factored into
an open immersion followed by a closed immersion.
-/
theorem isImmersion_iff_exists_of_quasiCompact [QuasiCompact f] :
    IsImmersion f ↔ ∃ (Z : Scheme) (g₁ : X ⟶ Z) (g₂ : Z ⟶ Y), IsOpenImmersion g₁ ∧ IsClosedImmersion g₂ ∧ g₁ ≫ g₂ = f :=
  ⟨fun _ ↦ ⟨_, f.toImage, f.imageι, inferInstance, inferInstance, f.toImage_imageι⟩, fun ⟨_, _, _, _, _, e⟩ ↦
    e ▸ inferInstance⟩

Похожие утверждения