Documentation

TauCeti.NumberTheory.LocalField.UnitFiltration.Pow.SubOne

The valuation of x ^ n - 1 in a local field #

Let K be a nonarchimedean local field and write v_K for its normalized additive valuation, read on all of K as WithZero.log ∘ normalizedValuationWithZero K (so that the junk value at 0 is 0). This file computes v_K(x ^ n - 1) for deep principal units and deduces the one-factor estimate for v_K(α ^ b - 1) in a local field of characteristic zero, that is, in a finite extension of ℚ_[p].

For x ∈ U(K,i) at a depth i with v_K(ℓ) < (ℓ - 1) * i for every prime ℓ ∣ n, the n-th power map carries U(K,j) onto U(K, j + v_K(n)) for every j ≥ i and is injective on U(K,i), so it moves the exact depth of x by v_K(n):

v_K(x ^ n - 1) = v_K(x - 1) + v_K(n) for x ≠ 1.

This plays the role of the isometry of the p-adic logarithm on deep units, without any logarithm in the statement.

In characteristic zero, with residue characteristic p and e = v_K(p), every unit α has a power γ = α ^ M in U(K, e + 1), where the formula applies at every exponent. If γ ≠ 1 this gives v_K(α ^ b - 1) ≤ v_K(γ - 1) + e v_p(b). Separating nonunits (where v_K(α ^ b - 1) ≤ 0) and roots of unity (where α ^ b takes only finitely many values) gives, for every fixed α, a constant C with

v_K(α ^ b - 1) ≤ C (1 + log max(1, |b|)) whenever α ^ b ≠ 1.

Main results #

References #

source
theorem TauCeti.log_normalizedValuationWithZero_pow_sub_one {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : ↑n ≠ 0) {i : ℕ} (hi : ∀ (p : ℕ), Nat.Prime p → ∀ (hpK : ↑p ≠ 0), p ∣ n → natCastValuation K p hpK < (p - 1) * i) {x : Kˣ} (hx : x ∈ unitFiltration K i) (hx1 : x ≠ 1) :
((normalizedValuationWithZero K) (↑x ^ n - 1)).log = ((normalizedValuationWithZero K) (↑x - 1)).log + ↑(natCastValuation K n hn)

The valuation of x ^ n - 1 for a deep unit. For (n : K) ≠ 0, a depth i with v_K(p) < (p - 1) * i for every prime p ∣ n, and x ∈ U(K,i) with x ≠ 1,

v_K(x ^ n - 1) = v_K(x - 1) + v_K(n).

source
theorem TauCeti.log_normalizedValuationWithZero_zpow_sub_one_le {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {x : Kˣ} {M i : ℕ} (hi0 : i ≠ 0) (hM : x ^ M ∈ unitFiltration K i) (hM1 : x ^ M ≠ 1) {b : ℤ} (hb : ↑b.natAbs ≠ 0) (hi : ∀ (ℓ : ℕ), Nat.Prime ℓ → ∀ (hℓK : ↑ℓ ≠ 0), ℓ ∣ b.natAbs → natCastValuation K ℓ hℓK < (ℓ - 1) * i) :
((normalizedValuationWithZero K) (↑x ^ b - 1)).log ≤ ((normalizedValuationWithZero K) (↑x ^ M - 1)).log + ↑(natCastValuation K b.natAbs hb)

The one-factor estimate, explicit form. Let x ∈ Kˣ have a power x ^ M ≠ 1 in a positive-depth step U(K,i), and let b be an integer with (|b| : K) ≠ 0 such that v_K(ℓ) < (ℓ - 1) * i for every prime ℓ ∣ b. Then

v_K(x ^ b - 1) ≤ v_K(x ^ M - 1) + v_K(|b|).

source
theorem TauCeti.log_normalizedValuationWithZero_zpow_sub_one_nonpos {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {x : Kˣ} (hx : x ∉ unitFiltration K 0) {b : ℤ} (hb : b ≠ 0) :
((normalizedValuationWithZero K) (↑x ^ b - 1)).log ≤ 0

Nonunits. If x is not a unit of 𝒪[K] and b ≠ 0, then v_K(x ^ b - 1) ≤ 0: a positive valuation would make x ^ b, hence x, a unit.

source
theorem TauCeti.exists_log_normalizedValuationWithZero_zpow_sub_one_le {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] (α : K) :
∃ (C : ℝ), ∀ (b : ℤ), α ^ b ≠ 1 → ↑((normalizedValuationWithZero K) (α ^ b - 1)).log ≤ C * (1 + Real.log (max 1 |↑b|))

The one-factor estimate. Let K be a nonarchimedean local field of characteristic zero, that is, a finite extension of ℚ_[p]. For every fixed α ∈ K there is a constant C, depending on α and K, such that

v_K(α ^ b - 1) ≤ C (1 + log max(1, |b|)) for every integer b with α ^ b ≠ 1.