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

Equations
• = {x : σk | pI, p = 0}
Instances For
@[simp]
theorem MvPolynomial.mem_zeroLocus_iff {k : Type u_1} [] {σ : Type u_2} {I : Ideal ()} {x : σk} :
pI, 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

Equations
• = { carrier := {p : | xV, p = 0}, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
@[simp]
theorem MvPolynomial.mem_vanishingIdeal_iff {k : Type u_1} [] {σ : Type u_2} {V : Set (σk)} {p : } :
xV, 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 : σk | pS, 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} :
.IsMaximal
Equations
• =
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

Equations
• = { asIdeal := , isPrime := }
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 ()) :
I.IsMaximal ∃ (x : σk),
@[simp]
theorem MvPolynomial.vanishingIdeal_zeroLocus_eq_radical {k : Type u_1} [] {σ : Type u_2} [] [] (I : Ideal ()) :