The exponential and the logarithm are inverse on deep units

Let K be a finite extension of ℚ_[p] with absolute ramification index e, and let i be a depth with e < (p - 1) * i. The exponential series converges on 𝓂[K] ^ i (TauCeti.hasSum_exp_of_mem_maximalIdeal_pow) and the logarithm series converges on U(K,i) (TauCeti.hasSum_log_of_mem_unitFiltration_one). This file proves that Mathlib's NormedSpace.exp and NormedSpace.log restrict to mutually inverse bijections

exp : 𝓂[K] ^ i → U(K,i), log : U(K,i) → 𝓂[K] ^ i.

These are the two inverse identities of the deep-unit logarithm: they make exp and log mutually inverse bijections between 𝓂[K] ^ i and U(K,i). Identifying these as groups additionally needs the homomorphism property of the logarithm, which this file does not prove.

Main results

• TauCeti.valuation_exp_sub_one: v(exp x - 1) = v(x) for x ∈ 𝓂[K] ^ i.
• TauCeti.exists_mem_unitFiltration_eq_exp: exp x is a unit in U(K,i) for x ∈ 𝓂[K] ^ i.
• TauCeti.log_exp_of_mem_maximalIdeal_pow: log (exp x) = x for x ∈ 𝓂[K] ^ i.
• TauCeti.exp_log_of_mem_unitFiltration: exp (log u) = u for u ∈ U(K,i).

References

• J. Neukirch, Algebraic Number Theory, Chapter II, Proposition (5.5).

theorem TauCeti.valuation_exp_sub_one {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) (x : ↥(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ i)) : (ValuativeRel.valuation K) (NormedSpace.exp ↑↑x - 1) = (ValuativeRel.valuation K) ↑↑x

On 𝓂[K] ^ i with (p - 1) * i > e, the exponential preserves the valuation of its argument: v(exp x - 1) = v(x).

theorem TauCeti.exists_mem_unitFiltration_eq_exp {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) (x : ↥(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ i)) : ∃ u ∈ unitFiltration K i, ↑u = NormedSpace.exp ↑↑x

On 𝓂[K] ^ i with (p - 1) * i > e, the exponential lands in the unit filtration U(K,i).

theorem TauCeti.log_exp_of_mem_maximalIdeal_pow {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) (x : ↥(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ i)) : NormedSpace.log (NormedSpace.exp ↑↑x) = ↑↑x

The logarithm inverts the exponential on deep elements. On 𝓂[K] ^ i with (p - 1) * i > e, log (exp x) = x.

theorem TauCeti.exp_log_of_mem_unitFiltration {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) : NormedSpace.exp (NormedSpace.log ↑u) = ↑u

The exponential inverts the logarithm on deep units. On U(K,i) with (p - 1) * i > e, exp (log u) = u.