Documentation

Hironaka.Analytic.Rueckert.Parameters

Systems of parameters in the germ ring π’ͺ_n #

The algebra behind the upper semicontinuity of the dimension of an analytic germ [Fre17, Ch. II, 5.4], on Conv K n. After a linear change of coordinates Οƒ = substEquiv L and a choice e : Fin d β†ͺ Fin n of base coordinates, suppose every fibre coordinate Οƒ (X i), i βˆ‰ range e, satisfies a monic polynomial with constant coefficients modulo I βŠ” (Οƒ X (e j))_j. Then the maximal ideal π”ͺ, generated by the Οƒ (X i) (maximalIdeal_conv_eq_span_algEquiv_convX: Hadamard's lemma for series sum_X_mul_divPart transported by the automorphism), lies in the radical of I βŠ” (Οƒ X (e j))_j (mem_radical_of_monic_aeval_mem: factor the monic polynomial as X^s Β· u with u(0) β‰  0, so u(Οƒ X i) is a unit), and Krull's height theorem (IsLocalRing.ringKrullDim_quotient_le_of_maximalIdeal_le_radical_sup) gives dim π’ͺ_n / I ≀ d (ringKrullDim_quotient_le_of_parameters). The lemma convEmbed_sub_algebraMap_mem (a series in the base coordinates is its constant term modulo the base coordinates) is what reduces the relations coming from a Noether normalization to relations with constant coefficients. The dimension theory itself is [Fre17, Ch. VII, 5.6] read on the germ ring.

source
noncomputable def Analytic.constantCoeffConv {K : Type u_1} [RCLike K] {n : β„•} :
β†₯(Conv K n) β†’+* K

The constant coefficient of a convergent series, as a ring homomorphism Conv K n β†’+* K.

Equations
Instances For
    source
    theorem Analytic.constantCoeffConv_apply {K : Type u_1} [RCLike K] {n : β„•} (f : β†₯(Conv K n)) :
    constantCoeffConv f = MvPowerSeries.constantCoeff ↑f
    source
    theorem Analytic.constantCoeffConv_algebraMap {K : Type u_1} [RCLike K] {n : β„•} (r : K) :
    constantCoeffConv ((algebraMap K β†₯(Conv K n)) r) = r

    The constant coefficient of a constant series.

    source
    theorem Analytic.mem_maximalIdeal_conv_iff {K : Type u_1} [RCLike K] {n : β„•} (f : β†₯(Conv K n)) :
    f ∈ IsLocalRing.maximalIdeal β†₯(Conv K n) ↔ MvPowerSeries.constantCoeff ↑f = 0

    f ∈ π”ͺ iff its constant coefficient vanishes (the unit criterion isUnit_iff_constantCoeff_ne_zero).

    source
    theorem Analytic.maximalIdeal_conv_eq_span_convX {K : Type u_1} [RCLike K] {n : β„•} :
    IsLocalRing.maximalIdeal β†₯(Conv K n) = Ideal.span (Set.range (convX K))

    The maximal ideal of Conv K n is generated by the coordinates (series-level Hadamard, sum_X_mul_divPart).

    source
    theorem Analytic.mem_maximalIdeal_algEquiv_iff {K : Type u_1} [RCLike K] {n : β„•} (Οƒ : β†₯(Conv K n) ≃ₐ[K] β†₯(Conv K n)) (f : β†₯(Conv K n)) :
    Οƒ f ∈ IsLocalRing.maximalIdeal β†₯(Conv K n) ↔ f ∈ IsLocalRing.maximalIdeal β†₯(Conv K n)

    An algebra automorphism of Conv K n preserves the maximal ideal.

    source
    theorem Analytic.maximalIdeal_conv_eq_span_algEquiv_convX {K : Type u_1} [RCLike K] {n : β„•} (Οƒ : β†₯(Conv K n) ≃ₐ[K] β†₯(Conv K n)) :
    IsLocalRing.maximalIdeal β†₯(Conv K n) = Ideal.span (Set.range fun (i : Fin n) => Οƒ (convX K i))

    The maximal ideal is generated by the images of the coordinates under an automorphism.

    source
    theorem Analytic.convEmbed_sub_algebraMap_mem {K : Type u_1} [RCLike K] {n d : β„•} (e : Fin d β†ͺ Fin n) (c : β†₯(Conv K d)) :
    (convEmbed K e) c - (algebraMap K β†₯(Conv K n)) (MvPowerSeries.constantCoeff ↑c) ∈ Ideal.span (Set.range fun (j : Fin d) => convX K (e j))

    A series in the coordinates e i differs from its constant coefficient by an element of the ideal generated by the coordinates X (e j) (series-level Hadamard, transported by rename).

    source
    theorem Analytic.constantCoeffConv_aeval {K : Type u_1} [RCLike K] {n : β„•} (p : Polynomial K) {x : β†₯(Conv K n)} (hx : x ∈ IsLocalRing.maximalIdeal β†₯(Conv K n)) :
    constantCoeffConv ((Polynomial.aeval x) p) = Polynomial.eval 0 p

    A polynomial with constant coefficients evaluated at an element of π”ͺ has constant coefficient p(0).

    source
    theorem Analytic.isUnit_conv_iff {K : Type u_1} [RCLike K] {n : β„•} (f : β†₯(Conv K n)) :
    IsUnit f ↔ MvPowerSeries.constantCoeff ↑f β‰  0

    A convergent series is a unit iff its constant coefficient is nonzero (isUnit_iff_constantCoeff_ne_zero, on Conv).

    source
    theorem Analytic.mem_radical_of_monic_aeval_mem {K : Type u_1} [RCLike K] {n : β„•} {I : Ideal β†₯(Conv K n)} {x : β†₯(Conv K n)} (hx : x ∈ IsLocalRing.maximalIdeal β†₯(Conv K n)) {p : Polynomial K} (hp : p.Monic) (hmem : (Polynomial.aeval x) p ∈ I) :
    x ∈ I.radical

    If a monic polynomial with constant coefficients vanishes at x ∈ π”ͺ modulo I, then x is in the radical of I β€” factor p = X^s Β· u with u(0) β‰  0, so u(x) is a unit.

    source
    theorem Analytic.span_algEquiv_convX_le_maximalIdeal {K : Type u_1} [RCLike K] {n d : β„•} (Οƒ : β†₯(Conv K n) ≃ₐ[K] β†₯(Conv K n)) (e : Fin d β†ͺ Fin n) :
    Ideal.span (Set.range fun (j : Fin d) => Οƒ (convX K (e j))) ≀ IsLocalRing.maximalIdeal β†₯(Conv K n)

    The base coordinates lie in the maximal ideal.

    source
    theorem Analytic.maximalIdeal_le_radical_sup_of_parameters {K : Type u_1} [RCLike K] {n d : β„•} (I : Ideal β†₯(Conv K n)) (Οƒ : β†₯(Conv K n) ≃ₐ[K] β†₯(Conv K n)) (e : Fin d β†ͺ Fin n) (hrel : βˆ€ i βˆ‰ Set.range ⇑e, βˆƒ (p : Polynomial K), p.Monic ∧ (Polynomial.aeval (Οƒ (convX K i))) p ∈ I βŠ” Ideal.span (Set.range fun (j : Fin d) => Οƒ (convX K (e j)))) :
    IsLocalRing.maximalIdeal β†₯(Conv K n) ≀ (I βŠ” Ideal.span (Set.range fun (j : Fin d) => Οƒ (convX K (e j)))).radical

    The maximal ideal lies in the radical of I βŠ” (Οƒ X (e j))_j when every fibre coordinate satisfies a monic relation with constant coefficients modulo that ideal.

    source
    theorem Analytic.ringKrullDim_quotient_le_of_parameters {K : Type u_1} [RCLike K] {n d : β„•} (I : Ideal β†₯(Conv K n)) (Οƒ : β†₯(Conv K n) ≃ₐ[K] β†₯(Conv K n)) (e : Fin d β†ͺ Fin n) (hrel : βˆ€ i βˆ‰ Set.range ⇑e, βˆƒ (p : Polynomial K), p.Monic ∧ (Polynomial.aeval (Οƒ (convX K i))) p ∈ I βŠ” Ideal.span (Set.range fun (j : Fin d) => Οƒ (convX K (e j)))) :
    ringKrullDim (β†₯(Conv K n) β§Έ I) ≀ ↑d

    Krull's height theorem in the germ ring: if for every coordinate X i outside the base coordinates X (e j) a monic polynomial with constant coefficients in Οƒ (X i) lies in I βŠ” (Οƒ X (e j))_j, then dim (π’ͺ_n / I) ≀ d, the d base coordinates being a system of parameters of π’ͺ_n / I [Fre17, Ch. VII, 5.6]. The general form for any Noetherian local ring (π”ͺ ≀ √(I βŠ” (s₁, …, s_d)) gives dim R/I ≀ d) is IsLocalRing.ringKrullDim_quotient_le_of_maximalIdeal_le_radical_sup.

    source
    theorem Analytic.exists_monic_aeval_mem_of_pow_add_sum {K : Type u_1} [RCLike K] {n : β„•} {J : Ideal β†₯(Conv K n)} {x : β†₯(Conv K n)} {D : β„•} (c : Fin D β†’ K) (a : K) (hmem : (x + (algebraMap K β†₯(Conv K n)) a) ^ D + βˆ‘ k : Fin D, (algebraMap K β†₯(Conv K n)) (c k) * (x + (algebraMap K β†₯(Conv K n)) a) ^ ↑k ∈ J) :
    βˆƒ (p : Polynomial K), p.Monic ∧ (Polynomial.aeval x) p ∈ J

    The relation (x + a)^D + βˆ‘_{k<D} c_k (x + a)^k ∈ J with constant coefficients c_k is a monic polynomial relation in x (the shape produced at a point near a Noether normalization).