forget_map_isOpenImmersion — Mathlib

English

If f: X → Z is an open immersion of schemes, then the induced map forget.map f from schemes to LocallyRingedSpaces is a LocallyRingedSpace open immersion.

Русский

Если f: X → Z является открытым вложением схем, то индуцированная карта forget.map f из схем в локально кольцевые пространства является открытым вложением в локально кольцевых пространствах.

LaTeX

$$$\text{IsOpenImmersion}(f) \Rightarrow \text{LocallyRingedSpace.IsOpenImmersion}(\text{forget}.map f)$$$

Lean4

instance forget_map_isOpenImmersion : LocallyRingedSpace.IsOpenImmersion ((forget).map f) :=
  ⟨H.base_open, H.c_iso⟩

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