Reductions for Rückert's Nullstellensatz, and the failure over ℝ

Three pieces of elementary algebra on the zero sets and vanishing ideals of ZeroSet.lean, used by the proof of Rückert's Nullstellensatz (Nullstellensatz.lean):

• Reduction to prime ideals (the first step of the proof of [Fre17, Ch. I, 9.1]: a proper radical ideal in a Noetherian ring is a finite intersection of primes, so the Nullstellensatz for prime ideals gives it for all radical ideals): with Mathlib's Ideal.sInf_minimalPrimes (√I is the intersection of the minimal primes over I, no finiteness needed) and the monotonicity of vanishingIdeal, the inclusion 𝓘(V(p)) ⊆ p for every prime p gives 𝓘(V(I)) = √I for every ideal I (vanishingIdeal_eq_radical_of_forall_isPrime); the pointwise form of the statement follows (mem_radical_of_vanishesOn_of_eq).
• Invariance under linear changes of coordinates (the "suitable linear transformation of the coordinates" of [Fre17, Ch. I, 7.4]; the automorphism P(z) ↦ P(Az) is substEquiv of Subst.lean): V(σ(S)) = L⁻¹(V(S)) near 0 because evalSeries (substConv L g) = evalSeries g ∘ L near 0 (evalSeries_substConv) and L is a homeomorphism fixing 0; hence σ f ∈ 𝓘(V(σ(I))) iff f ∈ 𝓘(V(I)), and the Nullstellensatz inclusion for σ(I) gives it for I (vanishingIdeal_le_radical_of_map_substEquiv; Mathlib's Ideal.map_radical_of_surjective).
• The failure over ℝ: V(x² + y²) = {0} but x ∉ √(x² + y²) (the same phenomenon as in [BM97, Example 3.16]): in Conv ℝ 2, x vanishes on the zero set of x² + y² near 0 (over ℝ, x² + y² = 0 forces x = 0), while x^k ∈ (x² + y²) would make x² + y² a divisor of a power of the prime x (prime_convX), hence a unit or divisible by x; neither is the case (constant coefficient 0; coefficient of y² equal to 1).

Reduction to prime ideals

theorem Analytic.vanishingIdeal_le_radical_of_minimalPrimes {K : Type u_1} [RCLike K] {n : ℕ} {I : Ideal ↥(Conv K n)} (h : ∀ p ∈ I.minimalPrimes, vanishingIdeal p ≤ p) : vanishingIdeal I ≤ I.radical

If 𝓘(V(p)) ⊆ p for every minimal prime p over I, then 𝓘(V(I)) ⊆ √I: √I is the intersection of its minimal primes and 𝓘(V(·)) is monotone.

theorem Analytic.vanishingIdeal_eq_radical_of_forall_isPrime {K : Type u_1} [RCLike K] {n : ℕ} (h : ∀ (P : Ideal ↥(Conv K n)), P.IsPrime → vanishingIdeal P ≤ P) (I : Ideal ↥(Conv K n)) : vanishingIdeal I = I.radical

The Nullstellensatz for prime ideals (𝓘(V(P)) ⊆ P) gives 𝓘(V(I)) = √I for every ideal (the reduction step of [Fre17, Ch. I, 9.1]).

theorem Analytic.mem_radical_of_vanishesOn_of_eq {K : Type u_1} [RCLike K] {n : ℕ} {S : Finset ↥(Conv K n)} {f : ↥(Conv K n)} (h : vanishingIdeal (Ideal.span ↑S) = (Ideal.span ↑S).radical) (hf : VanishesOn S f) : f ∈ (Ideal.span ↑S).radical

The pointwise form from the ideal-theoretic one: a series vanishing near 0 on the zero set of a finite system of generators of I lies in √I.

Invariance under linear changes of coordinates

theorem Analytic.map_nhds_zero_clequiv {K : Type u_1} [RCLike K] {n : ℕ} (L : (Fin n → K) ≃L[K] Fin n → K) : Filter.map (⇑L) (nhds 0) = nhds 0

A continuous linear automorphism of K^n carries the neighbourhood filter of 0 to itself.

theorem Analytic.vanishesOn_image_substEquiv {K : Type u_1} [RCLike K] {n : ℕ} [DecidableEq ↥(Conv K n)] (L : (Fin n → K) ≃L[K] Fin n → K) (S : Finset ↥(Conv K n)) (f : ↥(Conv K n)) : VanishesOn (Finset.image (⇑(substEquiv L)) S) ((substEquiv L) f) ↔ VanishesOn S f

V(σ(S)) = L⁻¹(V(S)) near 0 for σ = substEquiv L, so σ f vanishes on V(σ(S)) iff f vanishes on V(S).

theorem Analytic.mem_vanishingIdeal_map_substEquiv {K : Type u_1} [RCLike K] {n : ℕ} (L : (Fin n → K) ≃L[K] Fin n → K) (I : Ideal ↥(Conv K n)) (f : ↥(Conv K n)) : (substEquiv L) f ∈ vanishingIdeal (Ideal.map (↑(substEquiv L).toRingEquiv) I) ↔ f ∈ vanishingIdeal I

σ f ∈ 𝓘(V(σ(I))) iff f ∈ 𝓘(V(I)) for a linear change σ.

theorem Analytic.vanishingIdeal_le_radical_of_map_substEquiv {K : Type u_1} [RCLike K] {n : ℕ} (L : (Fin n → K) ≃L[K] Fin n → K) {I : Ideal ↥(Conv K n)} (h : vanishingIdeal (Ideal.map (↑(substEquiv L).toRingEquiv) I) ≤ (Ideal.map (↑(substEquiv L).toRingEquiv) I).radical) : vanishingIdeal I ≤ I.radical

The Nullstellensatz inclusion for the image σ(I) under a linear change of coordinates gives it for I (the linear transformation of the coordinates of [Fre17, Ch. I, 7.4]).

The failure over ℝ

theorem Analytic.not_nullstellensatz_real : convX ℝ 0 ∈ vanishingIdeal (Ideal.span {convX ℝ 0 ^ 2 + convX ℝ 1 ^ 2}) ∧ convX ℝ 0 ∉ (Ideal.span {convX ℝ 0 ^ 2 + convX ℝ 1 ^ 2}).radical

The failure of the Nullstellensatz over ℝ: in Conv ℝ 2, x vanishes on the zero-set germ of (x² + y²) (which is {0}) but is not in its radical (the same phenomenon as in [BM97, Example 3.16]).