English
For a subset s of A, the zero locus in ProjectiveSpectrum 𝒜 consists of those points x for which s is contained in x.asHomogeneousIdeal.
Русский
Для подмножества s ⊂ A нулевая зона в ProjectiveSpectrum 𝒜 состоит из таких точек x, что s ⊆ x.asHomogeneousIdeal.
LaTeX
$$$$ \\mathrm{zeroLocus}(\\mathcal{A}, s) = \\{ x \\in \\mathrm{ProjectiveSpectrum}(\\mathcal{A}) \\;|\\; s \\subseteq x.asHomogeneousIdeal \\}.$$$$
Lean4
/-- The zero locus of a set `s` of elements of a commutative ring `A` is the set of all relevant
homogeneous prime ideals of the ring that contain the set `s`.
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, `zeroLocus s` is exactly the subset
of `ProjectiveSpectrum 𝒜` where all "functions" in `s` vanish simultaneously. -/
def zeroLocus (s : Set A) : Set (ProjectiveSpectrum 𝒜) :=
{x | s ⊆ x.asHomogeneousIdeal}
