Theorems · Definition · algebraic geometry

PrimeSpectrum.zeroLocus

{R : Type u} → [inst : CommSemiring R] → Set R → Set (PrimeSpectrum R)

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.

Defined in

Mathlib.RingTheory.Spectrum.Prime.Basic

Cited by

164 results in Mathlib

Foundations

Depth 16 from the axioms, rests on 169 definitions · uses no axioms

Assumes

CommSemiring