Prime spectrum of (multivariate) polynomials #
Also see AlgebraicGeometry/AffineSpace
for the affine space over arbitrary schemes.
Main results #
isNilpotent_tensor_residueField_iff
: IfA
is a finite freeR
-algebra, thenf : A
is nilpotent onฮบ(๐ญ) โ A
for some prime๐ญ โ R
if and only if every non-leading coefficient ofcharpoly(f)
is in๐ญ
.Polynomial.exists_image_comap_of_monic
: Ifg : R[X]
is monic, the image ofZ(g) โฉ D(f) : Spec R[X]
inSpec R
is compact open.Polynomial.isOpenMap_comap_C
: The structure mapSpec R[X] โ Spec R
is an open map.MvPolynomial.isOpenMap_comap_C
: The structure mapSpec R[Xฬฒ] โ Spec R
is an open map.
theorem
isNilpotent_tensor_residueField_iff
{R : Type u_1}
{A : Type u_2}
[CommRing R]
[CommRing A]
[Algebra R A]
[Module.Free R A]
[Module.Finite R A]
(f : A)
(I : Ideal R)
[I.IsPrime]
:
If A
is a finite free R
-algebra, then f : A
is nilpotent on ฮบ(๐ญ) โ A
for some
prime ๐ญ โ R
if and only if every non-leading coefficient of charpoly(f)
is in ๐ญ
.
theorem
PrimeSpectrum.mem_image_comap_zeroLocus_sdiff
{R : Type u_2}
{A : Type u_1}
[CommRing R]
[CommRing A]
[Algebra R A]
(f : A)
(s : Set A)
(x : PrimeSpectrum R)
:
Let A
be an R
-algebra.
๐ญ : Spec R
is in the image of Z(I) โฉ D(f) โ Spec S
if and only if f
is not nilpotent on ฮบ(๐ญ) โ A โงธ I
.
theorem
PrimeSpectrum.mem_image_comap_basicOpen
{R : Type u_1}
{A : Type u_2}
[CommRing R]
[CommRing A]
[Algebra R A]
(f : A)
(x : PrimeSpectrum R)
:
Let A
be an R
-algebra.
๐ญ : Spec R
is in the image of D(f) โ Spec S
if and only if f
is not nilpotent on ฮบ(๐ญ) โ A
.
theorem
PrimeSpectrum.exists_image_comap_of_finite_of_free
{R : Type u_2}
{A : Type u_1}
[CommRing R]
[CommRing A]
[Algebra R A]
(f : A)
(s : Set A)
[Module.Finite R (A โงธ Ideal.span s)]
[Module.Free R (A โงธ Ideal.span s)]
:
Let A
be an R
-algebra. If A โงธ I
is finite free over R
,
then the image of Z(I) โฉ D(f) โ Spec S
in Spec R
is compact open.
theorem
Polynomial.mem_image_comap_C_basicOpen
{R : Type u_1}
[CommRing R]
(f : Polynomial R)
(x : PrimeSpectrum R)
:
theorem
MvPolynomial.mem_image_comap_C_basicOpen
{R : Type u_2}
[CommRing R]
{ฯ : Type u_1}
(f : MvPolynomial ฯ R)
(x : PrimeSpectrum R)
: