Nullstellensatz #

This file establishes a version of Hilbert's classical Nullstellensatz for MvPolynomials. The main statement of the theorem is MvPolynomial.vanishingIdeal_zeroLocus_eq_radical.

The statement is in terms of new definitions vanishingIdeal and zeroLocus. Mathlib already has versions of these in terms of the prime spectrum of a ring, but those are not well-suited for expressing this result. Suggestions for better ways to state this theorem or organize things are welcome.

The machinery around vanishingIdeal and zeroLocus is also minimal, I only added lemmas directly needed in this proof, since I'm not sure if they are the right approach.

def MvPolynomial.zeroLocus {k : Type u_1} [Field k] {σ : Type u_2} (I : Ideal (MvPolynomial σ k)) :
Set (σk)

Set of points that are zeroes of all polynomials in an ideal

Instances For
    theorem MvPolynomial.mem_zeroLocus_iff {k : Type u_1} [Field k] {σ : Type u_2} {I : Ideal (MvPolynomial σ k)} {x : σk} :
    x MvPolynomial.zeroLocus I ∀ (p : MvPolynomial σ k), p I↑(MvPolynomial.eval x) p = 0
    def MvPolynomial.vanishingIdeal {k : Type u_1} [Field k] {σ : Type u_2} (V : Set (σk)) :

    Ideal of polynomials with common zeroes at all elements of a set

    Instances For
      theorem MvPolynomial.mem_vanishingIdeal_iff {k : Type u_1} [Field k] {σ : Type u_2} {V : Set (σk)} {p : MvPolynomial σ k} :
      p MvPolynomial.vanishingIdeal V ∀ (x : σk), x V↑(MvPolynomial.eval x) p = 0
      theorem MvPolynomial.vanishingIdeal_anti_mono {k : Type u_1} [Field k] {σ : Type u_2} {A : Set (σk)} {B : Set (σk)} (h : A B) :
      theorem MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection {k : Type u_1} [Field k] {σ : Type u_2} :
      GaloisConnection MvPolynomial.zeroLocus MvPolynomial.vanishingIdeal
      theorem MvPolynomial.zeroLocus_span {k : Type u_1} [Field k] {σ : Type u_2} (S : Set (MvPolynomial σ k)) :
      MvPolynomial.zeroLocus (Ideal.span S) = {x | ∀ (p : MvPolynomial σ k), p S↑(MvPolynomial.eval x) p = 0}
      theorem MvPolynomial.mem_vanishingIdeal_singleton_iff {k : Type u_1} [Field k] {σ : Type u_2} (x : σk) (p : MvPolynomial σ k) :
      def MvPolynomial.pointToPoint {k : Type u_1} [Field k] {σ : Type u_2} (x : σk) :

      The point in the prime spectrum associated to a given point

      Instances For
        theorem MvPolynomial.vanishingIdeal_pointToPoint {k : Type u_1} [Field k] {σ : Type u_2} (V : Set (σk)) :
        theorem MvPolynomial.pointToPoint_zeroLocus_le {k : Type u_1} [Field k] {σ : Type u_2} (I : Ideal (MvPolynomial σ k)) :
        MvPolynomial.pointToPoint '' MvPolynomial.zeroLocus I PrimeSpectrum.zeroLocus I

        Main statement of the Nullstellensatz