zeroLocus_vanishingIdeal_eq_closure

English

For any t in the spectrum, the zero locus of the vanishing ideal of t equals the closure of t.

Русский

Для любого множества t спектра нулевая локус идеала исчезновения t равна замыканию t.

LaTeX

$$$\\mathrm{zeroLocus}(\\mathrm{vanishingIdeal}(t)) = \\mathrm{closure}(t)$$$

Lean4

theorem zeroLocus_vanishingIdeal_eq_closure (t : Set (PrimeSpectrum R)) :
    zeroLocus (vanishingIdeal t : Set R) = closure t :=
  by
  rcases isClosed_iff_zeroLocus (closure t) |>.mp isClosed_closure with ⟨I, hI⟩
  rw [subset_antisymm_iff, (isClosed_zeroLocus _).closure_subset_iff, hI, subset_zeroLocus_iff_subset_vanishingIdeal,
    (gc R).u_l_u_eq_u, ← subset_zeroLocus_iff_subset_vanishingIdeal, ← hI]
  exact ⟨subset_closure, subset_zeroLocus_vanishingIdeal t⟩

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