Documentation

Hironaka.Analytic.Rueckert.Reexpansion

Monic relations under translation of the centre #

The analytic half of the upper semicontinuity of the dimension of an analytic germ [Fre17, Ch. II, 5.4], on Conv K n. A Noether normalization π’ͺ_d β†’ π’ͺ_n/I (NoetherNormalization.lean: embed along e : Fin d β†ͺ Fin n, substitute the linear change Οƒ = substEquiv L, reduce mod I) is module-finite, so every coordinate Οƒ (X i) is integral over π’ͺ_d: it satisfies a monic relation Οƒ (X_i^D + βˆ‘_k c_k(X ∘ e) X_i^k) ∈ I (exists_monic_relation_of_finite; the module-finiteness of the normalization in the proof of [Fre17, Ch. II, 5.4]). The relation is a convergent series; its function near a nearby centre w is again of the same shape, with the coefficient series c_k re-expanded at the projected point (L w) ∘ e (exists_reexpansion, from AnalyticAt.exists_eventuallyEq_evalSeries) and the fibre coordinate translated by (L w) i (exists_substEquiv_shapeSeries_translate; the polynomial Q(a₁, …, a_{nβˆ’1}, z_n βˆ’ a_n), general in z_n βˆ’ a_n with coefficients converging on a common polydisc, of the same proof). Modulo the base coordinates Οƒ X_{e j} such a shape is a monic polynomial with constant coefficients in Οƒ X_i + a (substEquiv_shapeSeries_sub_mem, by convEmbed_sub_algebraMap_mem), which is what the parameter bound ringKrullDim_quotient_le_of_parameters (Parameters.lean, Krull's height theorem) needs: ringKrullDim_quotient_le_of_forall_exists_shape_mem. The semicontinuity theorem for analytic spaces (Hironaka/AnalyticSpace/Semicontinuity.lean) realizes the relations as sections near the point, spreads their membership in the ideal to a neighbourhood and reads their germs at nearby points through the Taylor isomorphism.

Two steps differ from the printed proof: the translation lemma eventually_eventually_add_of_eventuallyEq (a formal filter statement) and the re-expansion of the coefficients replace the Weierstrass polynomial whose coefficients converge on a polydisc, and the parameter bound replaces the appeal to Cohen–Seidenberg for dim π’ͺ_{Y,f(a)} β‰₯ dim π’ͺ_{X,a} ([Fre17, Ch. II, 5.4] with [Fre17, Ch. VII, 5.6–5.7]).

source
theorem Analytic.evalSeries_convEmbed {K : Type u_1} [RCLike K] {n d : β„•} (e : Fin d β†ͺ Fin n) (c : β†₯(Conv K d)) (x : Fin n β†’ K) :
evalSeries (↑((convEmbed K e) c)) x = evalSeries (↑c) (x ∘ ⇑e)

The function of a series embedded along e is the function of the series in the base coordinates x ∘ e (convEmbed is rename e).

source
theorem Analytic.evalSeries_algebraMap_conv {K : Type u_1} [RCLike K] {n : β„•} (a : K) (x : Fin n β†’ K) :
evalSeries (↑((algebraMap K β†₯(Conv K n)) a)) x = a

The function of a constant series is the constant.

source
theorem Analytic.evalSeries_convX {K : Type u_1} [RCLike K] {n : β„•} (i : Fin n) (x : Fin n β†’ K) :
evalSeries (↑(convX K i)) x = x i

The function of the coordinate series X i is the coordinate x i.

source
theorem Analytic.evalSeries_conv_add_eventually {K : Type u_1} [RCLike K] {n : β„•} (f g : β†₯(Conv K n)) :
evalSeries ↑(f + g) =αΆ [nhds 0] fun (x : Fin n β†’ K) => evalSeries (↑f) x + evalSeries (↑g) x

Conv-level form of evalSeries_add_eventually.

source
theorem Analytic.evalSeries_conv_mul_eventually {K : Type u_1} [RCLike K] {n : β„•} (f g : β†₯(Conv K n)) :
evalSeries ↑(f * g) =αΆ [nhds 0] fun (x : Fin n β†’ K) => evalSeries (↑f) x * evalSeries (↑g) x

Conv-level form of evalSeries_mul_eventually.

source
theorem Analytic.evalSeries_conv_pow_eventually {K : Type u_1} [RCLike K] {n : β„•} (f : β†₯(Conv K n)) (k : β„•) :
evalSeries ↑(f ^ k) =αΆ [nhds 0] fun (x : Fin n β†’ K) => evalSeries (↑f) x ^ k

Conv-level form of evalSeries_pow_eventually.

source
theorem Analytic.evalSeries_conv_sum_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

Conv-level form of evalSeries_finsetSum_eventually.

source
noncomputable def Analytic.shapeSeries (K : Type u_1) [RCLike K] {n d : β„•} (i : Fin n) (e : Fin d β†ͺ Fin n) {D : β„•} (a : K) (c : Fin D β†’ β†₯(Conv K d)) :
β†₯(Conv K n)

The shape (X_i + a)^D + βˆ‘_k c_k(X ∘ e) (X_i + a)^k of a monic relation for X_i over the base coordinates X ∘ e, translated by a in the fibre coordinate.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Analytic.evalSeries_shapeSeries {K : Type u_1} [RCLike K] {n d : β„•} (i : Fin n) (e : Fin d β†ͺ Fin n) {D : β„•} (a : K) (c : Fin D β†’ β†₯(Conv K d)) :
    evalSeries ↑(shapeSeries K i e a c) =αΆ [nhds 0] fun (x : Fin n β†’ K) => (x i + a) ^ D + βˆ‘ k : Fin D, evalSeries (↑(c k)) (x ∘ ⇑e) * (x i + a) ^ ↑k

    The function of the shape near 0.

    source
    theorem Analytic.substEquiv_shapeSeries_sub_mem {K : Type u_1} [RCLike K] {n d : β„•} (L : (Fin n β†’ K) ≃L[K] Fin n β†’ K) (i : Fin n) (e : Fin d β†ͺ Fin n) {D : β„•} (a : K) (c : Fin D β†’ β†₯(Conv K d)) :
    (substEquiv L) (shapeSeries K i e a c) - (((substEquiv L) (convX K i) + (algebraMap K β†₯(Conv K n)) a) ^ D + βˆ‘ k : Fin D, (algebraMap K β†₯(Conv K n)) (MvPowerSeries.constantCoeff ↑(c k)) * ((substEquiv L) (convX K i) + (algebraMap K β†₯(Conv K n)) a) ^ ↑k) ∈ Ideal.span (Set.range fun (j : Fin d) => (substEquiv L) (convX K (e j)))

    Modulo the base coordinates Οƒ X_{e j}, Οƒ (shapeSeries a c) is the polynomial expression with the constant coefficients of the c_k in Οƒ X_i + a.

    source
    theorem Analytic.exists_reexpansion {K : Type u_1} [RCLike K] {d : β„•} (c : β†₯(Conv K d)) :
    βˆ€αΆ  (uβ‚€ : Fin d β†’ K) in nhds 0, βˆƒ (c' : β†₯(Conv K d)), βˆ€αΆ  (u : Fin d β†’ K) in nhds uβ‚€, evalSeries (↑c) u = evalSeries (↑c') (u - uβ‚€)

    Re-expansion of a convergent series at a point near 0 (the coefficients are re-expanded at the projected point; the coefficients converging on a common polydisc in the proof of [Fre17, Ch. II, 5.4]).

    source
    theorem Analytic.eventually_eventually_add_of_eventuallyEq {K : Type u_1} [RCLike K] {n : β„•} {F G : (Fin n β†’ K) β†’ K} (h : F =αΆ [nhds 0] G) :
    βˆ€αΆ  (v : Fin n β†’ K) (z : Fin n β†’ K) in nhds 0, F (z + v) = G (z + v)

    Translation of an eventual equality at 0: if F and G agree near 0, then for v near 0, F (z + v) = G (z + v) for z near 0.

    source
    theorem Analytic.tendsto_comp_embedding {K : Type u_1} [RCLike K] {n d : β„•} (e : Fin d β†ͺ Fin n) :
    Filter.Tendsto (fun (v : Fin n β†’ K) => v ∘ ⇑e) (nhds 0) (nhds 0)

    Composition with ∘ e tends to 0 at 0.

    source
    theorem Analytic.tendsto_clequiv_zero {K : Type u_1} [RCLike K] {n : β„•} (L : (Fin n β†’ K) ≃L[K] Fin n β†’ K) :
    Filter.Tendsto (fun (z : Fin n β†’ K) => L z) (nhds 0) (nhds 0)

    A continuous linear equivalence tends to 0 at 0.

    source
    theorem Analytic.exists_substEquiv_shapeSeries_translate {K : Type u_1} [RCLike K] {n d : β„•} (L : (Fin n β†’ K) ≃L[K] Fin n β†’ K) (i : Fin n) (e : Fin d β†ͺ Fin n) {D : β„•} (c : Fin D β†’ β†₯(Conv K d)) :
    βˆ€αΆ  (w : Fin n β†’ K) in nhds 0, βˆƒ (c' : Fin D β†’ β†₯(Conv K d)), βˆ€αΆ  (z : Fin n β†’ K) in nhds 0, evalSeries (↑((substEquiv L) (shapeSeries K i e 0 c))) (z + w) = evalSeries (↑((substEquiv L) (shapeSeries K i e (L w i) c'))) z

    Translation of a monic relation: for w near 0, the function z ↦ Οƒ(shape 0 c)(z + w) is near z = 0 the function of Οƒ (shape ((L w) i) c') for re-expanded coefficients c'.

    source
    theorem Analytic.exists_monic_relation_of_finite {K : Type u_1} [RCLike K] {n d : β„•} (I : Ideal β†₯(Conv K n)) (e : Fin d β†ͺ Fin n) (L : (Fin n β†’ K) ≃L[K] Fin n β†’ K) (hfin : (↑(normMap K I e L)).Finite) (i : Fin n) :
    βˆƒ (D : β„•) (c : Fin D β†’ β†₯(Conv K d)), (substEquiv L) (shapeSeries K i e 0 c) ∈ I

    A finite normalization map makes every coordinate Οƒ (X i) integral over π’ͺ_d: a monic relation of the shape Οƒ (X_i^D + βˆ‘_k c_k(X ∘ e) X_i^k) ∈ I (shapeSeries with a = 0); the module-finiteness of the normalization in the proof of [Fre17, Ch. II, 5.4].

    source
    theorem Analytic.ringKrullDim_quotient_le_of_forall_exists_shape_mem {K : Type u_1} [RCLike K] {n d : β„•} (I : Ideal β†₯(Conv K n)) (L : (Fin n β†’ K) ≃L[K] Fin n β†’ K) (e : Fin d β†ͺ Fin n) (h : βˆ€ (i : Fin n), βˆƒ (D : β„•) (a : K) (c : Fin D β†’ β†₯(Conv K d)), (substEquiv L) (shapeSeries K i e a c) ∈ I) :
    ringKrullDim (β†₯(Conv K n) β§Έ I) ≀ ↑d

    If every coordinate Οƒ (X i) satisfies a relation of the shape Οƒ (shapeSeries i e a c) ∈ I, then dim π’ͺ_n / I ≀ d: the relation is monic with constant coefficients modulo the base coordinates, and the parameter bound applies ([Fre17, Ch. II, 5.4] with [Fre17, Ch. VII, 5.6]).