of_surjective_of_isAffine — Mathlib

English

If X and Y are affine schemes and the map on global sections Γ(Y, O_Y) → Γ(X, O_X) is surjective, then f: X → Y is a closed immersion.

Русский

Если X и Y — аффинные схемы и отображение на глобальных секциях Γ(Y, O_Y) → Γ(X, O_X) сюръективно, то морфизм f: X → Y является замкнутым вложением.

LaTeX

$$$$\\forall X,Y\\text{ схемы with } IsAffine(X), IsAffine(Y), f:X\\to Y, \\\\text{Surjective}(f.appTop)\\Rightarrow IsClosedImmersion(f).$$$$

Lean4

/-- Any morphism between affine schemes that is surjective on global sections is a
closed immersion. -/
theorem of_surjective_of_isAffine {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y)
    (h : Function.Surjective (f.appTop)) : IsClosedImmersion f :=
  by
  rw [MorphismProperty.arrow_mk_iso_iff @IsClosedImmersion (arrowIsoSpecΓOfIsAffine f)]
  apply spec_of_surjective
  exact h

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