English
For a morphism f: X → Y and an open U ⊆ Y with s ⊆ Γ(Y, U), the preimage of the zero locus of s equals the zero locus of the pushforward of s along f restricted to U: f.base^{-1} Y.zeroLocus s = X.zeroLocus ((f.app U).hom '' s).
Русский
Для морфизма f: X → Y и открытого U ⊆ Y с s ⊆ Γ(Y, U) предобраз нулевой области s по f равен нулевой области образа s по f на U: f.base^{-1} Y.zeroLocus s = X.zeroLocus ((f.app U).hom '' s).
LaTeX
$$$f.base^{-1} Y.zeroLocus(s) = X.zeroLocus\big((f.app U).hom '' s\big)$$$
Lean4
theorem preimage_zeroLocus {X Y : Scheme.{u}} (f : X ⟶ Y) {U : Y.Opens} (s : Set Γ(Y, U)) :
f.base ⁻¹' Y.zeroLocus s = X.zeroLocus ((f.app U).hom '' s) :=
by
ext
simp [← Scheme.preimage_basicOpen]
rfl