isIso_of_injective_of_isAffine — Mathlib

English

If f is a closed immersion with affine target and the map on global sections is injective, f is an isomorphism.

Русский

Если f — замкнутое вложение с аффинной целью и инъективен переход на глобальные секции, то f является изоморфизмом.

LaTeX

$$$[IsClosedImmersion f] \\land Injective(f.appTop) \\Rightarrow IsIso f$$$

Lean4

/-- If `f` is a closed immersion with affine target such that the induced map on global
sections is injective, `f` is an isomorphism. -/
theorem isIso_of_injective_of_isAffine [IsClosedImmersion f] (hf : Function.Injective (f.appTop)) : IsIso f :=
  isIso_iff_ker_eq_bot.mpr
    (Scheme.IdealSheafData.ext_of_isAffine
      (by simpa [f.ker_apply ⟨⊤, isAffineOpen_top Y⟩, ← RingHom.injective_iff_ker_eq_bot]))

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