Documentation

Mathlib.RingTheory.Spectrum.Prime.Polynomial

Prime spectrum of (multivariate) polynomials #

Also see AlgebraicGeometry/AffineSpace for the affine space over arbitrary schemes.

Main results #

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 ๐”ญ.

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.

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.

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.