A valuation on a power of a spanned ideal

If v ≤ δ on a generating set s and v ≤ 1 on the ideal Ideal.span s, then v ≤ δ ^ n on Ideal.span s ^ (n + 1).

s is an arbitrary Set R: the bound needs no finiteness. Finiteness enters only at the intended call site, Wedhorn's Theorem 7.10, where δ is chosen as the maximum of v over a finite generating set of an ideal of definition — a maximum that needs the set to be finite, whereas this bound does not.

Why the two hypotheses, and why the shift

Both are needed and neither can be dropped. An element of Ideal.span s ^ (n + 1) is a sum of terms c * t₀ * ⋯ * tₙ with tᵢ ∈ s and the coefficient c arbitrary, so a bound on the generators alone says nothing: v c can be as large as it likes. The trick is to attach the coefficient to one generator — c * t₀ lies in the ideal, so v (c * t₀) ≤ 1 — and to bound the remaining n bare generators by δ each. That is exactly where the shift comes from: n + 1 factors give δ ^ n, because one of them is spent absorbing the coefficient.

It is also why the proof does not simply induct along I ^ (n + 1) = I ^ n * I: splitting off an element of I rather than a generator only ever yields the bound 1, so the exponent never grows. Instead the power is rewritten as the span of the pointwise power s ^ n (Submodule.span_pow), which keeps the generators visible.

Main results

• Valuation.map_le_pow_of_mem_span_pow_succ

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Theorem 7.10.

theorem Valuation.map_le_pow_of_mem_span_pow_succ {R : Type u_1} [CommRing R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {s : Set R} {δ : Γ₀} (hs : ∀ t ∈ s, v t ≤ δ) (h1 : ∀ a ∈ Ideal.span s, v a ≤ 1) {n : ℕ} {a : R} (ha : a ∈ Ideal.span s ^ (n + 1)) : v a ≤ δ ^ n

A valuation on a power of a span. If v ≤ δ on a generating set s and v ≤ 1 on Ideal.span s, then v ≤ δ ^ n on Ideal.span s ^ (n + 1).

One of the n + 1 factors is spent absorbing the arbitrary coefficient, which is why the exponent on the right is n and not n + 1; see the module docstring.