The logarithm identifies deep units with a deep additive group

Let K be a finite extension of ℚ_[p] with absolute ramification index e, and let i be a depth with e < (p - 1) * i. On 𝓂[K] ^ i the exponential series converges, and on U(K,i) = 1 + 𝓂[K] ^ i the logarithm series converges; TauCeti.log_exp_of_mem_maximalIdeal_pow and TauCeti.exp_log_of_mem_unitFiltration show that they are mutually inverse bijections.

This file proves that these bijections are group homomorphisms and homeomorphisms, and packages them as an isomorphism of topological groups

deepUnitExpLogEquiv : U(K,i) ≃ₜ* Multiplicative (𝓂[K] ^ i),

given by u ↦ log u, with inverse x ↦ exp x. The homomorphism property comes from the functional equation exp (x + y) = exp x * exp y on 𝓂[K] ^ i: in a nonarchimedean field the Cauchy product of two convergent series converges to the product of their sums, and coefficientwise it is the formal identity PowerSeries.exp_mul_exp_eq_exp_add. Continuity of the exponential comes from its being an isometry of 𝓂[K] ^ i into K, inherited from the isometry property of the logarithm (TauCeti.valuation_log_sub_log).

This isomorphism turns multiplication of deep units into addition on 𝓂[K] ^ i: raising to the n-th power on U(K,i) corresponds to taking the n-fold sum on 𝓂[K] ^ i.

Main results

• TauCeti.valuation_exp_sub_exp: the exponential is an isometry on 𝓂[K] ^ i.
• TauCeti.continuous_exp_maximalIdeal_pow: the exponential is continuous on 𝓂[K] ^ i.
• TauCeti.log_mul_of_mem_unitFiltration: log (u * w) = log u + log w on U(K,i).
• TauCeti.deepUnitExpLogEquiv: the isomorphism of topological groups U(K,i) ≃ₜ* Multiplicative (𝓂[K] ^ i) given by the logarithm, with the exponential as inverse.
• TauCeti.exists_mem_unitFiltration_log_eq_smul: every element of K has a nonzero ℚ_p-multiple which is the logarithm of a unit in U(K,i), a deep unit for large i.

References

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

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

The exponential is an isometry on deep elements. On 𝓂[K] ^ i with (p - 1) * i > e, v(exp x - exp y) = v(x - y).

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

On 𝓂[K] ^ i with (p - 1) * i > e, the exponential is continuous.

theorem TauCeti.log_mul_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 w : Kˣ} (hu : u ∈ unitFiltration K i) (hw : w ∈ unitFiltration K i) : NormedSpace.log (↑u * ↑w) = NormedSpace.log ↑u + NormedSpace.log ↑w

The logarithm is a homomorphism on deep units. On U(K,i) with (p - 1) * i > e, log (u * w) = log u + log w.

noncomputable def TauCeti.deepUnitExpLogEquiv (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) : ↥(unitFiltration K i) ≃ₜ* Multiplicative ↥(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ i)

The deep-unit logarithm. For a finite extension K of ℚ_[p] with absolute ramification index e and a depth i with (p - 1) * i > e, the logarithm is an isomorphism of topological groups U(K,i) ≃ₜ* Multiplicative (𝓂[K] ^ i) from the deep units to the additive group 𝓂[K] ^ i, whose inverse is the exponential.

@[simp]

theorem TauCeti.coe_deepUnitExpLogEquiv_apply {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 : ↥(unitFiltration K i)) : ↑↑(Multiplicative.toAdd ((deepUnitExpLogEquiv K hi) u)) = NormedSpace.log ↑↑u

@[simp]

theorem TauCeti.coe_deepUnitExpLogEquiv_symm_apply {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 : Multiplicative ↥(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ i)) : ↑↑((deepUnitExpLogEquiv K hi).symm x) = NormedSpace.exp ↑↑(Multiplicative.toAdd x)

theorem TauCeti.exists_mem_unitFiltration_log_eq_smul {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [Fact (Nat.Prime p)] [FinitePadicExtension K p] (i : ℕ) (z : K) : ∃ u ∈ unitFiltration K i, ∃ (c : ℚ_[p]), c ≠ 0 ∧ NormedSpace.log ↑u = c • z

Deep logarithms in every direction. For every depth i and every z in K, some nonzero ℚ_p-scalar multiple of z is the logarithm of a unit in U(K,i). No hypothesis relates i to the ramification bound.