English
Let f: X → Y be a morphism of_locally ringed spaces whose underlying map on topological spaces is an open embedding, and suppose every stalk map f_x is an isomorphism. Then f is an open immersion.
Русский
Пусть f: X → Y — морфизм локально кольцевых пространств, чья основанная на топологических пространствах карта является открытым вложением, и предположим, что все локальные отображения стежков f_x являются изоморфизмами. Тогда f является открытым вложением.
LaTeX
$$$\big( IsOpenEmbedding(f.base) \big) \land \big( \forall x: X, IsIso(f.stalkMap(x)) \big) \Rightarrow IsOpenImmersion(f)$$$
Lean4
/-- Suppose `X Y : SheafedSpace C`, where `C` is a concrete category,
whose forgetful functor reflects isomorphisms, preserves limits and filtered colimits.
Then a morphism `X ⟶ Y` that is a topological open embedding
is an open immersion iff every stalk map is an iso.
-/
theorem of_stalk_iso {X Y : LocallyRingedSpace} (f : X ⟶ Y) (hf : IsOpenEmbedding f.base)
[stalk_iso : ∀ x : X.1, IsIso (f.stalkMap x)] : LocallyRingedSpace.IsOpenImmersion f :=
SheafedSpace.IsOpenImmersion.of_stalk_iso _ hf (H := stalk_iso)
