Additive characters of ℤ_[p]

We show that for any complete, ultrametric normed ℤ_[p]-algebra R, there is a bijection between continuous additive characters ℤ_[p] → R and topologically nilpotent elements of R, given by sending κ to the element κ 1 - 1. This is used to define the Mahler transform for p-adic measures.

Note that if the norm on R is not strictly multiplicative, then the condition that κ 1 - 1 be topologically nilpotent is strictly weaker than assuming ‖κ 1 - 1‖ < 1, although they are equivalent if NormMulClass R holds.

## Main definitions and theorems:

• addChar_of_value_at_one: given a topologically nilpotent r : R, construct a continuous additive character of ℤ_[p] mapping 1 to 1 + r.
• continuousAddCharEquiv: for any complete, ultrametric normed ℤ_[p]-algebra R, the map addChar_of_value_at_one defines a bijection between continuous additive characters ℤ_[p] → R and topologically nilpotent elements of R.
• continuousAddCharEquiv_of_norm_mul: if the norm on R is strictly multiplicative (not just sub-multiplicative), then addChar_of_value_at_one is a bijection between continuous additive characters ℤ_[p] → R and elements of R with ‖r‖ < 1.

## TODO:

• Show that the above equivalences are homeomorphisms, for appropriate choices of the topology.

theorem AddChar.tendsto_eval_one_sub_pow {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedRing R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] {κ : AddChar ℤ_[p] R} (hκ : Continuous ⇑κ) : Filter.Tendsto (fun (n : ℕ) => (κ 1 - 1) ^ n) Filter.atTop (nhds 0)

noncomputable def PadicInt.addChar_of_value_at_one {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedRing R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] (r : R) (hr : Filter.Tendsto (fun (x : ℕ) => r ^ x) Filter.atTop (nhds 0)) : AddChar ℤ_[p] R

The unique continuous additive character of ℤ_[p] mapping 1 to 1 + r.

theorem PadicInt.continuous_addChar_of_value_at_one {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedRing R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] {r : R} (hr : Filter.Tendsto (fun (x : ℕ) => r ^ x) Filter.atTop (nhds 0)) : Continuous ⇑(addChar_of_value_at_one r hr)

theorem PadicInt.coe_addChar_of_value_at_one {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedRing R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] {r : R} (hr : Filter.Tendsto (fun (x : ℕ) => r ^ x) Filter.atTop (nhds 0)) : ⇑(addChar_of_value_at_one r hr) = ⇑(mahlerSeries fun (x : ℕ) => r ^ x)

@[simp]

theorem PadicInt.addChar_of_value_at_one_def {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedRing R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] {r : R} (hr : Filter.Tendsto (fun (x : ℕ) => r ^ x) Filter.atTop (nhds 0)) : (addChar_of_value_at_one r hr) 1 = 1 + r

theorem PadicInt.eq_addChar_of_value_at_one {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedRing R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] {r : R} (hr : Filter.Tendsto (fun (x : ℕ) => r ^ x) Filter.atTop (nhds 0)) {κ : AddChar ℤ_[p] R} (hκ : Continuous ⇑κ) (hκ' : κ 1 = 1 + r) : κ = addChar_of_value_at_one r hr

noncomputable def PadicInt.continuousAddCharEquiv (p : ℕ) [Fact (Nat.Prime p)] (R : Type u_1) [NormedRing R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] : { κ : AddChar ℤ_[p] R // Continuous ⇑κ } ≃ { r : R // Filter.Tendsto (fun (x : ℕ) => r ^ x) Filter.atTop (nhds 0) }

Equivalence between continuous additive characters ℤ_[p] → R, and r ∈ R with r ^ n → 0.

@[simp]

theorem PadicInt.continuousAddCharEquiv_apply {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedRing R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] {κ : AddChar ℤ_[p] R} (hκ : Continuous ⇑κ) : ↑((continuousAddCharEquiv p R) ⟨κ, hκ⟩) = κ 1 - 1

@[simp]

theorem PadicInt.continuousAddCharEquiv_symm_apply {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedRing R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] {r : R} (hr : Filter.Tendsto (fun (x : ℕ) => r ^ x) Filter.atTop (nhds 0)) : ↑((continuousAddCharEquiv p R).symm ⟨r, hr⟩) = addChar_of_value_at_one r hr

noncomputable def PadicInt.continuousAddCharEquiv_of_norm_mul (p : ℕ) [Fact (Nat.Prime p)] (R : Type u_1) [NormedRing R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] [NormMulClass R] : { κ : AddChar ℤ_[p] R // Continuous ⇑κ } ≃ { r : R // ‖r‖ < 1 }

Equivalence between continuous additive characters ℤ_[p] → R, and r ∈ R with ‖r‖ < 1, for rings with strictly multiplicative norm.

@[simp]

theorem PadicInt.continuousAddCharEquiv_of_norm_mul_apply {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedRing R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] [NormMulClass R] {κ : AddChar ℤ_[p] R} (hκ : Continuous ⇑κ) : ↑((continuousAddCharEquiv_of_norm_mul p R) ⟨κ, hκ⟩) = κ 1 - 1

@[simp]

theorem PadicInt.continuousAddCharEquiv_of_norm_mul_symm_apply {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [NormedRing R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] [NormMulClass R] {r : R} (hr : ‖r‖ < 1) : ↑((continuousAddCharEquiv_of_norm_mul p R).symm ⟨r, hr⟩) = addChar_of_value_at_one r ⋯