AlgebraicGeometry.Polynomial.comap_C_mem_imageOfDf
theorem AlgebraicGeometry.Polynomial.comap_C_mem_imageOfDf :
∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} {I : PrimeSpectrum (Polynomial R)},
I ∈ (PrimeSpectrum.zeroLocus {f})ᶜ →
(PrimeSpectrum.comap Polynomial.C) I ∈ AlgebraicGeometry.Polynomial.imageOfDf f
This theorem from algebraic geometry states that for any commutative ring `R`, given a polynomial `f` over `R` and a prime ideal `I` of the ring `R[x]` (polynomials over `R`), if `I` is not in the zero locus of `f` (the set of all prime ideals that contain `f`), then the image of `I` under the ring homomorphism induced by the constant polynomial map is contained in the subset of the prime spectrum of `R` where there exits at least one coefficient of `f` that is non-zero. This theorem is a restatement of another theorem `exists_C_coeff_not_mem`.
More concisely: Given a commutative ring `R`, a polynomial `f` over `R`, and a prime ideal `I` of `R[x]` not in the zero locus of `f`, the image of `I` under the constant polynomial map lies in the subset of the prime spectrum of `R` where at least one coefficient of `f` is non-zero.
|
AlgebraicGeometry.Polynomial.imageOfDf_eq_comap_C_compl_zeroLocus
theorem AlgebraicGeometry.Polynomial.imageOfDf_eq_comap_C_compl_zeroLocus :
∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R},
AlgebraicGeometry.Polynomial.imageOfDf f =
⇑(PrimeSpectrum.comap Polynomial.C) '' (PrimeSpectrum.zeroLocus {f})ᶜ
This theorem states that for any commutative ring `R` and any polynomial `f` over `R`, the open set `imageOfDf f`, which is a subset of the prime spectrum of `R` where at least one of the coefficients of `f` does not vanish, coincides with the image of the complement of the zero locus of `{f}` under the morphism induced by the constant polynomial function `C`. The zero locus of `{f}` is the set of all prime ideals of `R[x]` that contain `f`, and the complement of this set is mapped to the prime spectrum of `R` using `C`, which sends each element of `R` to its corresponding constant polynomial in `R[x]`.
More concisely: The image of the constant map from a commutative ring `R` to its polynomial ring `R[x]` over prime ideals in `R` that do not contain a given polynomial `f` coincides with the set of prime ideals in `R` where at least one coefficient of `f` does not vanish.
|
AlgebraicGeometry.Polynomial.isOpenMap_comap_C
theorem AlgebraicGeometry.Polynomial.isOpenMap_comap_C :
∀ {R : Type u_1} [inst : CommRing R], IsOpenMap ⇑(PrimeSpectrum.comap Polynomial.C)
The theorem `AlgebraicGeometry.Polynomial.isOpenMap_comap_C` states that for all types `R` that have a `CommRing` structure, the morphism `C⁺` from the prime spectra of `R[x]` (the ring of polynomials with coefficients in `R`) to the prime spectra of `R` itself, induced by the constant polynomial ring homomorphism `C`, is an open map. This means that the image of any open subset of the prime spectra of `R[x]` is an open subset in the prime spectra of `R`. This theorem is a part of Algebraic Geometry, verifying a lemma from the Stacks Project.
More concisely: The morphism induced by the constant polynomial ring homomorphism from the prime spectrum of a commutative ring to the prime spectrum of its polynomial extension is an open map.
|