toSpecΓ_preimage_zeroLocus — Mathlib

English

The preimage under the base map of X.toSpecΓ of the zero locus of s equals the zero locus of s on X.

Русский

Подобие предобраза через базовую карту X.toSpecΓ нулевой локус s совпадает с нулевым локусом s на X.

LaTeX

$$$X.toSpecΓ.base^{-1}(\mathrm{PrimeSpectrum}.zeroLocus(s)) = X.zeroLocus(s)$$$

Lean4

/-- On a scheme `X`, the preimage of the zero locus of the prime spectrum
of `Γ(X, ⊤)` under `X.toSpecΓ : X ⟶ Spec Γ(X, ⊤)` agrees with the associated zero locus on `X`. -/
theorem toSpecΓ_preimage_zeroLocus (s : Set Γ(X, ⊤)) : X.toSpecΓ.base ⁻¹' PrimeSpectrum.zeroLocus s = X.zeroLocus s :=
  LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq s

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