Documentation

Hironaka.Analytic.Rueckert.NoetherNormalization

Noether normalization for analytic algebras #

For a proper ideal I of the ring π’ͺ_n = Conv K n of convergent power series there are d ≀ n, an injection e : Fin d β†ͺ Fin n of the coordinates and a K-linear change of coordinates L such that the composite π’ͺ_d β†’ π’ͺ_n β†’ π’ͺ_n β†’ π’ͺ_n / I (embed along e, substitute L, reduce modulo I) is injective and finite (exists_noetherNormalization_analytic). The proof follows [Fre17, Ch. I, Β§7]:

Freitag works over β„‚. The proof is carried out over any K with [RCLike K], the Weierstrass division and the linear changes of coordinates being stated over K. The map π’ͺ_d β†’ π’ͺ_n is convEmbed K e (Embed.lean) composed with substEquiv L (Subst.lean); the induction composes the block-diagonal change x ↦ (x_0, L' (x_1, …, x_{n-1})) (consCLE L') with L⁻¹ so that the tail embedding convTail intertwines the two substitutions (substConv_consCLE_convTail). The normalization is the starting point of the local parametrization of a prime germ (ParametrizationPrimitive.lean) and of the theory of dimension (Parameters.lean); the dimension theory of analytic spaces (Hironaka/AnalyticSpace/ConvDimension.lean, Hironaka/AnalyticSpace/Semicontinuity.lean) applies it to the stalks.

Finiteness over the tail ring #

source
theorem Analytic.eq_sum_liftTail_coeff_mul_X_pow {K : Type u_1} [RCLike K] {m : β„•} {r : MvPowerSeries (Fin (m + 1)) K} {d : β„•} (hr : βˆ€ (Ξ½ : Fin (m + 1) β†’β‚€ β„•), d ≀ Ξ½ 0 β†’ (MvPowerSeries.coeff Ξ½) r = 0) :
r = βˆ‘ i ∈ Finset.range d, liftTail ((PowerSeries.coeff i) ((splitFirst K m) r)) * MvPowerSeries.X 0 ^ i

A series whose coefficients vanish in degree β‰₯ d in x_0 is the polynomial βˆ‘_{i < d} r_i(x_1, …, x_m) x_0^i in x_0 with coefficients r_i the slices splitFirst, lifted by liftTail.

source
theorem Analytic.finite_mk_comp_convTail {K : Type u_1} [RCLike K] {m : β„•} {I : Ideal β†₯(Conv K (m + 1))} {P : β†₯(Conv K (m + 1))} (hP : P ∈ I) {d : β„•} (hreg : IsRegularIn (↑P) d) :
((Ideal.Quotient.mk I).comp (convTail K).toRingHom).Finite

[Fre17, Ch. I, Lemma 7.1] with its additional remark: if the ideal I βŠ† π’ͺ_{m+1} contains a series P regular of order d in x_0, then π’ͺ_{m+1} / I is a finite π’ͺ_m-module, generated by the images of 1, x_0, …, x_0^{d-1}, along the tail embedding π’ͺ_m β†’ π’ͺ_{m+1}. Proof: Weierstrass division of a representative by P (exists_unique_weierstrassDivision) gives a remainder polynomial of degree < d in x_0 with convergent coefficients.

The block-diagonal linear change id βŠ• L' and the tail embedding #

source
noncomputable def Analytic.consCLE {K : Type u_1} [RCLike K] {m : β„•} (L' : (Fin m β†’ K) ≃L[K] Fin m β†’ K) :
(Fin (m + 1) β†’ K) ≃L[K] Fin (m + 1) β†’ K

The linear change x ↦ (x_0, L' (x_1, …, x_m)) of K^{m+1}: the identity on the regular variable x_0, the induction hypothesis's change L' on the tail variables (the induction step of [Fre17, Ch. I, 7.2]).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Analytic.consCLE_apply {K : Type u_1} [RCLike K] {m : β„•} (L' : (Fin m β†’ K) ≃L[K] Fin m β†’ K) (x : Fin (m + 1) β†’ K) :
    (consCLE L') x = Fin.cons (x 0) (L' (Fin.tail x))

    consCLE L' x = (x_0, L' (x_1, …, x_m)).

    source
    theorem Analytic.tail_consCLE {K : Type u_1} [RCLike K] {m : β„•} (L' : (Fin m β†’ K) ≃L[K] Fin m β†’ K) (x : Fin (m + 1) β†’ K) :
    Fin.tail ((consCLE L') x) = L' (Fin.tail x)

    The tail of consCLE L' x is L' of the tail of x.

    source
    theorem Analytic.substConv_consCLE_convTail {K : Type u_1} [RCLike K] {m : β„•} (L' : (Fin m β†’ K) ≃L[K] Fin m β†’ K) (c : β†₯(Conv K m)) :
    substConv (↑(consCLE L')) ((convTail K) c) = (convTail K) (substConv (↑L') c)

    Substituting consCLE L' into a series lifted from the tail variables is the lift of the substitution of L': the tail embedding convTail intertwines the two linear changes. Proved on the function level through evalSeries_substConv and evalSeries_liftTail.

    Noether normalization #

    source
    noncomputable def Analytic.normMap (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) :
    β†₯(Conv K d) →ₐ[K] β†₯(Conv K n) β§Έ I

    The normalization map π’ͺ_d β†’ π’ͺ_n β†’ π’ͺ_n β†’ π’ͺ_n / I: embed along the injection e of the coordinates (convEmbed K e), substitute the linear change L (substEquiv L), reduce modulo I. The abbreviation unfolds definitionally to this composite.

    Equations
    Instances For
      source
      theorem Analytic.normMap_apply {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) (c : β†₯(Conv K d)) :
      (normMap K I e L) c = (Ideal.Quotient.mk I) ((substEquiv L) ((convEmbed K e) c))

      normMap K I e L c = [substEquiv L (convEmbed K e c)].

      source
      theorem Analytic.convEmbed_refl {K : Type u_1} [RCLike K] {n : β„•} (c : β†₯(Conv K n)) :
      (convEmbed K (Function.Embedding.refl (Fin n))) c = c

      Embedding along the identity injection is the identity.

      source
      theorem Analytic.convEmbed_succ {K : Type u_1} [RCLike K] {m : β„•} (c : β†₯(Conv K m)) :
      (convEmbed K { toFun := Fin.succ, inj' := β‹― }) c = (convTail K) c

      The tail embedding convTail is the case e = Fin.succ of convEmbed.

      source
      theorem Analytic.convTail_convEmbed {K : Type u_1} [RCLike K] {m d : β„•} (e : Fin d β†ͺ Fin m) (c : β†₯(Conv K d)) :
      (convTail K) ((convEmbed K e) c) = (convEmbed K (e.trans { toFun := Fin.succ, inj' := β‹― })) c

      The tail embedding of an embedding along e is the embedding along Fin.succ ∘ e (convEmbed_succ composed with the renaming along e).

      source
      theorem Analytic.exists_normMap_bot {K : Type u_1} [RCLike K] {n : β„•} (I : Ideal β†₯(Conv K n)) (hI : I = βŠ₯) :
      βˆƒ (d : β„•) (e : Fin d β†ͺ Fin n) (L : (Fin n β†’ K) ≃L[K] Fin n β†’ K), Function.Injective ⇑(normMap K I e L) ∧ (↑(normMap K I e L)).Finite

      The case I = 0 of [Fre17, Ch. I, 7.2]: for the zero ideal, d = n with the identity injection and the identity linear change, π’ͺ_n β†’ π’ͺ_n / 0 being an isomorphism.

      source
      theorem Analytic.exists_noetherNormalization_analytic {K : Type u_1} [RCLike K] {n : β„•} (I : Ideal β†₯(Conv K n)) (hI : I β‰  ⊀) :
      βˆƒ (d : β„•) (e : Fin d β†ͺ Fin n) (L : (Fin n β†’ K) ≃L[K] Fin n β†’ K), Function.Injective ⇑(normMap K I e L) ∧ (↑(normMap K I e L)).Finite

      Noether normalization for analytic algebras, existence clause [Fre17, Ch. I, Theorem 7.2] (the source works over β„‚; the proof here is over any K with [RCLike K]): for a proper ideal I βŠ† π’ͺ_n there are d, an injection e : Fin d β†ͺ Fin n and a linear change L with the normalization map π’ͺ_d β†’ π’ͺ_n / I (normMap K I e L) injective and finite. Induction on n by repeated application of Lemma 7.1 (finite_mk_comp_convTail) after the z_n-general reduction (exists_substEquiv_isRegularIn), with RingHom.kerLift for the induced map on π’ͺ_{n-1} / b, RingHom.Finite.comp for the transitivity of finiteness, and Ideal.quotientEquiv to transport back along L⁻¹.