vanishingIdeal_closure — Mathlib

English

The vanishing ideal is stable under taking closures: vanishingIdeal(closure t) = vanishingIdeal(t).

Русский

Идеал зануляния стабилен под взятием замыкания: vanishingIdeal(closure t) = vanishingIdeal(t).

LaTeX

$$$\mathrm{vanishingIdeal}(\overline{t}) = \mathrm{vanishingIdeal}(t)$$$

Lean4

theorem vanishingIdeal_closure (t : Set (ProjectiveSpectrum 𝒜)) : vanishingIdeal (closure t) = vanishingIdeal t :=
  by
  have : (vanishingIdeal (zeroLocus 𝒜 (vanishingIdeal t))).toIdeal = _ := (gc_ideal 𝒜).u_l_u_eq_u t
  ext1
  rw [zeroLocus_vanishingIdeal_eq_closure 𝒜 t] at this
  exact this

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