# Documentation

Mathlib.AlgebraicGeometry.PrimeSpectrum.IsOpenComapC

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} [] (f : ) :
Set ()

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.

Instances For
theorem AlgebraicGeometry.Polynomial.comap_C_mem_imageOfDf {R : Type u_1} [] {f : } {I : } (H : I ()) :
↑(PrimeSpectrum.comap Polynomial.C) I

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