The valuation of a difference of powers

For a valuation v on a commutative ring and elements x, y with v x ≤ c and v y ≤ c, the factorization x ^ n - y ^ n = (x - y) * ∑ j < n, x ^ j * y ^ (n - 1 - j) and the ultrametric inequality give

v (x ^ n - y ^ n) ≤ v (x - y) * c ^ (n - 1).

This estimate controls the nonlinear terms of a power series on sufficiently deep inputs; for instance, it shows that the logarithm is an isometry on the deep units of a local field.

The exact formulas here say that powers with unit exponent preserve the distance of a principal unit from one, and compute differences of integer powers after translation by an element of smaller valuation. These give the displacement orders of explicit uniformizers in wildly ramified Artin--Schreier extensions.

theorem Valuation.map_pow_sub_pow_le {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x y : R} {c : Γ₀} (hx : v x ≤ c) (hy : v y ≤ c) (n : ℕ) : v (x ^ n - y ^ n) ≤ v (x - y) * c ^ (n - 1)

If v x ≤ c and v y ≤ c, then v (x ^ n - y ^ n) ≤ v (x - y) * c ^ (n - 1).

@[simp]

theorem Valuation.map_one_add_pow_sub_one {R : Type u_1} {Γ₀ : Type u_2} [CommRing R] [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) {x : R} (hx : v x < 1) (n : ℕ) (hn : v ↑n = 1) : v ((1 + x) ^ n - 1) = v x

Raising a principal unit to a natural power of valuation one preserves its distance from one.

@[simp]

theorem Valuation.map_one_add_zpow_sub_one {F : Type u_3} {Γ₁ : Type u_4} [Field F] [LinearOrderedCommGroupWithZero Γ₁] (v : Valuation F Γ₁) {x : F} (hx : v x < 1) (n : ℤ) (hn : v ↑n = 1) : v ((1 + x) ^ n - 1) = v x

Raising a principal unit to an integer power of valuation one preserves its distance from one, including negative powers.

@[simp]

theorem Valuation.map_add_zpow_sub_zpow {F : Type u_3} {Γ₁ : Type u_4} [Field F] [LinearOrderedCommGroupWithZero Γ₁] (v : Valuation F Γ₁) {y c : F} (hc : v c < v y) (n : ℤ) (hn : v ↑n = 1) : v ((y + c) ^ n - y ^ n) = v y ^ (n - 1) * v c

Translating by an element of smaller valuation gives the exact valuation of the difference of integer powers, when the exponent has valuation one.