Evaluating a multivariate power series at arguments from an adic ideal

Let S carry the I-adic topology for an ideal I, and let f be a multivariate power series evaluated at a family a : σ → S through a continuous coefficient map φ. This file bounds the value eval₂ φ a f by a power of I, in the three forms the estimate is used in: the value is confined to I ^ k as soon as the arguments are and φ sends the constant term there, and the confinement improves when the series vanishes in low total degree or when φ sends every coefficient into a power of I.

Three further results serve the same arguments from either side. Over finitely many variables a pointwise topologically nilpotent family admits evaluation; arguments drawn from I satisfy MvPowerSeries.HasEval in the first place, so that the value is defined at all; and the value is congruent to the image of the constant term modulo I.

They are proved differently. hasEval_of_finite_of_isTopologicallyNilpotent does not use the estimates above at all: over finitely many variables the decay condition at infinity is vacuous, so topological nilpotence of each argument is the whole content. hasEval_of_mem is its corollary, obtained by supplying that nilpotence from membership in I through IsAdic.isTopologicallyNilpotent_of_mem. eval₂_sub_constantCoeff_mem is the one that reduces to them — subtracting the constant term kills the constant monomial and every surviving monomial carries an argument, so the difference is the k = 1 case of eval₂_mem_pow applied to f - C (constantCoeff f).

The three bounds have the same one-line mechanism. MvPowerSeries.hasSum_eval₂ writes the value as the sum of its monomial values φ (coeff d f) * ∏ s, a s ^ d s; each such monomial is checked to lie in the relevant power of I; and the sum of a family inside I ^ n stays inside I ^ n because I ^ n is closed (IsAdic.isClosed_pow) and tsum_mem applies. The three statements differ only in which power the monomial estimate produces.

Three hypotheses of the source turn out to be unnecessary. Nothing asks for I to be maximal or for S to be local, only that the topology be I-adic, so the results are stated for an arbitrary ideal; the coefficient map is an arbitrary continuous φ : R →+* S rather than the identity, since MvPowerSeries.hasSum_eval₂ is already stated at that generality; and the index type need not be finite, because the summation argument uses only the Tendsto a cofinite (𝓝 0) already carried by HasEval. Taking I to be IsLocalRing.maximalIdeal S and φ to be RingHom.id S recovers the source statements.

Finiteness of σ survives in hasEval_of_finite_of_isTopologicallyNilpotent, where it is what makes the decay condition of HasEval vacuous; that is the one place the hypothesis does work, and hasEval_of_mem inherits it from there.

Main results

• MvPowerSeries.eval₂_mem_pow : arguments in I ^ k, and a constant term whose image under φ lies in I ^ k, confine the value to I ^ k.
• MvPowerSeries.eval₂_mem_pow_mul : a series vanishing below total degree c, evaluated at arguments of I ^ j, takes values in I ^ (c * j).
• MvPowerSeries.eval₂_mem_pow_add_mul : if moreover φ sends every coefficient into I ^ k, the value lies in I ^ (k + c * j).
• MvPowerSeries.hasEval_of_finite_of_isTopologicallyNilpotent : finitely many topologically nilpotent arguments are an admissible evaluation point.
• MvPowerSeries.hasEval_of_mem : a family of finitely many arguments drawn from I is an admissible evaluation point.
• MvPowerSeries.eval₂_sub_constantCoeff_mem : the value and the image of the constant term differ by an element of I.

Provenance

Adapted from Michael Stoll's EllipticCurves (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0) at commit 66889eada51a74c2f5dfb7fb5909b0b5a0a2d96e, file EllipticCurves/WeierstrassFormalGroup/Eval.lean, where the three bounds are ChabautyColeman.MvPSeries.eval_mem_maximalIdeal_pow, ..._pow_mul and ..._pow_add_mul, and EllipticCurves/Mathlib/Chabauty/MvPSeries.lean, where hasEval_of_mem carries the same name and eval₂_sub_constantCoeff_mem is ChabautyColeman.MvPSeries.eval_sub_constantCoeff_mem. That development evaluates through its own ChabautyColeman.MvPSeries.eval, which is by definition MvPowerSeries.eval₂ (RingHom.id _); the wrapper is dropped here and the statements are made directly about Mathlib's MvPowerSeries.eval₂, as are the generalisations noted above. The monomial estimates and the closed-ideal summation argument are the source's, as is the HasEval construction. The congruence modulo I is not: the source proves it from the hasSum expansion directly, whereas here it is the k = 1 case of eval₂_mem_pow applied to f - C (constantCoeff f), which is shorter and needs no finiteness of σ.

theorem MvPowerSeries.eval₂_mem_pow {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] [IsTopologicalSemiring R] [IsUniformAddGroup R] {S : Type u_3} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] {φ : R →+* S} {a : σ → S} {I : Ideal S} (hφ : Continuous ⇑φ) (ha : HasEval a) (hI : IsAdic I) {k : ℕ} (hmem : ∀ (i : σ), a i ∈ I ^ k) (f : MvPowerSeries σ R) (hcc : φ (constantCoeff f) ∈ I ^ k) : eval₂ φ a f ∈ I ^ k

The value lies in I ^ k when the arguments do and φ sends the constant term there. Every monomial of positive degree already carries an argument, hence a factor from I ^ k; the constant monomial is covered by the hypothesis on the image of the constant term.

theorem MvPowerSeries.eval₂_mem_pow_add_mul {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] [IsTopologicalSemiring R] [IsUniformAddGroup R] {S : Type u_3} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] {φ : R →+* S} {a : σ → S} {I : Ideal S} (hφ : Continuous ⇑φ) (ha : HasEval a) (hI : IsAdic I) {j c k : ℕ} (hmem : ∀ (i : σ), a i ∈ I ^ j) (f : MvPowerSeries σ R) (hcoeff : ∀ (d : σ →₀ ℕ), φ ((coeff d) f) ∈ I ^ k) (hlow : ∀ (d : σ →₀ ℕ), Finsupp.degree d < c → (coeff d) f = 0) : eval₂ φ a f ∈ I ^ (k + c * j)

Small coefficient images improve the bound. If in addition φ sends every coefficient of f into I ^ k, the two contributions multiply and the value lies in I ^ (k + c * j).

theorem MvPowerSeries.eval₂_mem_pow_mul {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] [IsTopologicalSemiring R] [IsUniformAddGroup R] {S : Type u_3} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] {φ : R →+* S} {a : σ → S} {I : Ideal S} (hφ : Continuous ⇑φ) (ha : HasEval a) (hI : IsAdic I) {j c : ℕ} (hmem : ∀ (i : σ), a i ∈ I ^ j) (f : MvPowerSeries σ R) (hcoeff : ∀ (d : σ →₀ ℕ), Finsupp.degree d < c → (coeff d) f = 0) : eval₂ φ a f ∈ I ^ (c * j)

A series vanishing below total degree c, evaluated at arguments of I ^ j, takes values in I ^ (c * j). This is the k = 0 case of eval₂_mem_pow_add_mul: every coefficient image lies in I ^ 0 = ⊤, so that hypothesis is vacuous and the exponent collapses.

theorem MvPowerSeries.eval₂_sub_constantCoeff_mem {σ : Type u_1} {R : Type u_2} [CommRing R] [UniformSpace R] [IsTopologicalSemiring R] [IsUniformAddGroup R] {S : Type u_3} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S] {φ : R →+* S} {a : σ → S} {I : Ideal S} (hφ : Continuous ⇑φ) (ha : HasEval a) (hI : IsAdic I) (hmem : ∀ (i : σ), a i ∈ I) (f : MvPowerSeries σ R) : eval₂ φ a f - φ (constantCoeff f) ∈ I

The value differs from the image of the constant term by an element of I. Equivalently, for arguments drawn from I the value of f is congruent to the image of its constant term modulo I.

theorem MvPowerSeries.hasEval_of_finite_of_isTopologicallyNilpotent {σ : Type u_1} {S : Type u_2} [CommRing S] [TopologicalSpace S] {a : σ → S} [Finite σ] (h : ∀ (i : σ), IsTopologicallyNilpotent (a i)) : HasEval a

Finitely many topologically nilpotent arguments can be substituted into a power series. Over finitely many variables the decay condition HasEval asks for at infinity is vacuous, so pointwise topological nilpotence is the whole of it.

theorem MvPowerSeries.hasEval_of_mem {σ : Type u_1} {S : Type u_2} [CommRing S] [TopologicalSpace S] {a : σ → S} {I : Ideal S} [Finite σ] (hI : IsAdic I) (hmem : ∀ (i : σ), a i ∈ I) : HasEval a

A family drawn from an adic ideal can be substituted into a power series. For an index type with finitely many variables, lying in I is the only condition the arguments need: it already gives them the HasEval property that evaluation requires.