of_stalk_iso — Mathlib

English

For every x ∈ X, the stalk map f.stalkMap x is an isomorphism whenever f is an open immersion.

Русский

Для каждого x ∈ X отображение stalkMap f является изоморфизмом, если f — открытое вложение.

LaTeX

$$$$ \forall x, \ IsIso( f.stalkMap x ) $$$$

Lean4

theorem of_stalk_iso {X Y : Scheme.{u}} (f : X ⟶ Y) (hf : IsOpenEmbedding f.base) [∀ x, IsIso (f.stalkMap x)] :
    IsOpenImmersion f :=
  haveI (x : X) : IsIso (f.toShHom.stalkMap x) := inferInstanceAs <| IsIso (f.stalkMap x)
  SheafedSpace.IsOpenImmersion.of_stalk_iso f.toShHom hf

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