Powers of deep units

Let K be a nonarchimedean local field, let n be a natural number with (n : K) ≠ 0, and write v_K(n) for its normalized valuation natCastValuation K n hn. This file shows that at every depth i with v_K(p) < (p - 1) * i for each prime p ∣ n, in particular at every depth i > v_K(n), the n-th power map is an isomorphism of the unit filtration step U(K,i) onto U(K, i + v_K(n)):

• it maps U(K,i) onto U(K, i + v_K(n));
• it is injective on U(K,i), that is, U(K,i) contains no nontrivial n-th root of unity.

For a prime p the depth condition is the usual v_K(p) < (p - 1) * i, stated as an integer inequality so that no division of natural numbers occurs. When p is not the residue characteristic, v_K(p) = 0 and the condition is just i ≥ 1.

The argument is the binomial expansion: for x ∈ 𝓂[K] ^ i,

(1 + x) ^ p = 1 + p x + r, with v_K(r) > v_K(p x),

because the middle binomial coefficients are divisible by p and v_K(x ^ p) = p v_K(x) exceeds v_K(p x) = v_K(p) + v_K(x) exactly under the threshold. Hence (1 + x) ^ p ≡ 1 + p x modulo 𝓂[K] ^ (i + v_K(p) + 1). This gives the inclusion U(K,i) ^ p ⊆ U(K, i + v_K(p)) and the injectivity at once. For the reverse inclusion the congruence shows that every element of U(K, j + v_K(p)) is a p-th power of an element of U(K,j) up to U(K, j + v_K(p) + 1). Iterating, U(K, i + v_K(p)) lies in U(K,i) ^ p · U(K,m) for every m, hence in the closure of U(K,i) ^ p, which is closed as the image of the compact set U(K,i). The general exponent follows by induction on the prime factorization of n.

In mixed characteristic this is the input that computes the p-primary part of the power classes Kˣ ⧸ (Kˣ)ⁿ (TauCeti.card_powerClasses): it identifies the deep subgroup U(K,i) ^ n of (Kˣ)ⁿ with a step of the filtration, which is open in Kˣ.

Main results

• TauCeti.map_powMonoidHom_unitFiltration_of_prime: for v_K(p) < (p - 1) * i, U(K,i) ^ p = U(K, i + v_K(p)).
• TauCeti.disjoint_rootsOfUnity_unitFiltration_of_prime: for v_K(p) < (p - 1) * i, the group U(K,i) contains no nontrivial p-th root of unity.
• TauCeti.map_powMonoidHom_unitFiltration: if v_K(p) < (p - 1) * i for every prime p ∣ n, then U(K,i) ^ n = U(K, i + v_K(n)).
• TauCeti.unitFiltration_le_range_powMonoidHom: under the same depth condition, every unit in U(K, i + v_K(n)) is an n-th power.
• TauCeti.disjoint_rootsOfUnity_unitFiltration: under the same depth condition, the group U(K,i) contains no nontrivial n-th root of unity.

References

• J.-P. Serre, Corps Locaux, Chapter XIV, §4, Proposition 9.
• J. Neukirch, Algebraic Number Theory, Chapter II, §5.

theorem TauCeti.map_powMonoidHom_unitFiltration_of_prime {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {p : ℕ} (hp : Nat.Prime p) (hpK : ↑p ≠ 0) {i : ℕ} (hi : natCastValuation K p hpK < (p - 1) * i) : Subgroup.map (powMonoidHom p) (unitFiltration K i) = unitFiltration K (i + natCastValuation K p hpK)

Deep units are p-th powers. For a prime p with (p : K) ≠ 0 and a depth i with v_K(p) < (p - 1) * i, the p-th power map carries U(K,i) onto U(K, i + v_K(p)).

theorem TauCeti.disjoint_rootsOfUnity_unitFiltration_of_prime {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {p : ℕ} (hp : Nat.Prime p) (hpK : ↑p ≠ 0) {i : ℕ} (hi : natCastValuation K p hpK < (p - 1) * i) : Disjoint (rootsOfUnity p K) (unitFiltration K i)

Deep units carry no p-torsion. For a prime p with (p : K) ≠ 0 and a depth i with v_K(p) < (p - 1) * i, the only p-th root of unity in U(K,i) is 1.

theorem TauCeti.map_powMonoidHom_unitFiltration {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) : Subgroup.map (powMonoidHom n) (unitFiltration K i) = unitFiltration K (i + natCastValuation K n hn)

Deep units are n-th powers. For (n : K) ≠ 0 and a depth i with v_K(p) < (p - 1) * i for every prime p ∣ n, the n-th power map carries U(K,i) onto U(K, i + v_K(n)). The depth condition holds in particular for every i > v_K(n), by natCastValuation_lt_sub_one_mul_of_lt_of_dvd.

theorem TauCeti.unitFiltration_le_range_powMonoidHom {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) : unitFiltration K (i + natCastValuation K n hn) ≤ (powMonoidHom n).range

Under the depth condition of map_powMonoidHom_unitFiltration, every unit in U(K, i + v_K(n)) is an n-th power in Kˣ.

theorem TauCeti.disjoint_rootsOfUnity_unitFiltration {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) : Disjoint (rootsOfUnity n K) (unitFiltration K i)

Deep units carry no n-torsion. For (n : K) ≠ 0 and a depth i with v_K(p) < (p - 1) * i for every prime p ∣ n, the only n-th root of unity in U(K,i) is 1. The depth condition holds in particular for every i > v_K(n), by natCastValuation_lt_sub_one_mul_of_lt_of_dvd.