English
The coe of vanishingIdeal t equals the set of f in R that vanish on all x in t.
Русский
Образ элемента vanishingIdeal t равен множеству f в R, которые обращаются к нулю на каждом x в t.
LaTeX
$$$(vanishingIdeal t : Set R) = \\{ f : R \\\\mid \\\\forall x \\\\in t, f \\\\in x.asIdeal \\}$$$
Lean4
/-- The vanishing ideal of a set `t` of points of the prime spectrum of a commutative ring `R` is
the intersection of all the prime ideals in the set `t`.
An element `f` of `R` can be thought of as a dependent function on the prime spectrum of `R`.
At a point `x` (a prime ideal) the function (i.e., element) `f` takes values in the quotient ring
`R` modulo the prime ideal `x`. In this manner, `vanishingIdeal t` is exactly the ideal of `R`
consisting of all "functions" that vanish on all of `t`.
-/
def vanishingIdeal (t : Set (PrimeSpectrum R)) : Ideal R :=
⨅ x ∈ t, x.asIdeal
