instIsOpenImmersionToImageOfQuasiCompact

English

If f: X → Y is an immersion and quasi-compact, then the induced morphism to the image, f.toImage: X → im f, is an open immersion.

Русский

Если f: X → Y — вложение и квази-управляемо (quasi-compact), тогда отображение f к образу im f: X → im f является открытым вложением.

LaTeX

$$$IsOpenImmersion\, f^{toImage}$$$

Lean4

instance [IsImmersion f] [QuasiCompact f] : IsOpenImmersion f.toImage :=
  MorphismProperty.of_isPullback (IsImmersion.isPullback_toImage_liftCoborder f).flip inferInstance

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