mathlib3 documentation


Nullstellensatz #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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} :
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

Instances for mv_polynomial.vanishing_ideal
theorem mv_polynomial.mem_vanishing_ideal_iff {k : Type u_1} [field k] {σ : Type u_2} {V : set k)} {p : mv_polynomial σ k} :
@[protected, instance]
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


Main statement of the Nullstellensatz