English
For any s ⊆ Γ(Spec R, ⊤), the zero locus on Spec R equals the zero locus on PrimeSpectrum of the preimage under the ΓSpecIso inverse.
Русский
Для любого s ⊆ Γ(Spec R, ⊤) нулевая область на Spec R равна нулевой области на PrimeSpectrum для соответствующего образа через инверсию ΓSpecIso.
LaTeX
$$$(Spec R).zeroLocus s = PrimeSpectrum.zeroLocus (\mathrm{preimage}((\mathrm{ΓSpecIso} R)^{-1}, s))$$$
Lean4
@[simp]
theorem Spec_zeroLocus {R : CommRingCat} (s : Set Γ(Spec R, ⊤)) :
(Spec R).zeroLocus s = PrimeSpectrum.zeroLocus ((Scheme.ΓSpecIso R).inv ⁻¹' s) :=
by
convert Spec_zeroLocus_eq_zeroLocus ((Scheme.ΓSpecIso R).inv ⁻¹' s)
rw [Set.image_preimage_eq]
exact (ConcreteCategory.bijective_of_isIso (C := CommRingCat) _).2
