# mathlibdocumentation

ring_theory.nullstellensatz

# 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 k)) :
set (σ → k)

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

Equations
• = {x : σ → k | ∀ (p : k), p I p = 0}
@[simp]
theorem mv_polynomial.mem_zero_locus_iff {k : Type u_1} [field k] {σ : Type u_2} {I : ideal k)} {x : σ → k} :
∀ (p : k), p I p = 0
theorem mv_polynomial.zero_locus_anti_mono {k : Type u_1} [field k] {σ : Type u_2} {I J : ideal 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

Equations
Instances for mv_polynomial.vanishing_ideal
@[simp]
theorem mv_polynomial.mem_vanishing_ideal_iff {k : Type u_1} [field k] {σ : Type u_2} {V : set (σ → k)} {p : k} :
∀ (x : σ → k), x V 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.vanishing_ideal_empty {k : Type u_1} [field k] {σ : Type u_2} :
theorem mv_polynomial.le_vanishing_ideal_zero_locus {k : Type u_1} [field k] {σ : Type u_2} (I : ideal k)) :
theorem mv_polynomial.zero_locus_vanishing_ideal_le {k : Type u_1} [field k] {σ : Type u_2} (V : set (σ → k)) :
theorem mv_polynomial.zero_locus_vanishing_ideal_galois_connection {k : Type u_1} [field k] {σ : Type u_2} :
theorem mv_polynomial.mem_vanishing_ideal_singleton_iff {k : Type u_1} [field k] {σ : Type u_2} (x : σ → k) (p : k) :
p = 0
@[protected, instance]
def mv_polynomial.vanishing_ideal_singleton_is_maximal {k : Type u_1} [field k] {σ : Type u_2} {x : σ → k} :
theorem mv_polynomial.radical_le_vanishing_ideal_zero_locus {k : Type u_1} [field k] {σ : Type u_2} (I : ideal 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

Equations
@[simp]
theorem mv_polynomial.vanishing_ideal_point_to_point {k : Type u_1} [field k] {σ : Type u_2} (V : set (σ → k)) :
theorem mv_polynomial.point_to_point_zero_locus_le {k : Type u_1} [field k] {σ : Type u_2} (I : ideal k)) :
theorem mv_polynomial.is_maximal_iff_eq_vanishing_ideal_singleton {k : Type u_1} [field k] {σ : Type u_2} [fintype σ] (I : ideal k)) :
I.is_maximal ∃ (x : σ → k),
@[simp]
theorem mv_polynomial.vanishing_ideal_zero_locus_eq_radical {k : Type u_1} [field k] {σ : Type u_2} [fintype σ] (I : ideal k)) :

Main statement of the Nullstellensatz

@[simp]
theorem mv_polynomial.is_prime.vanishing_ideal_zero_locus {k : Type u_1} [field k] {σ : Type u_2} [fintype σ] (P : ideal k)) [h : P.is_prime] :