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} :
    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} :
      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 : σk | pS, (MvPolynomial.eval x) p = 0}
      instance MvPolynomial.vanishingIdeal_singleton_isMaximal {k : Type u_1} [Field k] {σ : Type u_2} {x : σ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
        theorem MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton {k : Type u_1} [Field k] {σ : Type u_2} [IsAlgClosed k] [Finite σ] (I : Ideal (MvPolynomial σ k)) :
        I.IsMaximal ∃ (x : σk), I = MvPolynomial.vanishingIdeal {x}

        Main statement of the Nullstellensatz