Documentation

Hironaka.Analytic.Rueckert.Parametrization

Points of V(P) over the generic points of V(P ∩ π’ͺ_m) #

The parametrization lemma used in the second alternative of RΓΌckert's Nullstellensatz (Nullstellensatz.lean), in place of [Fre17, Ch. I, 7.3–7.4 and 8.2]. What the proof of the Nullstellensatz uses of the second alternative is only this: for a prime P βŠ† π’ͺ_{m+1} containing the series of a Weierstrass polynomial in x_0, with 𝔭 = P ∩ π’ͺ_m, over every point y ∈ V(𝔭) near 0 off the zero set of a fixed A βˆ‰ 𝔭 there is a point (t, y) ∈ V(P) with t as small as prescribed (exists_eventually_exists_cons_mem_zeroSet).

The argument. Reduce the finitely many generators of P modulo the Weierstrass series to polynomials B ∈ π’ͺ_m[x_0] whose series lie in P (Weierstrass division, exists_division_conv); let 𝔅 be the family of these remainders together with the Weierstrass polynomial. Over the domain RΜ„ = π’ͺ_m/𝔭 and its fraction field K', the ideal of K'[T] generated by the classes of 𝔅 is principal (K'[T] is a principal ideal domain); its generator g is nonzero (the Weierstrass polynomial is monic) and not a unit: a nonzero constant in the ideal would, after clearing denominators (exists_C_mul_eq_map_of_mem_span_image), give a nonzero element of RΜ„ in the ideal generated by 𝔅 in RΜ„[T], hence an element of π’ͺ_m βˆ– 𝔭 in P (the mechanism "P_0 ∈ 𝒫 ∩ π’ͺ_{nβˆ’1} = 𝔭" of [Fre17, Ch. I, 8.3], convPolyEval_mem_of_coeff_mem). Clearing denominators (IsLocalization.integerNormalization) gives Ο‰ ∈ RΜ„[T] of positive degree with C c_B Β· BΜ„ = Ο‰ Β· H_B for every B ∈ 𝔅 (exists_common_factor_of_span); lifted to π’ͺ_m[T], these identities hold modulo 𝔭[T], so they specialize exactly at the points of V(𝔭) near 0 (eventually_specialize_eq_zero_of_coeff_mem). Put A = lead(Ο‰) Β· ∏ c_B βˆ‰ 𝔭. At y ∈ V(𝔭) with A(y) β‰  0 the specialized Ο‰(y, Β·) has positive degree and a root t (β„‚ is algebraically closed), which is a root of every B(y, Β·), in particular of the Weierstrass polynomial, so t is small (eventually_forall_root_norm_lt), and (t, y) is a common zero of the generators of P.

source
theorem Analytic.smul_eq_C_algebraMap_mul {R : Type u_1} [CommRing R] (b : R) (c : Polynomial (FractionRing R)) :
b β€’ c = Polynomial.C ((algebraMap R (FractionRing R)) b) * c

The action of R on polynomials over the fraction field is multiplication by the constant.

source
theorem Analytic.exists_C_mul_eq_map_of_mem_span_image {R : Type u_1} [CommRing R] [IsDomain R] (𝔅 : Finset (Polynomial R)) {z : Polynomial (FractionRing R)} (hz : z ∈ Ideal.span (Polynomial.map (algebraMap R (FractionRing R)) '' ↑𝔅)) :
βˆƒ (r : R), r β‰  0 ∧ βˆƒ q ∈ Ideal.span ↑𝔅, Polynomial.C ((algebraMap R (FractionRing R)) r) * z = Polynomial.map (algebraMap R (FractionRing R)) q

Every element of the ideal generated by the images of a finite family of polynomials over R in K[T] (K the fraction field) becomes, after clearing a denominator, the image of an element of the ideal generated by the family in R[T].

source
theorem Analytic.exists_common_factor_of_span {R : Type u_1} [CommRing R] [IsDomain R] (𝔅 : Finset (Polynomial R)) (hne : βˆƒ W ∈ 𝔅, W β‰  0) (hprop : βˆ€ (r : R), Polynomial.C r ∈ Ideal.span ↑𝔅 β†’ r = 0) :
βˆƒ (Ο‰ : Polynomial R), 0 < Ο‰.natDegree ∧ βˆ€ B ∈ 𝔅, βˆƒ (c : R), c β‰  0 ∧ βˆƒ (H : Polynomial R), Polynomial.C c * B = Ο‰ * H

The algebraic core of the parametrization: a finite family 𝔅 of polynomials over the domain R, containing a nonzero polynomial and generating an ideal of R[T] without nonzero constants, has a common "root polynomial" Ο‰ ∈ R[T] of positive degree: every B ∈ 𝔅 satisfies C c * B = Ο‰ * H for some c β‰  0 and H.

source
theorem Analytic.evalSeries_finsetProd_eventually {K : Type u_1} [RCLike K] {n : β„•} {ΞΉ : Type u_2} (s : Finset ΞΉ) (F : ΞΉ β†’ β†₯(Conv K n)) :
evalSeries (∏ i ∈ s, ↑(F i)) =αΆ [nhds 0] fun (x : Fin n β†’ K) => ∏ i ∈ s, evalSeries (↑(F i)) x

Near 0, the value of a finite product of convergent series is the product of the values.

source
theorem Analytic.convPolyEval_mem_of_coeff_mem {K : Type u_1} [RCLike K] {m : β„•} {P : Ideal β†₯(Conv K (m + 1))} {Q : Polynomial β†₯(Conv K m)} (hQ : βˆ€ (i : β„•), Q.coeff i ∈ Ideal.comap (convTail K).toRingHom P) :
(convPolyEval K) Q ∈ P

A polynomial over π’ͺ_m whose coefficients lie in P ∩ π’ͺ_m has its series in P.

source
theorem Analytic.eventually_specialize_eq_zero_of_coeff_mem {K : Type u_1} [RCLike K] {m : β„•} {p : Ideal β†₯(Conv K m)} {Sp : Finset β†₯(Conv K m)} (hSp : Ideal.span ↑Sp = p) {D : Polynomial β†₯(Conv K m)} (hD : βˆ€ (i : β„•), D.coeff i ∈ p) :
βˆ€αΆ  (y : Fin m β†’ K) in nhds 0, y ∈ zeroSet Sp β†’ specialize D y = 0

Near 0, a polynomial with coefficients in p specializes to 0 at the points of V(p).

source
theorem Analytic.exists_eq_mul_add_convPolyEval {K : Type u_1} [RCLike K] {m : β„•} {W : β†₯(Conv K (m + 1))} {d : β„•} (hreg : IsRegularIn (↑W) d) (G : β†₯(Conv K (m + 1))) :
βˆƒ (q : β†₯(Conv K (m + 1))) (B : Polynomial β†₯(Conv K m)), G = q * W + (convPolyEval K) B

Weierstrass division with the remainder as the series of a polynomial.

source
theorem Analytic.exists_eventually_exists_cons_mem_zeroSet {m : β„•} {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) {S : Finset β†₯(Conv β„‚ (m + 1))} (hS : Ideal.span ↑S = P) {Sp : Finset β†₯(Conv β„‚ m)} (hSp : Ideal.span ↑Sp = Ideal.comap (convTail β„‚).toRingHom P) {Ξ΄ : ℝ} (hΞ΄ : 0 < Ξ΄) :
βˆƒ A βˆ‰ Ideal.comap (convTail β„‚).toRingHom P, βˆ€αΆ  (y : Fin m β†’ β„‚) in nhds 0, y ∈ zeroSet Sp β†’ evalSeries (↑A) y β‰  0 β†’ βˆƒ (t : β„‚), β€–tβ€– < Ξ΄ ∧ Fin.cons t y ∈ zeroSet S

The parametrization lemma (in place of [Fre17, Ch. I, 7.4 and 8.2]): for a prime P βŠ† π’ͺ_{m+1} containing the series of a Weierstrass polynomial in x_0, with p = P ∩ π’ͺ_m, there is A βˆ‰ p such that over every point y ∈ V(p) near 0 with A(y) β‰  0 there is a point (t, y) ∈ V(P) with t as small as prescribed.