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⟩