Documentation

Mathlib.NumberTheory.Padics.AddChar

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:

## TODO:

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} ( : 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)) :

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

Equations
Instances For
    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.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} ( : Continuous κ) (hκ' : κ 1 = 1 + r) :
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[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} ( : Continuous κ) :
      ((continuousAddCharEquiv p R) κ, ) = κ 1 - 1

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

      Equations
      Instances For