English
For an affine X, the image of the zero locus of global sections under isoSpec matches the zero locus in the prime spectrum.
Русский
Для аффинного X образ нулевого локуса глобальных секций через isoSpec совпадает с нулевым локусом в PrimeSpectrum.
LaTeX
$$$X.isoSpec.hom.base'' X.zeroLocus s = PrimeSpectrum.zeroLocus s$$$
Lean4
/-- If `X` is affine, the image of the zero locus of global sections of `X` under `X.isoSpec`
is the zero locus in terms of the prime spectrum of `Γ(X, ⊤)`. -/
theorem isoSpec_image_zeroLocus [IsAffine X] (s : Set Γ(X, ⊤)) :
X.isoSpec.hom.base '' X.zeroLocus s = PrimeSpectrum.zeroLocus s :=
by
rw [← X.toSpecΓ_preimage_zeroLocus]
erw [Set.image_preimage_eq]
exact (bijective_of_isIso X.isoSpec.hom.base).surjective