English
For an open subset U of X and a set s of global sections on U, the preimage of the zero locus of s under the base map U.toSpecΓ equals the intersection of U with the zero locus of s on X.
Русский
Для открытого подмножества U внутри X и множества s секций на U, предобраз нулевой локации s через базовую схему U.toSpecΓ равен пересечению U с нулевой локацией s на X.
LaTeX
$$$U.toSpecΓ.base^{-1}'\,\operatorname{PrimeSpectrum.zeroLocus}(s) = U.1 \cap X.zeroLocus(s)$$$
Lean4
theorem toSpecΓ_preimage_zeroLocus {X : Scheme.{u}} (U : X.Opens) (s : Set Γ(X, U)) :
U.toSpecΓ.base ⁻¹' PrimeSpectrum.zeroLocus s = U.1 ↓∩ X.zeroLocus s :=
by
rw [toSpecΓ, Scheme.comp_base, TopCat.coe_comp, Set.preimage_comp, Spec.map_base, hom_ofHom]
erw [PrimeSpectrum.preimage_comap_zeroLocus]
rw [Scheme.toSpecΓ_preimage_zeroLocus]
change _ = U.ι.base ⁻¹' (X.zeroLocus s)
rw [Scheme.preimage_zeroLocus, U.ι_app_self, ← zeroLocus_map_of_eq _ U.ι_preimage_self, ← Set.image_comp, ←
RingHom.coe_comp, ← CommRingCat.hom_comp]
congr!
simp [← Functor.map_comp]
rfl
