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.
• TauCeti.pow_mem_unitFiltration_add_natCastValuation_iff: under the same depth condition, the n-th power map shifts every deeper step by exactly v_K(n) on U(K,i).
• TauCeti.map_powMonoidHom_unitFiltration_succ_of_isUnit: when n is invertible in 𝒪[K], the n-th power map carries every positive-depth step onto itself.
• TauCeti.powMonoidHom_unitFiltration_succ_bijective_of_isUnit: the same map is a bijection.
• TauCeti.pow_mem_unitFiltration_succ_iff_of_isUnit: on principal units, taking n-th powers detects membership in each positive-depth step.

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.

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

Powers shift deep steps exactly. For (n : K) ≠ 0, a depth i with v_K(p) < (p - 1) * i for every prime p ∣ n, and x ∈ U(K,i), the power x ^ n lies in U(K, j + v_K(n)) exactly when x lies in U(K,j), for every j. Thus the n-th power map moves the exact depth of every x ∈ U(K,i) by v_K(n).

theorem TauCeti.map_powMonoidHom_unitFiltration_succ_of_isUnit {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) (i : ℕ) : Subgroup.map (powMonoidHom n) (unitFiltration K (i + 1)) = unitFiltration K (i + 1)

For n invertible in 𝒪[K], the n-th power map carries each positive-depth step U(K,i+1) of the unit filtration onto itself. This is the case v_K(n) = 0 of map_powMonoidHom_unitFiltration.

theorem TauCeti.disjoint_rootsOfUnity_unitFiltration_one_of_isUnit {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) : Disjoint (rootsOfUnity n K) (unitFiltration K 1)

For n invertible in 𝒪[K], the only n-th root of unity in K that is a principal unit is 1: the groups μ_n(K) and U(K,1) intersect trivially. This is the case v_K(n) = 0 of disjoint_rootsOfUnity_unitFiltration.

theorem TauCeti.powMonoidHom_unitFiltration_succ_bijective_of_isUnit {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) (i : ℕ) : Function.Bijective ⇑(powMonoidHom n)

For n invertible in 𝒪[K], the n-th power map is a bijection of each positive-depth step U(K,i+1) of the unit filtration.

theorem TauCeti.pow_mem_unitFiltration_succ_iff_of_isUnit {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) {x : Kˣ} (hx : x ∈ unitFiltration K 1) (i : ℕ) : x ^ n ∈ unitFiltration K (i + 1) ↔ x ∈ unitFiltration K (i + 1)

For n invertible in 𝒪[K], the n-th power map detects depth on principal units: for x ∈ U(K,1), x ^ n ∈ U(K,i+1) exactly when x ∈ U(K,i+1).