The morphism Spec R[x] --> Spec R induced by the natural inclusion R --> R[x] is an open map.

The main result is the first part of the statement of Lemma 00FB in the Stacks Project.

https://stacks.math.columbia.edu/tag/00FB

def AlgebraicGeometry.Polynomial.imageOfDf {R : Type u_1} [CommRing R] (f : Polynomial R) : Set (PrimeSpectrum R)

Given a polynomial f ∈ R[x], imageOfDf is the subset of Spec R where at least one of the coefficients of f does not vanish. Lemma imageOfDf_eq_comap_C_compl_zeroLocus proves that imageOfDf is the image of (zeroLocus {f})ᶜ under the morphism comap C : Spec R[x] → Spec R.

Equations

• AlgebraicGeometry.Polynomial.imageOfDf f = {p : PrimeSpectrum R | ∃ (i : ℕ), f.coeff i ∉ p.asIdeal}

theorem AlgebraicGeometry.Polynomial.isOpen_imageOfDf {R : Type u_1} [CommRing R] {f : Polynomial R} : IsOpen (AlgebraicGeometry.Polynomial.imageOfDf f)

theorem AlgebraicGeometry.Polynomial.comap_C_mem_imageOfDf {R : Type u_1} [CommRing R] {f : Polynomial R} {I : PrimeSpectrum (Polynomial R)} (H : I ∈ (PrimeSpectrum.zeroLocus {f})ᶜ) : (PrimeSpectrum.comap Polynomial.C) I ∈ AlgebraicGeometry.Polynomial.imageOfDf f

If a point of Spec R[x] is not contained in the vanishing set of f, then its image in Spec R is contained in the open set where at least one of the coefficients of f is non-zero. This lemma is a reformulation of exists_C_coeff_not_mem.

theorem AlgebraicGeometry.Polynomial.imageOfDf_eq_comap_C_compl_zeroLocus {R : Type u_1} [CommRing R] {f : Polynomial R} : AlgebraicGeometry.Polynomial.imageOfDf f = ⇑(PrimeSpectrum.comap Polynomial.C) '' (PrimeSpectrum.zeroLocus {f})ᶜ

The open set imageOfDf f coincides with the image of basicOpen f under the morphism C⁺ : Spec R[x] → Spec R.

theorem AlgebraicGeometry.Polynomial.isOpenMap_comap_C {R : Type u_1} [CommRing R] : IsOpenMap ⇑(PrimeSpectrum.comap Polynomial.C)

The morphism C⁺ : Spec R[x] → Spec R is open. Stacks Project "Lemma 00FB", first part.

https://stacks.math.columbia.edu/tag/00FB