The weak Nullstellensatz

Let K be an algebraically closed extension of a field k and σ a finite type. An ideal of k[X_σ] whose polynomials have no common zero in K^σ is the unit ideal. This is the weak form of Hilbert's Nullstellensatz, read off from Mathlib's strong form MvPolynomial.vanishingIdeal_zeroLocus_eq_radical: the vanishing ideal of the empty set is the unit ideal, so an ideal with empty zero locus has unit radical. It is the form in which a polynomial condition checked at the points of K^σ gives an identity in k[X_σ].

Main results

• MvPolynomial.zeroLocus_eq_empty_iff: an ideal of k[X_σ] has no zero in K^σ exactly when it is the unit ideal.
• MvPolynomial.span_eq_top_iff_forall_exists_aeval_ne_zero: a set of polynomials generates the unit ideal exactly when they have no common zero in K^σ.

theorem MvPolynomial.zeroLocus_eq_empty_iff {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] [IsAlgClosed K] [Finite σ] {I : Ideal (MvPolynomial σ k)} : zeroLocus K I = ∅ ↔ I = ⊤

The weak Nullstellensatz: for an algebraically closed extension K of k, an ideal of k[X_σ] has no zero in K^σ exactly when it is the unit ideal.

theorem MvPolynomial.span_eq_top_iff_forall_exists_aeval_ne_zero {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] [IsAlgClosed K] [Finite σ] {S : Set (MvPolynomial σ k)} : Ideal.span S = ⊤ ↔ ∀ (x : σ → K), ∃ p ∈ S, (aeval x) p ≠ 0

The weak Nullstellensatz for generators: for an algebraically closed extension K of k, polynomials in k[X_σ] generate the unit ideal exactly when they have no common zero in K^σ.