English
If U is affine-open, then the preimage of the zero locus of a set of global sections on X under the map from U to Γ(X, U) identifies with the zero locus of the same set in Spec of the global sections.
Русский
Если U — аффинно-открытое подмножество, то предобраз нулевой локации множества глобальных секций на X под маппингом от U к Γ(X, U) совпадает с нулевой локацией того же множества в Spec Γ(X, U).
LaTeX
$$If [IsAffineOpen U], then $h_U.fromSpec.base^{-1}' X.zeroLocus(s) = \operatorname{PrimeSpectrum.zeroLocus}(s)$.$$
Lean4
theorem fromSpec_preimage_zeroLocus {X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U) (s : Set Γ(X, U)) :
hU.fromSpec.base ⁻¹' X.zeroLocus s = PrimeSpectrum.zeroLocus s :=
by
ext x
suffices (∀ f ∈ s, ¬f ∉ x.asIdeal) ↔ s ⊆ x.asIdeal by simpa [← hU.fromSpec_image_basicOpen, -not_not] using this
simp_rw [not_not]
rfl