English
Let X be a Scheme and U an affine-open. For a set s of global sections on X restricted to U, the image under the canonical map to X intersects the zero locus as X.zeroLocus(s) ∩ U.
Русский
Пусть X — схема, U — аффинно открытое. Для множества s глобальных секций на X, ограниченных на U, образ через каноническое отображение пересекает нулевую локацию: X.zeroLocus(s) ∩ U.
LaTeX
$$$h_U.fromSpec.base '' PrimeSpectrum.zeroLocus(s) = X.zeroLocus(s) \cap U$$$
Lean4
theorem fromSpec_image_zeroLocus {X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U) (s : Set Γ(X, U)) :
hU.fromSpec.base '' PrimeSpectrum.zeroLocus s = X.zeroLocus s ∩ U := by
rw [← hU.fromSpec_preimage_zeroLocus, Set.image_preimage_eq_inter_range, range_fromSpec]