isIso_of_isClosedImmersion_of_surjective

English

A surjective closed immersion is an isomorphism when the target is reduced.

Русский

Замкнутое вложение, являющееся сюръективным, есть изоморфизм при редуцированной цели.

LaTeX

$$IsIso f if IsClosedImmersion f and Surjective f and IsReduced target$$

Lean4

/-- A surjective closed immersion is an isomorphism when the target is reduced. -/
theorem isIso_of_isClosedImmersion_of_surjective {X Y : Scheme.{u}} (f : X ⟶ Y) [IsClosedImmersion f] [Surjective f]
    [IsReduced Y] : IsIso f :=
  by
  rw [IsClosedImmersion.isIso_iff_ker_eq_bot, ← Scheme.IdealSheafData.support_eq_top_iff, ←
    SetLike.coe_injective.eq_iff, Scheme.Hom.support_ker]
  simp

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