English
The zero locus of a set s of elements of a commutative (semi)ring R is the set of all prime ideals of R that contain s.
Русский
Нулевая характеристика множества элементов s — это множество простых идеалов, содержащих s.
LaTeX
$$$\\operatorname{zeroLocus}(s) = \\{ x \\\\in \\\\operatorname{PrimeSpectrum}(R) \\\\mid s \\\\subseteq x.asIdeal \\}$$$
Lean4
/-- The zero locus of a set `s` of elements of a commutative (semi)ring `R` is the set of all
prime ideals of the ring that contain the set `s`.
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, `zeroLocus s` is exactly the subset of
`PrimeSpectrum R` where all "functions" in `s` vanish simultaneously.
-/
def zeroLocus (s : Set R) : Set (PrimeSpectrum R) :=
{x | s ⊆ x.asIdeal}
