English
There is a natural bijection between the set of continuous additive characters and the set of r in R such that r^n → 0, given by κ ↦ κ(1) − 1 and r ↦ addChar_of_value_at_one r hr.
Русский
Существует естественная биекция между множеством непрерывных аддитивных гармоник и множеством элементов r в R, для которых r^n → 0, задаваемая переходами κ ↦ κ(1) − 1 и r ↦ addChar_of_value_at_one r hr.
LaTeX
$$$$\{ \kappa:\mathrm{AddChar}(\mathbb{Z}_p,R)\mid \mathrm{Continuous}(\kappa)\} \cong \{ r\in R \mid \operatorname{Tendsto}(r^{\cdot})\text{ atTop }(\mathcal{N}_0) \}.$$$$
Lean4
/-- Equivalence between continuous additive characters `ℤ_[p] → R`, and `r ∈ R` with `r ^ n → 0`. -/
noncomputable def continuousAddCharEquiv :
{ κ : AddChar ℤ_[p] R // Continuous κ } ≃ { r : R // Tendsto (r ^ ·) atTop (𝓝 0) }
where
toFun := fun ⟨κ, hκ⟩ ↦ ⟨κ 1 - 1, κ.tendsto_eval_one_sub_pow hκ⟩
invFun := fun ⟨r, hr⟩ ↦ ⟨_, continuous_addChar_of_value_at_one hr⟩
left_inv := fun ⟨κ, hκ⟩ ↦ by simpa using (eq_addChar_of_value_at_one _ hκ (by abel)).symm
right_inv := fun ⟨r, hr⟩ ↦ by simp [addChar_of_value_at_one_def hr]
