toSpecΓ_image_zeroLocus — Mathlib

English

In an affine setting, the image of the zero locus under the Spec map equals the zero locus in the spectrum.

Русский

В аффинной ситуации образ нулевого локуса под отображением Spec равен нулевому локусу в спектре.

LaTeX

$$$\mathrm{Set.image}(\mathrm{Spec.map}\, -)\; X.zeroLocus(s) = \mathrm{PrimeSpectrum}.zeroLocus(s)$$$

Lean4

theorem toSpecΓ_image_zeroLocus [IsAffine X] (s : Set Γ(X, ⊤)) :
    X.toSpecΓ.base '' X.zeroLocus s = PrimeSpectrum.zeroLocus s :=
  X.isoSpec_image_zeroLocus _

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