Prime spectrum of (multivariate) polynomials

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

Main results

• isNilpotent_tensor_residueField_iff: 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 𝔭.
• Polynomial.exists_image_comap_of_monic: If g : R[X] is monic, the image of Z(g) ∩ D(f) : Spec R[X] in Spec R is compact open.
• Polynomial.isOpenMap_comap_C: The structure map Spec R[X] → Spec R is an open map.
• MvPolynomial.isOpenMap_comap_C: The structure map Spec 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] : IsNilpotent ((algebraMap A (TensorProduct R A I.ResidueField)) f) ↔ ∀ i < Module.finrank R A, (LinearMap.charpoly ((Algebra.lmul R A) f)).coeff i ∈ I

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) : x ∈ ⇑(PrimeSpectrum.comap (algebraMap R A)) '' (PrimeSpectrum.zeroLocus s \ PrimeSpectrum.zeroLocus {f}) ↔ ¬IsNilpotent ((algebraMap A (TensorProduct R (A ⧸ Ideal.span s) x.asIdeal.ResidueField)) f)

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) : x ∈ ⇑(PrimeSpectrum.comap (algebraMap R A)) '' ↑(PrimeSpectrum.basicOpen f) ↔ ¬IsNilpotent ((algebraMap A (TensorProduct R A x.asIdeal.ResidueField)) f)

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)] : ∃ (t : Finset R), ⇑(PrimeSpectrum.comap (algebraMap R A)) '' (PrimeSpectrum.zeroLocus s \ PrimeSpectrum.zeroLocus {f}) = (PrimeSpectrum.zeroLocus ↑t)ᶜ

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) : x ∈ ⇑(PrimeSpectrum.comap Polynomial.C) '' ↑(PrimeSpectrum.basicOpen f) ↔ ∃ (i : ℕ), f.coeff i ∉ x.asIdeal

theorem Polynomial.image_comap_C_basicOpen {R : Type u_1} [CommRing R] (f : Polynomial R) : ⇑(PrimeSpectrum.comap Polynomial.C) '' ↑(PrimeSpectrum.basicOpen f) = (PrimeSpectrum.zeroLocus (Set.range f.coeff))ᶜ

theorem Polynomial.isOpenMap_comap_C {R : Type u_1} [CommRing R] : IsOpenMap ⇑(PrimeSpectrum.comap Polynomial.C)

theorem Polynomial.exists_image_comap_of_monic {R : Type u_1} [CommRing R] (f g : Polynomial R) (hg : g.Monic) : ∃ (t : Finset R), ⇑(PrimeSpectrum.comap Polynomial.C) '' (PrimeSpectrum.zeroLocus {g} \ PrimeSpectrum.zeroLocus {f}) = (PrimeSpectrum.zeroLocus ↑t)ᶜ

theorem Polynomial.isCompact_image_comap_of_monic {R : Type u_1} [CommRing R] (f g : Polynomial R) (hg : g.Monic) : IsCompact (⇑(PrimeSpectrum.comap Polynomial.C) '' (PrimeSpectrum.zeroLocus {g} \ PrimeSpectrum.zeroLocus {f}))

theorem Polynomial.isOpen_image_comap_of_monic {R : Type u_1} [CommRing R] (f g : Polynomial R) (hg : g.Monic) : IsOpen (⇑(PrimeSpectrum.comap Polynomial.C) '' (PrimeSpectrum.zeroLocus {g} \ PrimeSpectrum.zeroLocus {f}))

theorem MvPolynomial.mem_image_comap_C_basicOpen {R : Type u_2} [CommRing R] {σ : Type u_1} (f : MvPolynomial σ R) (x : PrimeSpectrum R) : x ∈ ⇑(PrimeSpectrum.comap MvPolynomial.C) '' ↑(PrimeSpectrum.basicOpen f) ↔ ∃ (i : σ →₀ ℕ), MvPolynomial.coeff i f ∉ x.asIdeal

theorem MvPolynomial.image_comap_C_basicOpen {R : Type u_2} [CommRing R] {σ : Type u_1} (f : MvPolynomial σ R) : ⇑(PrimeSpectrum.comap MvPolynomial.C) '' ↑(PrimeSpectrum.basicOpen f) = (PrimeSpectrum.zeroLocus (Set.range fun (m : σ →₀ ℕ) => MvPolynomial.coeff m f))ᶜ

theorem MvPolynomial.isOpenMap_comap_C {R : Type u_2} [CommRing R] {σ : Type u_1} : IsOpenMap ⇑(PrimeSpectrum.comap MvPolynomial.C)