mathlib3 documentation

ring_theory.nullstellensatz

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

Equations

mv_polynomial.zero_locus I = {x : σ → k | ∀ (p : mv_polynomial σ k), p ∈ I → ⇑(mv_polynomial.eval x) p = 0}

@[simp]

theorem mv_polynomial.mem_zero_locus_iff {k : Type u_1} [field k] {σ : Type u_2} {I : ideal (mv_polynomial σ k)} {x : σ → k} :

x ∈ mv_polynomial.zero_locus I ↔ ∀ (p : mv_polynomial σ k), p ∈ I → ⇑(mv_polynomial.eval x) p = 0

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) :

mv_polynomial.zero_locus J ≤ mv_polynomial.zero_locus I

theorem mv_polynomial.zero_locus_bot {k : Type u_1} [field k] {σ : Type u_2} :

mv_polynomial.zero_locus ⊥ = ⊤

theorem mv_polynomial.zero_locus_top {k : Type u_1} [field k] {σ : Type u_2} :

mv_polynomial.zero_locus ⊤ = ⊥

def mv_polynomial.vanishing_ideal {k : Type u_1} [field k] {σ : Type u_2} (V : set (σ → k)) :

ideal (mv_polynomial σ k)

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

mv_polynomial.vanishing_ideal_singleton_is_maximal

@[simp]

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) :

mv_polynomial.vanishing_ideal B ≤ mv_polynomial.vanishing_ideal A

theorem mv_polynomial.vanishing_ideal_empty {k : Type u_1} [field k] {σ : Type u_2} :

mv_polynomial.vanishing_ideal ∅ = ⊤

theorem mv_polynomial.le_vanishing_ideal_zero_locus {k : Type u_1} [field k] {σ : Type u_2} (I : ideal (mv_polynomial σ k)) :

I ≤ mv_polynomial.vanishing_ideal (mv_polynomial.zero_locus I)

theorem mv_polynomial.zero_locus_vanishing_ideal_le {k : Type u_1} [field k] {σ : Type u_2} (V : set (σ → k)) :

V ≤ mv_polynomial.zero_locus (mv_polynomial.vanishing_ideal V)

theorem mv_polynomial.zero_locus_vanishing_ideal_galois_connection {k : Type u_1} [field k] {σ : Type u_2} :

galois_connection mv_polynomial.zero_locus mv_polynomial.vanishing_ideal

theorem mv_polynomial.mem_vanishing_ideal_singleton_iff {k : Type u_1} [field k] {σ : Type u_2} (x : σ → k) (p : mv_polynomial σ k) :

p ∈ mv_polynomial.vanishing_ideal {x} ↔ ⇑(mv_polynomial.eval x) p = 0

@[protected, instance]

def mv_polynomial.vanishing_ideal_singleton_is_maximal {k : Type u_1} [field k] {σ : Type u_2} {x : σ → k} :

(mv_polynomial.vanishing_ideal {x}).is_maximal

theorem mv_polynomial.radical_le_vanishing_ideal_zero_locus {k : Type u_1} [field k] {σ : Type u_2} (I : ideal (mv_polynomial σ k)) :

I.radical ≤ mv_polynomial.vanishing_ideal (mv_polynomial.zero_locus I)

def mv_polynomial.point_to_point {k : Type u_1} [field k] {σ : Type u_2} (x : σ → k) :

prime_spectrum (mv_polynomial σ k)

The point in the prime spectrum assosiated to a given point

Equations

mv_polynomial.point_to_point x = {as_ideal := mv_polynomial.vanishing_ideal {x}, is_prime := _}

@[simp]

theorem mv_polynomial.vanishing_ideal_point_to_point {k : Type u_1} [field k] {σ : Type u_2} (V : set (σ → k)) :

prime_spectrum.vanishing_ideal (mv_polynomial.point_to_point '' V) = mv_polynomial.vanishing_ideal V

theorem mv_polynomial.point_to_point_zero_locus_le {k : Type u_1} [field k] {σ : Type u_2} (I : ideal (mv_polynomial σ k)) :

mv_polynomial.point_to_point '' mv_polynomial.zero_locus I ≤ prime_spectrum.zero_locus ↑I

theorem mv_polynomial.is_maximal_iff_eq_vanishing_ideal_singleton {k : Type u_1} [field k] {σ : Type u_2} [is_alg_closed k] [finite σ] (I : ideal (mv_polynomial σ k)) :

I.is_maximal ↔ ∃ (x : σ → k), I = mv_polynomial.vanishing_ideal {x}

@[simp]

theorem mv_polynomial.vanishing_ideal_zero_locus_eq_radical {k : Type u_1} [field k] {σ : Type u_2} [is_alg_closed k] [finite σ] (I : ideal (mv_polynomial σ k)) :

mv_polynomial.vanishing_ideal (mv_polynomial.zero_locus I) = I.radical

Main statement of the Nullstellensatz

@[simp]

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

mv_polynomial.vanishing_ideal (mv_polynomial.zero_locus P) = P