Rückert's Nullstellensatz over ℂ

For an ideal I of the germ ring 𝒪_n = ℂ{x_1, …, x_n}, 𝓘(V(I)) = √I (vanishingIdeal_eq_radical), and a series vanishing near 0 on the common zero set of a finite system of generators of I lies in √I (mem_radical_of_vanishesOn). The proof follows [Fre17, Ch. I, Theorem 9.1], by induction on the number of variables:

• n = 0: 𝒪_0 = ℂ, whose ideals are ⊥ and ⊤ (vanishingIdeal_eq_radical_conv_zero).
• The reduction to prime ideals (every proper radical ideal in a Noetherian ring is the intersection of finitely many primes) is NullstellensatzReduction.lean (vanishingIdeal_eq_radical_of_forall_isPrime, Mathlib's Ideal.sInf_minimalPrimes).
• A prime P ⊆ 𝒪_{m+1}: a linear change of coordinates makes a nonzero element of P regular in x_0 (exists_substEquiv_isRegularIn, Subst.lean; the statement is invariant, vanishingIdeal_le_radical_of_map_substEquiv), and the preparation theorem puts the series of a Weierstrass polynomial into P (vanishingIdeal_le_of_isPrime). Freitag's two alternatives (vanishingIdeal_le_of_isPrime_of_weierstrass_mem): a principal P = (Q) is the hypersurface case [Fre17, Ch. I, 5.1] (Hypersurface.lean, vanishingIdeal_span_singleton_le_of_prime); otherwise, for f ∈ 𝓘(V(P)), Lemma 7.1 (finite_mk_comp_convTail, NoetherNormalization.lean) makes f integral over 𝒪_m modulo P, and a monic relation q(f) ∈ P of minimal degree is examined as in the proof of 9.1: if the constant term q_0 ∈ 𝔭 = P ∩ 𝒪_m then f · q'(f) ∈ P with q' monic of smaller degree, so f ∈ P by primality and minimality; if q_0 ∉ 𝔭, the parametrization lemma (Parametrization.lean) gives A ∉ 𝔭 and, over the points y ∈ V(𝔭) near 0 with A(y) ≠ 0, points (t, y) ∈ V(P) near 0; there f(t, y) = 0 and q(f)(t, y) = 0, so q_0(y) = 0 (evalSeries_eval₂_convTail_eventually): A q_0 ∈ 𝓘(V(𝔭)) = 𝔭 by the induction hypothesis, hence q_0 ∈ 𝔭 (𝔭 prime, A ∉ 𝔭), a contradiction.

Followed from [Fre17]: 5.1, 7.1, the mechanism of 8.3, and 9.1 (reduction, case split, minimal integral equation, A q_0 ∈ 𝓘(V(𝔭)) = 𝔭). Replaced: 7.3, 7.4 and 8.2, by the argument over a principal ideal domain of Parametrization.lean. The failure of the statement over ℝ (not_nullstellensatz_real) is in NullstellensatzReduction.lean. The Nullstellensatz is what identifies the vanishing ideal of an irreducible germ with its prime; the Nullstellensatz for analytic spaces (Hironaka/AnalyticSpace/Nullstellensatz.lean) applies it to the stalks.

theorem Analytic.vanishingIdeal_eq_radical_conv_zero (I : Ideal ↥(Conv ℂ 0)) : vanishingIdeal I = I.radical

The base case n = 0: 𝒪_0 = ℂ, whose ideals are ⊥ and ⊤.

theorem Analytic.evalSeries_eval₂_convTail_eventually {m : ℕ} (q : Polynomial ↥(Conv ℂ m)) (f : ↥(Conv ℂ (m + 1))) : evalSeries ↑(Polynomial.eval₂ (convTail ℂ).toRingHom f q) =ᶠ[nhds 0] fun (z : Fin (m + 1) → ℂ) => ∑ i ∈ Finset.range (q.natDegree + 1), evalSeries (↑(q.coeff i)) (Fin.tail z) * evalSeries (↑f) z ^ i

Near 0, the series q(f) (q ∈ 𝒪_m[T] evaluated at f ∈ 𝒪_{m+1}) evaluates as ∑ q_i(x') f(x)^i.

theorem Analytic.vanishingIdeal_le_of_isPrime_of_weierstrass_mem {m : ℕ} (ih : ∀ (I : Ideal ↥(Conv ℂ m)), vanishingIdeal I = I.radical) {P : Ideal ↥(Conv ℂ (m + 1))} [hP : P.IsPrime] {d : ℕ} {c : Fin d → ↥(Conv ℂ m)} (hc : ∀ (j : Fin d), MvPowerSeries.constantCoeff ↑(c j) = 0) (hW : (convPolyEval ℂ) (weierstrassPolynomial d c) ∈ P) : vanishingIdeal P ≤ P

The prime case of [Fre17, Ch. I, 9.1] for a prime ideal containing the series of a Weierstrass polynomial in x_0, given the Nullstellensatz in m variables: 𝓘(V(P)) ⊆ P. Freitag's case split is kept: a principal P is the first alternative ([Fre17, Ch. I, 5.1], vanishingIdeal_span_singleton_le_of_prime); otherwise the minimal integral equation of a series f ∈ 𝓘(V(P)) over 𝒪_m modulo P (Lemma 7.1, finite_mk_comp_convTail) and the parametrization lemma give f ∈ P.

theorem Analytic.vanishingIdeal_le_of_isPrime {m : ℕ} (ih : ∀ (I : Ideal ↥(Conv ℂ m)), vanishingIdeal I = I.radical) (P : Ideal ↥(Conv ℂ (m + 1))) [hP : P.IsPrime] : vanishingIdeal P ≤ P

The induction step: the Nullstellensatz in m variables gives 𝓘(V(P)) ⊆ P for every prime P ⊆ 𝒪_{m+1}: a linear change of coordinates makes a nonzero element of P regular in x_0 (exists_substEquiv_isRegularIn), the preparation theorem puts the series of a Weierstrass polynomial into the image ideal, and the statement is invariant under the change (vanishingIdeal_le_radical_of_map_substEquiv).

theorem Analytic.vanishingIdeal_eq_radical (n : ℕ) (I : Ideal ↥(Conv ℂ n)) : vanishingIdeal I = I.radical

Rückert's Nullstellensatz over ℂ [Fre17, Ch. I, Theorem 9.1]: 𝓘(V(I)) = √I for every ideal I of 𝒪_n, by induction on the number of variables.

theorem Analytic.mem_radical_of_vanishesOn {n : ℕ} {S : Finset ↥(Conv ℂ n)} {f : ↥(Conv ℂ n)} (hf : VanishesOn S f) : f ∈ (Ideal.span ↑S).radical

The pointwise form: a series vanishing near 0 on the common zero set of a finite system of generators of I lies in √I.