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

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 : ℕ), Polynomial.coeff f i ∉ p.asIdeal}

## Instances For

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`

.

The open set `imageOfDf f`

coincides with the image of `basicOpen f`

under the
morphism `C⁺ : Spec R[x] → Spec R`

.

The morphism `C⁺ : Spec R[x] → Spec R`

is open.
Stacks Project "Lemma 00FB", first part.

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