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 nilpotentr : R
, construct a continuous additive character ofℤ_[p]
mapping1
to1 + r
.continuousAddCharEquiv
: for any complete, ultrametric normedℤ_[p]
-algebraR
, the mapaddChar_of_value_at_one
defines a bijection between continuous additive charactersℤ_[p] → R
and topologically nilpotent elements ofR
.continuousAddCharEquiv_of_norm_mul
: if the norm onR
is strictly multiplicative (not just sub-multiplicative), thenaddChar_of_value_at_one
is a bijection between continuous additive charactersℤ_[p] → R
and elements ofR
with‖r‖ < 1
.
## TODO:
- Show that the above equivalences are homeomorphisms, for appropriate choices of the topology.
The unique continuous additive character of ℤ_[p]
mapping 1
to 1 + r
.
Equations
- PadicInt.addChar_of_value_at_one r hr = { toFun := ⇑(PadicInt.mahlerSeries fun (x : ℕ) => r ^ x), map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }
Instances For
Equivalence between continuous additive characters ℤ_[p] → R
, and r ∈ R
with r ^ n → 0
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equivalence between continuous additive characters ℤ_[p] → R
, and r ∈ R
with ‖r‖ < 1
,
for rings with strictly multiplicative norm.