Spec_zeroLocus_eq_zeroLocus — Mathlib

English

For any ring R and subset s ⊆ R, the zero locus on Spec R corresponding to the image via ΓSpecIso matches the zero locus on PrimeSpectrum of s.

Русский

Для кольца R и подмножества s ⊆ R нулевая область на Spec R, соответствующая образу через ΓSpecIso, совпадает с нулевой областью на PrimeSpectrum числа s.

LaTeX

$$(Spec R).zeroLocus ((Scheme.ΓSpecIso R).inv '' s) = PrimeSpectrum.zeroLocus s$$

Lean4

theorem Spec_zeroLocus_eq_zeroLocus {R : CommRingCat} (s : Set R) :
    (Spec R).zeroLocus ((Scheme.ΓSpecIso R).inv '' s) = PrimeSpectrum.zeroLocus s :=
  by
  ext x
  suffices (∀ a ∈ s, x ∉ PrimeSpectrum.basicOpen a) ↔ x ∈ PrimeSpectrum.zeroLocus s by simpa
  simp [Spec_carrier, PrimeSpectrum.mem_zeroLocus, Set.subset_def, PrimeSpectrum.mem_basicOpen _ x]

Похожие утверждения