mathlib3 documentation


THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.


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 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.