Theorems · Definition · algebraic geometry

PrimeSpectrum.vanishingIdeal

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

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.

Defined in

Mathlib.RingTheory.Spectrum.Prime.Basic

Cited by

36 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound

Assumes

CommSemiring