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.
Given a polynomial f ∈ R[x]
, image_of_Df
is the subset of Spec R
where at least one
of the coefficients of f
does not vanish. Lemma image_of_Df_eq_comap_C_compl_zero_locus
proves that image_of_Df
is the image of (zero_locus {f})ᶜ
under the morphism
comap C : Spec R[x] → Spec R
.
Equations
- algebraic_geometry.polynomial.image_of_Df f = {p : prime_spectrum R | ∃ (i : ℕ), f.coeff i ∉ p.as_ideal}
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_coeff_not_mem_C_inverse
.
The open set image_of_Df f
coincides with the image of basic_open 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.