isoSpec_image_zeroLocus — Mathlib

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

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