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} (K : Type u_2) [Field k] [Field K] [Algebra k K] {σ : Type u_3} (I : Ideal (MvPolynomial σ k)) : Set (σ → K)

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

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

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

theorem MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {σ : Type u_3} : GaloisConnection (zeroLocus K) (vanishingIdeal k)

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

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

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

instance MvPolynomial.instIsPrimeVanishingIdealSingletonForallSet {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {σ : Type u_3} {x : σ → K} : (vanishingIdeal k {x}).IsPrime

instance MvPolynomial.instIsMaximalVanishingIdealSingletonForallSet {K : Type u_2} [Field K] {σ : Type u_3} {x : σ → K} : (vanishingIdeal K {x}).IsMaximal

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

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

The point in the prime spectrum associated to a given point

@[simp]

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

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

theorem MvPolynomial.eq_vanishingIdeal_singleton_of_isMaximal {k : Type u_1} (K : Type u_2) [Field k] [Field K] [Algebra k K] {σ : Type u_3} [IsAlgClosed K] [Finite σ] {I : Ideal (MvPolynomial σ k)} (hI : I.IsMaximal) : ∃ (x : σ → K), I = vanishingIdeal k {x}

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

@[simp]

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

Main statement of the Nullstellensatz

@[simp]

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