isoSpec_inv_image_zeroLocus — Mathlib

English

Under an affine hypothesis, the image of the zero locus of global sections through the inverse isoSpec map equals the zero locus on the scheme.

Русский

При допущении аффинности образ нулевого локуса глобальных секций через обратное isoSpec равен нулевому локусу на схеме.

LaTeX

$$$X.isoSpec.inv.base '' PrimeSpectrum.zeroLocus s = X.zeroLocus s$$$

Lean4

theorem isoSpec_inv_image_zeroLocus [IsAffine X] (s : Set Γ(X, ⊤)) :
    X.isoSpec.inv.base '' PrimeSpectrum.zeroLocus s = X.zeroLocus s :=
  by
  rw [← isoSpec_inv_preimage_zeroLocus, Set.image_preimage_eq]
  exact (bijective_of_isIso X.isoSpec.inv.base).surjective

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