iff_stalk_iso — Mathlib

English

For a morphism f: X → Y of schemes, f is an open immersion if and only if the base map f.base is an open embedding and every stalk map f.stalkMap x is an isomorphism.

Русский

Для морфизма f: X → Y между схемами: f является открытым вложением тогда и только тогда, когда базовая карта f.base является открытым вложением, и для каждого x ∈ X отображение штампа стоиков f.stalkMap x является изоморфизмом.

LaTeX

$$$\text{IsOpenImmersion}(f) \iff \text{IsOpenEmbedding}(f_{\text{base}}) \land \forall x, \text{IsIso}(f_{\text{stalk}}(x))$$$

Lean4

theorem iff_stalk_iso {X Y : Scheme.{u}} (f : X ⟶ Y) :
    IsOpenImmersion f ↔ IsOpenEmbedding f.base ∧ ∀ x, IsIso (f.stalkMap x) :=
  ⟨fun H => ⟨H.1, fun x ↦ inferInstanceAs <| IsIso (f.toPshHom.stalkMap x)⟩, fun ⟨h, _⟩ =>
    IsOpenImmersion.of_stalk_iso f h⟩

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