algebraic_geometry.prime_spectrum.is_open_comap_C

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.

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

def algebraic_geometry.polynomial.image_of_Df {R : Type u_1} [comm_ring R] (f : polynomial R) :

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}

source

theorem algebraic_geometry.polynomial.is_open_image_of_Df {R : Type u_1} [comm_ring R] {f : polynomial R} :

is_open (algebraic_geometry.polynomial.image_of_Df f)

source

theorem algebraic_geometry.polynomial.comap_C_mem_image_of_Df {R : Type u_1} [comm_ring R] {f : polynomial R} {I : prime_spectrum (polynomial R)} (H : I ∈ (prime_spectrum.zero_locus {f})ᶜ) :

⇑(prime_spectrum.comap polynomial.C) I ∈ algebraic_geometry.polynomial.image_of_Df 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.

source

theorem algebraic_geometry.polynomial.image_of_Df_eq_comap_C_compl_zero_locus {R : Type u_1} [comm_ring R] {f : polynomial R} :

algebraic_geometry.polynomial.image_of_Df f = ⇑(prime_spectrum.comap polynomial.C) '' (prime_spectrum.zero_locus {f})ᶜ

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

source

theorem algebraic_geometry.polynomial.is_open_map_comap_C {R : Type u_1} [comm_ring R] :

is_open_map ⇑(prime_spectrum.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