English
The vanishing ideal of a set t of points in ProjectiveSpectrum 𝒜 is the intersection of all the corresponding homogeneous prime ideals in t.
Русский
Затухающий (ванишинг) идеал множества t точек в ProjectiveSpectrum 𝒜 есть пересечение всех соответствующих однородных простых идеалов из t.
LaTeX
$$$$ \\operatorname{vanishingIdeal}(t) = \\bigwedge_{x \\in t} x.asHomogeneousIdeal $$$$
Lean4
/-- The vanishing ideal of a set `t` of points of the projective spectrum of a commutative ring `R`
is the intersection of all the relevant homogeneous prime ideals in the set `t`.
An element `f` of `A` can be thought of as a dependent function on the projective spectrum of `𝒜`.
At a point `x` (a homogeneous prime ideal) the function (i.e., element) `f` takes values in the
quotient ring `A` modulo the prime ideal `x`. In this manner, `vanishingIdeal t` is exactly the
ideal of `A` consisting of all "functions" that vanish on all of `t`. -/
def vanishingIdeal (t : Set (ProjectiveSpectrum 𝒜)) : HomogeneousIdeal 𝒜 :=
⨅ (x : ProjectiveSpectrum 𝒜) (_ : x ∈ t), x.asHomogeneousIdeal
