English
For any morphism f: X → Y of schemes, f is an isomorphism if and only if f is an open immersion and epi on the base.
Русский
Для любого морфизма f: X → Y между схемами: f является изоморфизмом тогда и только тогда, когда f открыто вложение и базовый компонент является эпиморфизмом.
LaTeX
$$$\text{IsIso}(f) \iff \text{IsOpenImmersion}(f) \land \text{Epi}(f_{\text{base}})$$$
Lean4
theorem _root_.AlgebraicGeometry.isIso_iff_stalk_iso {X Y : Scheme.{u}} (f : X ⟶ Y) :
IsIso f ↔ IsIso f.base ∧ ∀ x, IsIso (f.stalkMap x) :=
by
rw [isIso_iff_isOpenImmersion, IsOpenImmersion.iff_stalk_iso, and_comm, ← and_assoc]
refine and_congr ⟨?_, ?_⟩ Iff.rfl
· rintro ⟨h₁, h₂⟩
convert_to
IsIso
(TopCat.isoOfHomeo
(Equiv.toHomeomorphOfContinuousOpen (.ofBijective _ ⟨h₂.injective, (TopCat.epi_iff_surjective _).mp h₁⟩)
h₂.continuous h₂.isOpenMap)).hom
infer_instance
· intro H; exact ⟨inferInstance, (TopCat.homeoOfIso (asIso f.base)).isOpenEmbedding⟩
