English
Let X be an affine scheme. A subset S of X is closed if and only if there exists an ideal I of the ring of global sections Γ(X, O_X) such that S is the zero locus of I.
Русский
Пусть X есть афинная схема. Подмножество S схемы X замкнуто тогда и только тогда, когда существует идеал I над кольцом глобальных секций Γ(X, O_X) так, что S является нулевой локацией (нулевой зоной) I.
LaTeX
$$$\operatorname{IsClosed}(S) \iff \exists I : \operatorname{Ideal}(\Gamma(X, \top)),\; S = X.zeroLocus (I : Set \Gamma(X, \top))$$$
Lean4
/-- If `X` is an affine scheme, every closed set of `X` is the zero locus
of a set of global sections. -/
theorem eq_zeroLocus_of_isClosed_of_isAffine [IsAffine X] (s : Set X) :
IsClosed s ↔ ∃ I : Ideal (Γ(X, ⊤)), s = X.zeroLocus (I : Set Γ(X, ⊤)) :=
by
refine ⟨fun hs ↦ ?_, ?_⟩
· let Z : Set (Spec <| Γ(X, ⊤)) := X.toΓSpecFun '' s
have hZ : IsClosed Z := (X.isoSpec.hom.homeomorph).isClosedMap _ hs
obtain ⟨I, (hI : Z = _)⟩ := (PrimeSpectrum.isClosed_iff_zeroLocus_ideal _).mp hZ
use I
simp only [← Scheme.toSpecΓ_preimage_zeroLocus, ← hI, Z]
symm
exact Set.preimage_image_eq _ (bijective_of_isIso X.isoSpec.hom.base).injective
· rintro ⟨I, rfl⟩
exact zeroLocus_isClosed X I.carrier
