# Documentation

Mathlib.RingTheory.Nullstellensatz

# 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} [] {σ : Type u_2} (I : Ideal ()) :
Set (σk)

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

Instances For
@[simp]
theorem MvPolynomial.mem_zeroLocus_iff {k : Type u_1} [] {σ : Type u_2} {I : Ideal ()} {x : σk} :
∀ (p : ), p I↑() p = 0
theorem MvPolynomial.zeroLocus_anti_mono {k : Type u_1} [] {σ : Type u_2} {I : Ideal ()} {J : Ideal ()} (h : I J) :
@[simp]
theorem MvPolynomial.zeroLocus_bot {k : Type u_1} [] {σ : Type u_2} :
@[simp]
theorem MvPolynomial.zeroLocus_top {k : Type u_1} [] {σ : Type u_2} :
def MvPolynomial.vanishingIdeal {k : Type u_1} [] {σ : Type u_2} (V : Set (σk)) :

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

Instances For
@[simp]
theorem MvPolynomial.mem_vanishingIdeal_iff {k : Type u_1} [] {σ : Type u_2} {V : Set (σk)} {p : } :
∀ (x : σk), x V↑() p = 0
theorem MvPolynomial.vanishingIdeal_anti_mono {k : Type u_1} [] {σ : Type u_2} {A : Set (σk)} {B : Set (σk)} (h : A B) :
theorem MvPolynomial.vanishingIdeal_empty {k : Type u_1} [] {σ : Type u_2} :
theorem MvPolynomial.le_vanishingIdeal_zeroLocus {k : Type u_1} [] {σ : Type u_2} (I : Ideal ()) :
theorem MvPolynomial.zeroLocus_vanishingIdeal_le {k : Type u_1} [] {σ : Type u_2} (V : Set (σk)) :
theorem MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection {k : Type u_1} [] {σ : Type u_2} :
GaloisConnection MvPolynomial.zeroLocus MvPolynomial.vanishingIdeal
theorem MvPolynomial.le_zeroLocus_iff_le_vanishingIdeal {k : Type u_1} [] {σ : Type u_2} {V : Set (σk)} {I : Ideal ()} :
theorem MvPolynomial.zeroLocus_span {k : Type u_1} [] {σ : Type u_2} (S : Set ()) :
= {x | ∀ (p : ), p S↑() p = 0}
theorem MvPolynomial.mem_vanishingIdeal_singleton_iff {k : Type u_1} [] {σ : Type u_2} (x : σk) (p : ) :
↑() p = 0
instance MvPolynomial.vanishingIdeal_singleton_isMaximal {k : Type u_1} [] {σ : Type u_2} {x : σk} :
theorem MvPolynomial.radical_le_vanishingIdeal_zeroLocus {k : Type u_1} [] {σ : Type u_2} (I : Ideal ()) :
def MvPolynomial.pointToPoint {k : Type u_1} [] {σ : Type u_2} (x : σk) :

The point in the prime spectrum associated to a given point

Instances For
@[simp]
theorem MvPolynomial.vanishingIdeal_pointToPoint {k : Type u_1} [] {σ : Type u_2} (V : Set (σk)) :
PrimeSpectrum.vanishingIdeal (MvPolynomial.pointToPoint '' V) =
theorem MvPolynomial.pointToPoint_zeroLocus_le {k : Type u_1} [] {σ : Type u_2} (I : Ideal ()) :
MvPolynomial.pointToPoint ''
theorem MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton {k : Type u_1} [] {σ : Type u_2} [] [] (I : Ideal ()) :
x,
@[simp]
theorem MvPolynomial.vanishingIdeal_zeroLocus_eq_radical {k : Type u_1} [] {σ : Type u_2} [] [] (I : Ideal ()) :

Main statement of the Nullstellensatz

@[simp]
theorem MvPolynomial.IsPrime.vanishingIdeal_zeroLocus {k : Type u_1} [] {σ : Type u_2} [] [] (P : Ideal ()) [h : ] :