Nullstellensatz

This file establishes a version of Hilbert's classical Nullstellensatz for MvPolynomials. The main statement of the theorem is MvPolynomial.vanishingIdeal_zeroLocus_eq_radical.

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

def MvPolynomial.zeroLocus {k : Type u_1} [Field k] {σ : Type u_2} (I : Ideal (MvPolynomial σ k)) : Set (σ → k)

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

Equations

• MvPolynomial.zeroLocus I = {x : σ → k | ∀ p ∈ I, (MvPolynomial.eval x) p = 0}

@[simp]

theorem MvPolynomial.mem_zeroLocus_iff {k : Type u_1} [Field k] {σ : Type u_2} {I : Ideal (MvPolynomial σ k)} {x : σ → k} : x ∈ zeroLocus I ↔ ∀ p ∈ I, (eval x) p = 0

theorem MvPolynomial.zeroLocus_anti_mono {k : Type u_1} [Field k] {σ : Type u_2} {I J : Ideal (MvPolynomial σ k)} (h : I ≤ J) : zeroLocus J ≤ zeroLocus I

@[simp]

theorem MvPolynomial.zeroLocus_bot {k : Type u_1} [Field k] {σ : Type u_2} : zeroLocus ⊥ = ⊤

@[simp]

theorem MvPolynomial.zeroLocus_top {k : Type u_1} [Field k] {σ : Type u_2} : zeroLocus ⊤ = ⊥

def MvPolynomial.vanishingIdeal {k : Type u_1} [Field k] {σ : Type u_2} (V : Set (σ → k)) : Ideal (MvPolynomial σ k)

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

Equations

• MvPolynomial.vanishingIdeal V = { carrier := {p : MvPolynomial σ k | ∀ x ∈ V, (MvPolynomial.eval x) p = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem MvPolynomial.mem_vanishingIdeal_iff {k : Type u_1} [Field k] {σ : Type u_2} {V : Set (σ → k)} {p : MvPolynomial σ k} : p ∈ vanishingIdeal V ↔ ∀ x ∈ V, (eval x) p = 0

theorem MvPolynomial.vanishingIdeal_anti_mono {k : Type u_1} [Field k] {σ : Type u_2} {A B : Set (σ → k)} (h : A ≤ B) : vanishingIdeal B ≤ vanishingIdeal A

theorem MvPolynomial.vanishingIdeal_empty {k : Type u_1} [Field k] {σ : Type u_2} : vanishingIdeal ∅ = ⊤

theorem MvPolynomial.le_vanishingIdeal_zeroLocus {k : Type u_1} [Field k] {σ : Type u_2} (I : Ideal (MvPolynomial σ k)) : I ≤ vanishingIdeal (zeroLocus I)

theorem MvPolynomial.zeroLocus_vanishingIdeal_le {k : Type u_1} [Field k] {σ : Type u_2} (V : Set (σ → k)) : V ≤ zeroLocus (vanishingIdeal V)

theorem MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection {k : Type u_1} [Field k] {σ : Type u_2} : GaloisConnection zeroLocus vanishingIdeal

theorem MvPolynomial.le_zeroLocus_iff_le_vanishingIdeal {k : Type u_1} [Field k] {σ : Type u_2} {V : Set (σ → k)} {I : Ideal (MvPolynomial σ k)} : V ≤ zeroLocus I ↔ I ≤ vanishingIdeal V

theorem MvPolynomial.zeroLocus_span {k : Type u_1} [Field k] {σ : Type u_2} (S : Set (MvPolynomial σ k)) : zeroLocus (Ideal.span S) = {x : σ → k | ∀ p ∈ S, (eval x) p = 0}

theorem MvPolynomial.mem_vanishingIdeal_singleton_iff {k : Type u_1} [Field k] {σ : Type u_2} (x : σ → k) (p : MvPolynomial σ k) : p ∈ vanishingIdeal {x} ↔ (eval x) p = 0

instance MvPolynomial.vanishingIdeal_singleton_isMaximal {k : Type u_1} [Field k] {σ : Type u_2} {x : σ → k} : (vanishingIdeal {x}).IsMaximal

theorem MvPolynomial.radical_le_vanishingIdeal_zeroLocus {k : Type u_1} [Field k] {σ : Type u_2} (I : Ideal (MvPolynomial σ k)) : I.radical ≤ vanishingIdeal (zeroLocus I)

def MvPolynomial.pointToPoint {k : Type u_1} [Field k] {σ : Type u_2} (x : σ → k) : PrimeSpectrum (MvPolynomial σ k)

The point in the prime spectrum associated to a given point

Equations

• MvPolynomial.pointToPoint x = { asIdeal := MvPolynomial.vanishingIdeal {x}, isPrime := ⋯ }

@[simp]

theorem MvPolynomial.vanishingIdeal_pointToPoint {k : Type u_1} [Field k] {σ : Type u_2} (V : Set (σ → k)) : PrimeSpectrum.vanishingIdeal (pointToPoint '' V) = vanishingIdeal V

theorem MvPolynomial.pointToPoint_zeroLocus_le {k : Type u_1} [Field k] {σ : Type u_2} (I : Ideal (MvPolynomial σ k)) : pointToPoint '' zeroLocus I ≤ PrimeSpectrum.zeroLocus ↑I

theorem MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton {k : Type u_1} [Field k] {σ : Type u_2} [IsAlgClosed k] [Finite σ] (I : Ideal (MvPolynomial σ k)) : I.IsMaximal ↔ ∃ (x : σ → k), I = vanishingIdeal {x}

@[simp]

theorem MvPolynomial.vanishingIdeal_zeroLocus_eq_radical {k : Type u_1} [Field k] {σ : Type u_2} [IsAlgClosed k] [Finite σ] (I : Ideal (MvPolynomial σ k)) : vanishingIdeal (zeroLocus I) = I.radical

Main statement of the Nullstellensatz

@[simp]

theorem MvPolynomial.IsPrime.vanishingIdeal_zeroLocus {k : Type u_1} [Field k] {σ : Type u_2} [IsAlgClosed k] [Finite σ] (P : Ideal (MvPolynomial σ k)) [h : P.IsPrime] : vanishingIdeal (zeroLocus P) = P