isIso_iff_isOpenImmersion — Mathlib

English

For a morphism f: X → Y of schemes, f is an isomorphism if and only if f.base is an isomorphism and all stalk maps f.stalkMap x are isomorphisms.

Русский

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

LaTeX

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

Lean4

theorem _root_.AlgebraicGeometry.isIso_iff_isOpenImmersion {X Y : Scheme.{u}} (f : X ⟶ Y) :
    IsIso f ↔ IsOpenImmersion f ∧ Epi f.base :=
  ⟨fun _ => ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ => IsOpenImmersion.to_iso f⟩

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