Documentation

Hironaka.Analytic.Rueckert.FibreDivision

Iterated Weierstrass division by monic relations of the fibre coordinates #

The division argument of [Fre17, Ch. I, 8.3], done simultaneously in all fibre coordinates (see also [GR84, Chapter 3]): let e : Fin d β†ͺ Fin m embed the base coordinates and let every fibre coordinate x_i (i βˆ‰ range e) satisfy a monic relation Qf_i(x_i), Qf_i ∈ π’ͺ_d[T]. Then every F ∈ π’ͺ_m is, modulo the ideal generated by the relations, a polynomial in the fibre coordinates over the base: F ≑ βˆ‘_ΞΌ a_ΞΌ(x_base) x_fibre^ΞΌ with ΞΌ_i < deg Qf_i. The textbooks divide one variable at a time; here the induction is on the number m of variables: a fibre coordinate is moved to the first position by the permutation permConv (swap 0 i) (PermConv.lean), the monic relation in x_0 is x_0-regular of some order ≀ deg Qf_i (exists_isRegularIn_convPolyEval_of_monic), Weierstrass division (exists_eq_mul_add_sum_convTail_mul_convX_pow, MonicDivision.lean) yields a polynomial remainder in x_0 whose coefficients live in the tail ring π’ͺ_{m-1}, and the induction hypothesis reduces those coefficients modulo the remaining relations (now relations in π’ͺ_{m-1}). The base of the induction is the case of no fibre coordinate (e onto), where F itself is a base series.

fibreBox e Qf is the additive monoid of such polynomials (exponents 0 on the base indices, < deg Qf_i on the fibre indices); fibreRelIdeal e Qf is the ideal of the relations. This is the finiteness step of the parametrization of a prime germ (ParametrizationDivision.lean).

source
theorem Analytic.convTail_convX {m : β„•} (j : Fin m) :
(convTail β„‚) (convX β„‚ j) = convX β„‚ j.succ

The tail embedding of a coordinate series is the next coordinate series (liftTail is the renaming along Fin.succ).

source
noncomputable def Analytic.fibreBox {m d : β„•} (e : Fin d β†ͺ Fin m) (Qf : Fin m β†’ Polynomial β†₯(Conv β„‚ d)) :
AddSubmonoid β†₯(Conv β„‚ m)

The additive monoid of polynomials in the fibre coordinates over the base: sums of a(x_base) · ∏ x_i^{μ_i} with μ_i = 0 on the base indices and μ_i < deg Qf_i on the fibre indices.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Analytic.fibreRelIdeal {m d : β„•} (e : Fin d β†ͺ Fin m) (Qf : Fin m β†’ Polynomial β†₯(Conv β„‚ d)) :
    Ideal β†₯(Conv β„‚ m)

    The ideal generated by the monic relations Qf_i(x_i) of the fibre coordinates.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Analytic.mem_fibreBox_of {m d : β„•} {e : Fin d β†ͺ Fin m} {Qf : Fin m β†’ Polynomial β†₯(Conv β„‚ d)} (a : β†₯(Conv β„‚ d)) (ΞΌ : Fin m β†’ β„•) (h0 : βˆ€ i ∈ Set.range ⇑e, ΞΌ i = 0) (hlt : βˆ€ i βˆ‰ Set.range ⇑e, ΞΌ i < (Qf i).natDegree) :
      (convEmbed β„‚ e) a * ∏ i : Fin m, convX β„‚ i ^ ΞΌ i ∈ fibreBox e Qf
      source
      theorem Analytic.rel_mem_fibreRelIdeal {m d : β„•} {e : Fin d β†ͺ Fin m} {Qf : Fin m β†’ Polynomial β†₯(Conv β„‚ d)} {i : Fin m} (hi : i βˆ‰ Set.range ⇑e) :
      Polynomial.eval (convX β„‚ i) (Polynomial.map (convEmbed β„‚ e).toRingHom (Qf i)) ∈ fibreRelIdeal e Qf
      source
      theorem Analytic.exists_mem_fibreBox_sub_mem_of_surjective {m d : β„•} {e : Fin d β†ͺ Fin m} (Qf : Fin m β†’ Polynomial β†₯(Conv β„‚ d)) (hsurj : Function.Surjective ⇑e) (F : β†₯(Conv β„‚ m)) :
      βˆƒ G ∈ fibreBox e Qf, F - G ∈ fibreRelIdeal e Qf

      No fibre coordinate (e onto): every series is a base series, the box itself.

      source
      theorem Analytic.swap_apply_ne_zero_of_mem_range {m d : β„•} (e : Fin d β†ͺ Fin (m + 1)) {i : Fin (m + 1)} (hi : i βˆ‰ Set.range ⇑e) {x : Fin (m + 1)} (hx : x ∈ Set.range ⇑e) :
      (Equiv.swap 0 i) x β‰  0

      After the swap 0 ↔ i, a base index is never 0.

      source
      noncomputable def Analytic.predEmb {m d : β„•} (e : Fin d β†ͺ Fin (m + 1)) {i : Fin (m + 1)} (hi : i βˆ‰ Set.range ⇑e) :
      Fin d β†ͺ Fin m

      The base embedding after removing the fibre coordinate i (moved to position 0 by the swap): k ↦ pred (swap 0 i (e k)).

      Equations
      Instances For
        source
        theorem Analytic.predEmb_succ {m d : β„•} (e : Fin d β†ͺ Fin (m + 1)) {i : Fin (m + 1)} (hi : i βˆ‰ Set.range ⇑e) (k : Fin d) :
        ((predEmb e hi) k).succ = (Equiv.swap 0 i) (e k)
        source
        theorem Analytic.predEmb_trans_succ {m d : β„•} (e : Fin d β†ͺ Fin (m + 1)) {i : Fin (m + 1)} (hi : i βˆ‰ Set.range ⇑e) :
        (predEmb e hi).trans { toFun := Fin.succ, inj' := β‹― } = e.trans (Equiv.toEmbedding (Equiv.swap 0 i))
        source
        theorem Analytic.notMem_range_predEmb_iff {m d : β„•} (e : Fin d β†ͺ Fin (m + 1)) {i : Fin (m + 1)} (hi : i βˆ‰ Set.range ⇑e) (j : Fin m) :
        j βˆ‰ Set.range ⇑(predEmb e hi) ↔ (Equiv.swap 0 i) j.succ βˆ‰ Set.range ⇑e
        source
        noncomputable def Analytic.tailSwap {m : β„•} (i : Fin (m + 1)) :
        β†₯(Conv β„‚ m) →ₐ[β„‚] β†₯(Conv β„‚ (m + 1))

        The transport π’ͺ_m β†’ π’ͺ_{m+1}, tail embedding followed by the inverse swap: it puts the remaining variables back in their places.

        Equations
        Instances For
          source
          theorem Analytic.tailSwap_apply {m : β„•} (i : Fin (m + 1)) (x : β†₯(Conv β„‚ m)) :
          (tailSwap i) x = (permConv β„‚ (Equiv.swap 0 i)).symm ((convTail β„‚) x)
          source
          theorem Analytic.tailSwap_convX {m : β„•} (i : Fin (m + 1)) (j : Fin m) :
          (tailSwap i) (convX β„‚ j) = convX β„‚ ((Equiv.swap 0 i) j.succ)
          source
          theorem Analytic.tailSwap_convEmbed {m d : β„•} (e : Fin d β†ͺ Fin (m + 1)) {i : Fin (m + 1)} (hi : i βˆ‰ Set.range ⇑e) (a : β†₯(Conv β„‚ d)) :
          (tailSwap i) ((convEmbed β„‚ (predEmb e hi)) a) = (convEmbed β„‚ e) a
          source
          theorem Analytic.tailSwap_rel {m d : β„•} (e : Fin d β†ͺ Fin (m + 1)) {i : Fin (m + 1)} (hi : i βˆ‰ Set.range ⇑e) (Qf : Fin (m + 1) β†’ Polynomial β†₯(Conv β„‚ d)) (j : Fin m) :
          (tailSwap i) (Polynomial.eval (convX β„‚ j) (Polynomial.map (convEmbed β„‚ (predEmb e hi)).toRingHom (Qf ((Equiv.swap 0 i) j.succ)))) = Polynomial.eval (convX β„‚ ((Equiv.swap 0 i) j.succ)) (Polynomial.map (convEmbed β„‚ e).toRingHom (Qf ((Equiv.swap 0 i) j.succ)))
          source
          theorem Analytic.permConv_swap_rel {m d : β„•} (e : Fin d β†ͺ Fin (m + 1)) {i : Fin (m + 1)} (hi : i βˆ‰ Set.range ⇑e) (Qf : Fin (m + 1) β†’ Polynomial β†₯(Conv β„‚ d)) :
          (permConv β„‚ (Equiv.swap 0 i)) (Polynomial.eval (convX β„‚ i) (Polynomial.map (convEmbed β„‚ e).toRingHom (Qf i))) = (convPolyEval β„‚) (Polynomial.map (convEmbed β„‚ (predEmb e hi)).toRingHom (Qf i))

          The relation of the fibre coordinate i, after the swap, is the monic polynomial Qf_i in x_0 with coefficients embedded from the tail ring.

          source
          theorem Analytic.tailSwap_mem_fibreBox {m d : β„•} (e : Fin d β†ͺ Fin (m + 1)) {i : Fin (m + 1)} (hi : i βˆ‰ Set.range ⇑e) (Qf : Fin (m + 1) β†’ Polynomial β†₯(Conv β„‚ d)) {g : β†₯(Conv β„‚ m)} (hg : g ∈ fibreBox (predEmb e hi) fun (j : Fin m) => Qf ((Equiv.swap 0 i) j.succ)) {k : β„•} (hk : k < (Qf i).natDegree) :
          (tailSwap i) g * convX β„‚ i ^ k ∈ fibreBox e Qf

          The transport of a box element of the smaller ring, times a power x_i^k with k < deg Qf_i, is a box element of the larger ring.

          source
          theorem Analytic.tailSwap_mem_fibreRelIdeal {m d : β„•} (e : Fin d β†ͺ Fin (m + 1)) {i : Fin (m + 1)} (hi : i βˆ‰ Set.range ⇑e) (Qf : Fin (m + 1) β†’ Polynomial β†₯(Conv β„‚ d)) {r : β†₯(Conv β„‚ m)} (hr : r ∈ fibreRelIdeal (predEmb e hi) fun (j : Fin m) => Qf ((Equiv.swap 0 i) j.succ)) :
          (tailSwap i) r ∈ fibreRelIdeal e Qf

          The transport of the relation ideal of the smaller ring lies in the relation ideal of the larger ring.

          source
          theorem Analytic.exists_mem_fibreBox_sub_mem {d m : β„•} (e : Fin d β†ͺ Fin m) (Qf : Fin m β†’ Polynomial β†₯(Conv β„‚ d)) :
          (βˆ€ i βˆ‰ Set.range ⇑e, (Qf i).Monic) β†’ βˆ€ (F : β†₯(Conv β„‚ m)), βˆƒ G ∈ fibreBox e Qf, F - G ∈ fibreRelIdeal e Qf

          Iterated Weierstrass division (the division argument of [Fre17, Ch. I, 8.3], simultaneous in the fibre coordinates): with monic relations Qf_i(x_i) for every fibre coordinate, every F ∈ π’ͺ_m is, modulo the ideal of the relations, a polynomial in the fibre coordinates over the base with exponents below the degrees, by induction on the number of variables, dividing by one relation at a time.