mathlib documentation


Nullstellensatz #

This file establishes a version of Hilbert's classical Nullstellensatz for mv_polynomials. The main statement of the theorem is vanishing_ideal_zero_locus_eq_radical.

The statement is in terms of new definitions vanishing_ideal and zero_locus. 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 vanishing_ideal and zero_locus is also minimal, I only added lemmas directly needed in this proof, since I'm not sure if they are the right approach.

def mv_polynomial.zero_locus {k : Type u_1} [field k] {σ : Type u_2} (I : ideal (mv_polynomial σ k)) :
set (σ → k)

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

theorem mv_polynomial.mem_zero_locus_iff {k : Type u_1} [field k] {σ : Type u_2} {I : ideal (mv_polynomial σ k)} {x : σ → k} :
theorem mv_polynomial.zero_locus_anti_mono {k : Type u_1} [field k] {σ : Type u_2} {I J : ideal (mv_polynomial σ k)} (h : I J) :
theorem mv_polynomial.zero_locus_bot {k : Type u_1} [field k] {σ : Type u_2} :
theorem mv_polynomial.zero_locus_top {k : Type u_1} [field k] {σ : Type u_2} :
def mv_polynomial.vanishing_ideal {k : Type u_1} [field k] {σ : Type u_2} (V : set (σ → k)) :

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

theorem mv_polynomial.mem_vanishing_ideal_iff {k : Type u_1} [field k] {σ : Type u_2} {V : set (σ → k)} {p : mv_polynomial σ k} :
p mv_polynomial.vanishing_ideal V ∀ (x : σ → k), x V(mv_polynomial.eval x) p = 0
theorem mv_polynomial.vanishing_ideal_anti_mono {k : Type u_1} [field k] {σ : Type u_2} {A B : set (σ → k)} (h : A B) :
theorem mv_polynomial.zero_locus_vanishing_ideal_le {k : Type u_1} [field k] {σ : Type u_2} (V : set (σ → k)) :
theorem mv_polynomial.mem_vanishing_ideal_singleton_iff {k : Type u_1} [field k] {σ : Type u_2} (x : σ → k) (p : mv_polynomial σ k) :
def mv_polynomial.vanishing_ideal_singleton_is_maximal {k : Type u_1} [field k] {σ : Type u_2} {x : σ → k} :
def mv_polynomial.point_to_point {k : Type u_1} [field k] {σ : Type u_2} (x : σ → k) :

The point in the prime spectrum assosiated to a given point

theorem mv_polynomial.is_maximal_iff_eq_vanishing_ideal_singleton {k : Type u_1} [field k] {σ : Type u_2} [is_alg_closed k] [fintype σ] (I : ideal (mv_polynomial σ k)) :
I.is_maximal ∃ (x : σ → k), I = mv_polynomial.vanishing_ideal {x}

Main statement of the Nullstellensatz