English
The equivalence over X between closed immersions and ideal sheaf data is established by a large structure of morphisms and commutative diagrams.
Русский
Установлена эквивалентность над X между замкнутыми вложениями и данными идеал-шаров через совокупность морфизмов и коммутативных диаграмм.
LaTeX
$$$(overEquivIdealSheafData(X))\\;:\\; (Over \\;@IsClosedImmersion \\top X)^{op} \\simeq X.IdealSheafData$$$
Lean4
/-- If `f` is a closed immersion with affine target, the source is affine and
the induced map on global sections is surjective. -/
theorem isAffine_surjective_of_isAffine [IsClosedImmersion f] : IsAffine X ∧ Function.Surjective (f.appTop) :=
by
refine ⟨isAffine_of_isAffineHom f, ?_⟩
simp only [← f.toImage_imageι, Scheme.comp_appTop, CommRingCat.hom_comp, RingHom.coe_comp, Scheme.Hom.image,
Scheme.Hom.imageι]
rw [Scheme.Hom.appTop, Scheme.Hom.appTop, f.ker.subschemeι_app ⟨⊤, isAffineOpen_top Y⟩, CommRingCat.hom_comp,
RingHom.coe_comp]
exact
(ConcreteCategory.bijective_of_isIso _).2.comp
((ConcreteCategory.bijective_of_isIso _).2.comp Ideal.Quotient.mk_surjective)
