Hypersurfaces: zeros of a square-free series

The hypersurface case of Rückert's Nullstellensatz [Fre17, Ch. I, 5.1], in its square-free form over ℂ: if every zero of the nonzero square-free series Q ∈ 𝒪_{m+1} near 0 is a zero of P, then Q ∣ P (dvd_of_eventually_of_squarefree). For a prime Q this is the first case of the Nullstellensatz (Nullstellensatz.lean): a series vanishing on the zero-set germ of (Q) lies in (Q) (dvd_of_vanishesOn_of_prime, vanishingIdeal_span_singleton_le_of_prime).

The proof follows Freitag's, with two replacements by Mathlib results:

• Freitag first reduces to the case where Q is a Weierstrass polynomial: a linear change of coordinates makes Q regular in x_0 (exists_substEquiv_isRegularIn, Subst.lean; the hypothesis and the conclusion are invariant, vanishesOn_image_substEquiv, squarefree_map_mulEquiv_iff, map_dvd_iff), and the preparation theorem writes Q = u W with u a unit and W the series of a Weierstrass polynomial W_p ∈ 𝒪_m[x_0] of degree d (exists_preparation_conv); u does not vanish near 0, so V(Q) = V(W) near 0, and W is square-free with Q.
• The division theorem gives P = A Q + B with B a polynomial in x_0 of degree < d: exists_division_conv and the slices (eq_sum_convTail_sliceConv, Slices.lean) give the remainder as the series of a polynomial B of degree < d; by assumption W(z) = 0 ⇒ B(z) = 0 near 0.
• Q is square-free in 𝒪_m[x_0], so its discriminant is nonzero: the Weierstrass polynomial W_p is square-free in 𝒪_m[x_0] because its monic divisors are Weierstrass polynomials (exists_weierstrassPolynomial_of_monic_dvd) and a Weierstrass polynomial of positive degree is not a unit of 𝒪_{m+1} (squarefree_weierstrassPolynomial_of_squarefree); the discriminant is replaced by the resultant D = Res(W_p, W_p') ∈ 𝒪_m, nonzero because W_p stays square-free, hence separable, over the fraction field of the integrally closed domain 𝒪_m (squarefree_map_fractionRing, Mathlib's Gauss lemma IsIntegrallyClosed.eq_map_mul_C_of_dvd, Monic.dvd_iff_fraction_map_dvd_fraction_map, PerfectField.separable_iff_squarefree, resultant_ne_zero, resultant_map_map), with the Bezout identity W_p U + W_p' V = C D (Mathlib's exists_mul_add_mul_eq_C_resultant).
• On a dense subset of a small neighbourhood of 0 the specialization Q_a has d pairwise distinct small zeros: specializing the Bezout identity at a parameter x with D(x) ≠ 0 (Specialize.lean) makes W_p(x, ·) coprime to its derivative, hence separable with d distinct roots over the algebraically closed ℂ (eventually_isCoprime_specialize, card_roots_toFinset_specialize); the roots are small by norm_root_lt_of_monic (eventually_forall_root_norm_lt).
• Hence B_a vanishes for these a, and B = 0 by continuity: at such x, B(x, ·) of degree < d vanishes at the d roots, so it is 0 (eq_zero_of_natDegree_lt_card_of_eval_eq_zero); the coefficients of B vanish on the set {D ≠ 0}, which meets every open set near 0 (exists_evalSeries_ne_zero_of_isOpen), hence near 0 by continuity, hence are 0 by the identity theorem (convPolyEval_dvd_of_eventually_of_squarefree).

instance Analytic.instCharZeroConv {K : Type u_1} [RCLike K] {m : ℕ} : CharZero ↥(Conv K m)

The germ ring has characteristic zero (a K-algebra).

theorem Analytic.squarefree_map_mulEquiv_iff {R : Type u_2} {S : Type u_3} [CommMonoid R] [CommMonoid S] (σ : R ≃* S) (a : R) : Squarefree (σ a) ↔ Squarefree a

Square-freeness is invariant under a multiplicative equivalence.

theorem Analytic.eventually_evalSeries_ne_zero_of_isUnit {K : Type u_1} [RCLike K] {n : ℕ} {u : ↥(Conv K n)} (hu : IsUnit u) : ∀ᶠ (x : Fin n → K) in nhds 0, evalSeries (↑u) x ≠ 0

A unit of the germ ring does not vanish near 0 (its inverse is convergent too).

theorem Analytic.constantCoeff_convPolyEval_weierstrassPolynomial {K : Type u_1} [RCLike K] {m d : ℕ} {c : Fin d → ↥(Conv K m)} (hc : ∀ (j : Fin d), MvPowerSeries.constantCoeff ↑(c j) = 0) (hd : 0 < d) : MvPowerSeries.constantCoeff ↑((convPolyEval K) (weierstrassPolynomial d c)) = 0

The series of a Weierstrass polynomial of positive degree has constant coefficient 0.

theorem Analytic.squarefree_weierstrassPolynomial_of_squarefree {K : Type u_1} [RCLike K] {m d : ℕ} {c : Fin d → ↥(Conv K m)} (hc : ∀ (j : Fin d), MvPowerSeries.constantCoeff ↑(c j) = 0) (hsq : Squarefree ((convPolyEval K) (weierstrassPolynomial d c))) : Squarefree (weierstrassPolynomial d c)

A Weierstrass polynomial whose series is square-free in 𝒪_{m+1} is square-free in 𝒪_m[x_0]: its monic divisors are Weierstrass polynomials (exists_weierstrassPolynomial_of_monic_dvd), and a Weierstrass polynomial of positive degree is not a unit of 𝒪_{m+1} (the square-freeness step of [Fre17, Ch. I, 5.1]).

theorem Analytic.squarefree_map_fractionRing {R : Type u_2} [CommRing R] [IsDomain R] [IsIntegrallyClosed R] {W : Polynomial R} (hW : W.Monic) (hsq : Squarefree W) : Squarefree (Polynomial.map (algebraMap R (FractionRing R)) W)

A monic square-free polynomial over an integrally closed domain stays square-free over the fraction field (Gauss's lemma: a monic factor over the fraction field descends).

theorem Analytic.resultant_derivative_ne_zero_of_squarefree {R : Type u_2} [CommRing R] [IsDomain R] [IsIntegrallyClosed R] [CharZero R] {W : Polynomial R} (hW : W.Monic) (hsq : Squarefree W) : W.resultant (Polynomial.derivative W) ≠ 0

A monic square-free polynomial over an integrally closed domain of characteristic zero is separable over the fraction field, so its resultant with its derivative is nonzero (the nonzero discriminant of [Fre17, Ch. I, 5.1], with the resultant of W and W' in place of the discriminant).

The analytic argument

theorem Analytic.eventually_isCoprime_specialize {K : Type u_1} [RCLike K] {m : ℕ} {W : Polynomial ↥(Conv K m)} (hd : 0 < W.natDegree) : ∀ᶠ (x : Fin m → K) in nhds 0, evalSeries (↑(W.resultant (Polynomial.derivative W))) x ≠ 0 → IsCoprime (specialize W x) (Polynomial.derivative (specialize W x))

The Bezout identity W U + W' V = C (Res(W, W')) specialized at a parameter x near 0: where the resultant does not vanish, W(x, ·) is coprime to its derivative.

theorem Analytic.card_roots_toFinset_specialize {K : Type u_1} [RCLike K] {m : ℕ} [IsAlgClosed K] {W : Polynomial ↥(Conv K m)} (hW : W.Monic) {x : Fin m → K} (hcop : IsCoprime (specialize W x) (Polynomial.derivative (specialize W x))) : (specialize W x).roots.toFinset.card = W.natDegree

Over an algebraically closed field, a specialization coprime to its derivative has exactly deg W distinct roots.

theorem Analytic.eventually_forall_root_norm_lt {K : Type u_1} [RCLike K] {m d : ℕ} {c : Fin d → ↥(Conv K m)} (hc : ∀ (j : Fin d), MvPowerSeries.constantCoeff ↑(c j) = 0) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : ∀ᶠ (x : Fin m → K) in nhds 0, ∀ (t : K), Polynomial.eval t (specialize (weierstrassPolynomial d c) x) = 0 → ‖t‖ < ε

Near 0, every root of the specialized Weierstrass polynomial has norm < ε (the small zeros of [Fre17, Ch. I, 5.1]).

theorem Analytic.convPolyEval_dvd_of_eventually_of_squarefree {m d : ℕ} {c : Fin d → ↥(Conv ℂ m)} (hc : ∀ (j : Fin d), MvPowerSeries.constantCoeff ↑(c j) = 0) (hd : 0 < d) (hsq : Squarefree ((convPolyEval ℂ) (weierstrassPolynomial d c))) {P : ↥(Conv ℂ (m + 1))} (h : ∀ᶠ (z : Fin (m + 1) → ℂ) in nhds 0, evalSeries (↑((convPolyEval ℂ) (weierstrassPolynomial d c))) z = 0 → evalSeries (↑P) z = 0) : (convPolyEval ℂ) (weierstrassPolynomial d c) ∣ P

The hypersurface Nullstellensatz for a Weierstrass polynomial over ℂ [Fre17, Ch. I, 5.1]: if the zero set of the square-free W = convPolyEval (weierstrassPolynomial d c) near 0 lies in the zero set of P, then W ∣ P.

theorem Analytic.dvd_of_eventually_of_squarefree {m : ℕ} {Q P : ↥(Conv ℂ (m + 1))} (hQ0 : Q ≠ 0) (hsq : Squarefree Q) (h : ∀ᶠ (z : Fin (m + 1) → ℂ) in nhds 0, evalSeries (↑Q) z = 0 → evalSeries (↑P) z = 0) : Q ∣ P

The hypersurface Nullstellensatz over ℂ [Fre17, Ch. I, 5.1], square-free case: if every zero of the nonzero square-free series Q near 0 is a zero of P, then Q ∣ P.

theorem Analytic.dvd_of_vanishesOn_of_prime {m : ℕ} {Q f : ↥(Conv ℂ (m + 1))} (hQ : Prime Q) (hf : VanishesOn {Q} f) : Q ∣ f

The hypersurface Nullstellensatz for a prime Q [Fre17, Ch. I, 5.1]: a series vanishing on the zero-set germ of the prime Q is divisible by Q.

theorem Analytic.vanishingIdeal_span_singleton_le_of_prime {m : ℕ} {Q : ↥(Conv ℂ (m + 1))} (hQ : Prime Q) : vanishingIdeal (Ideal.span {Q}) ≤ Ideal.span {Q}

The Nullstellensatz for a principal prime ideal: 𝓘(V((Q))) ⊆ (Q) for Q prime.