Nullstellensatz #
This file establishes a version of Hilbert's classical Nullstellensatz for mv_polynomial
s.
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.
Set of points that are zeroes of all polynomials in an ideal
Equations
- mv_polynomial.zero_locus I = {x : σ → k | ∀ (p : mv_polynomial σ k), p ∈ I → ⇑(mv_polynomial.eval x) p = 0}
Ideal of polynomials with common zeroes at all elements of a set
Equations
- mv_polynomial.vanishing_ideal V = {carrier := {p : mv_polynomial σ k | ∀ (x : σ → k), x ∈ V → ⇑(mv_polynomial.eval x) p = 0}, add_mem' := _, zero_mem' := _, smul_mem' := _}
Instances for mv_polynomial.vanishing_ideal
The point in the prime spectrum assosiated to a given point
Equations
Main statement of the Nullstellensatz