The prime spectrum of a polynomial ring

The map on prime spectra induced by evaluation at zero identifies the spectrum of the coefficient ring with the vanishing locus of the polynomial coordinate.

Main results

• Polynomial.range_comap_evalRingHom_zero: the image of evaluation at zero on prime spectra consists of the prime ideals containing X.

theorem Polynomial.range_comap_evalRingHom_zero (R : Type u_1) [CommRing R] : Set.range (PrimeSpectrum.comap (evalRingHom 0)) = {q : PrimeSpectrum (Polynomial R) | X ∈ q.asIdeal}

Evaluation at zero induces a map on prime spectra whose image is the vanishing locus of the polynomial coordinate.