The logarithm on the principal units of a finite extension of ℚ_[p]

Let K be a finite extension of ℚ_[p], with absolute ramification index e. This file studies Mathlib's logarithm NormedSpace.log x = ∑ n, (-1) ^ (n + 1) / n * (x - 1) ^ n on K.

In this overview v_K denotes the normalized additive valuation of K, with v_K(π) = 1 for a uniformizer π, so greater v_K means deeper. The normalized valuation of n in K is v_K(n) = e * padicValNat p n, which grows only logarithmically in n. Hence the series converges on the whole disc v_K(x - 1) ≥ 1, that is on U(K,1): this is TauCeti.hasSum_log_of_mem_unitFiltration_one. The same estimate bounds the difference of two logarithm series uniformly, so the logarithm is continuous on U(K,1).

At a depth i with (p - 1) * i > e, the terms of degree n ≥ 2 are strictly deeper than the linear term, uniformly in the argument: for x, y ∈ 𝓂[K] ^ i one has e * v_p(n) < i * (n - 1), and hence v_K((x ^ n - y ^ n) / n) > v_K(x - y). Summing, the logarithm is an isometry on U(K,i):

v_K(log u - log w) = v_K(u - w) for u, w ∈ U(K,i).

In particular it is injective on U(K,i), and v_K(log u) = v_K(u - 1), so it maps U(K,i) into 𝓂[K] ^ i. These are the analytic inputs for the isomorphism U(K,i) ≃ 𝓂[K] ^ i given by the logarithm, with the exponential as its inverse.

Main results

• TauCeti.hasSum_log_of_mem_unitFiltration_one: the logarithm series converges to NormedSpace.log u for every u ∈ U(K,1).
• TauCeti.continuous_log_unitFiltration: the logarithm is continuous on U(K,i) for i ≥ 1.
• TauCeti.valuation_log_sub_log_sub_sub_lt: on U(K,i) with (p - 1) * i > e, the difference log u - log w agrees with u - w up to strictly deeper terms.
• TauCeti.valuation_log_sub_log: the logarithm is an isometry on U(K,i).
• TauCeti.valuation_log: v(log u) = v(u - 1) on U(K,i), and TauCeti.exists_mem_maximalIdeal_pow_eq_log: log u lies in 𝓂[K] ^ i.
• TauCeti.log_unitFiltration_injective: the logarithm is injective on U(K,i).
• AlgEquiv.map_log: the logarithm commutes with every automorphism of an extension of nonarchimedean local fields.

Implementation notes

The valuation in the statements is Mathlib's multiplicative ValuativeRel.valuation K, for which greater depth means a smaller value; an inequality v_K(a) > v_K(b) above is stated as valuation K a < valuation K b. The depth hypothesis is the integer inequality absoluteRamificationIndex K p < (p - 1) * i, so that no division of natural numbers occurs.

References

• J. Neukirch, Algebraic Number Theory, Chapter II, §5.
• Mathlib's NormedSpace.log (Kevin Buzzard), whose TODO list asks for ultrametric convergence and for ‖log x‖ = ‖x - 1‖; here these are proved for finite extensions of ℚ_[p], the latter on the deep units U(K,i) with (p - 1) * i > e.

theorem TauCeti.hasSum_log_of_mem_unitFiltration_one {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension K p] {u : Kˣ} (hu : u ∈ unitFiltration K 1) : HasSum (fun (n : ℕ) => (-1) ^ (n + 1) / ↑n * (↑u - 1) ^ n) (NormedSpace.log ↑u)

On a finite extension of ℚ_[p], the logarithm series converges to NormedSpace.log u for every principal unit u ∈ U(K,1).

theorem TauCeti.continuous_log_unitFiltration {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension K p] {i : ℕ} (hi : 1 ≤ i) : Continuous fun (u : ↥(unitFiltration K i)) => NormedSpace.log ↑↑u

On a finite extension of ℚ_[p], the logarithm is continuous on U(K,i) for every i ≥ 1.

theorem TauCeti.valuation_log_sub_log_sub_sub_lt {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {p : ℕ} [Fact (Nat.Prime p)] [FinitePadicExtension K p] {i : ℕ} (hi : absoluteRamificationIndex K p < (p - 1) * i) {u w : Kˣ} (hu : u ∈ unitFiltration K i) (hw : w ∈ unitFiltration K i) (huw : u ≠ w) : (ValuativeRel.valuation K) (NormedSpace.log ↑u - NormedSpace.log ↑w - (↑u - ↑w)) < (ValuativeRel.valuation K) (↑u - ↑w)

On U(K,i) with (p - 1) * i > e, the logarithm agrees with the identity up to strictly deeper terms: v(log u - log w - (u - w)) < v(u - w) for u ≠ w, where v is the multiplicative valuation.

theorem TauCeti.valuation_log_sub_log {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {p : ℕ} [Fact (Nat.Prime p)] [FinitePadicExtension K p] {i : ℕ} (hi : absoluteRamificationIndex K p < (p - 1) * i) {u w : Kˣ} (hu : u ∈ unitFiltration K i) (hw : w ∈ unitFiltration K i) : (ValuativeRel.valuation K) (NormedSpace.log ↑u - NormedSpace.log ↑w) = (ValuativeRel.valuation K) (↑u - ↑w)

The logarithm is an isometry on U(K,i) when (p - 1) * i > e.

theorem TauCeti.valuation_log {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {p : ℕ} [Fact (Nat.Prime p)] [FinitePadicExtension K p] {i : ℕ} (hi : absoluteRamificationIndex K p < (p - 1) * i) {u : Kˣ} (hu : u ∈ unitFiltration K i) : (ValuativeRel.valuation K) (NormedSpace.log ↑u) = (ValuativeRel.valuation K) (↑u - 1)

On U(K,i) with (p - 1) * i > e, the logarithm preserves the valuation of u - 1; in particular it maps U(K,i) into 𝓂[K] ^ i (see exists_mem_maximalIdeal_pow_eq_log).

theorem TauCeti.exists_mem_maximalIdeal_pow_eq_log {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {p : ℕ} [Fact (Nat.Prime p)] [FinitePadicExtension K p] {i : ℕ} (hi : absoluteRamificationIndex K p < (p - 1) * i) {u : Kˣ} (hu : u ∈ unitFiltration K i) : ∃ z ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ i, ↑z = NormedSpace.log ↑u

On U(K,i) with (p - 1) * i > e, the logarithm of u is an element of 𝓂[K] ^ i.

theorem TauCeti.log_unitFiltration_injective {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {p : ℕ} [Fact (Nat.Prime p)] [FinitePadicExtension K p] {i : ℕ} (hi : absoluteRamificationIndex K p < (p - 1) * i) : Function.Injective fun (u : ↥(unitFiltration K i)) => NormedSpace.log ↑↑u

The logarithm is injective on U(K,i) when (p - 1) * i > e.

@[simp]

theorem AlgEquiv.map_log {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (σ : Gal(L/K)) (u : L) : σ (NormedSpace.log u) = NormedSpace.log (σ u)

The logarithm is Galois-equivariant. Every K-automorphism of an extension L/K of nonarchimedean local fields (necessarily finite) commutes with the logarithm: σ (log u) = log (σ u). This is RingEquiv.map_log_of_continuous for the homeomorphism σ.