zeroLocus_vanishingIdeal_eq_closure

English

Let t be any subset of the projective spectrum 𝒜. The zero locus of the vanishing ideal of t equals the closure of t in the Zariski topology.

Русский

Пусть t — произвольное подмножество проективного спектра 𝒜. Нулевое множество vanishingIdeal(t) равно замыканию t в топологии Зари.

LaTeX

$$$\mathrm{zeroLocus}_{\mathcal{A}}(\mathrm{vanishingIdeal}(t)) = \overline{t}$$$

Lean4

theorem zeroLocus_vanishingIdeal_eq_closure (t : Set (ProjectiveSpectrum 𝒜)) :
    zeroLocus 𝒜 (vanishingIdeal t : Set A) = closure t :=
  by
  apply Set.Subset.antisymm
  · rintro x hx t' ⟨ht', ht⟩
    obtain ⟨fs, rfl⟩ : ∃ s, t' = zeroLocus 𝒜 s := by rwa [isClosed_iff_zeroLocus] at ht'
    rw [subset_zeroLocus_iff_subset_vanishingIdeal] at ht
    exact Set.Subset.trans ht hx
  · rw [(isClosed_zeroLocus _ _).closure_subset_iff]
    exact subset_zeroLocus_vanishingIdeal 𝒜 t

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