9.5. Definition of the Coleman map🔗

The example of cyclotomic units suggests a recipe for \zeta_p. Given the construction of \zeta_p from \mu_a and the relation Lemma 9.3.4, one may obtain \zeta_p by: (1) take the tower c(a) of cyclotomic units; (2) form its Coleman series f_{c(a)}; (3) apply \partial\log; (4) apply 1 - \varphi\circ\psi (restriction to \Zpx); (5) apply \partial^{-1} (multiplication by x^{-1} on measures); (6) invert the Mahler transform to land in \Lam(\Zpx); (7) divide by \theta_a. Abstracting steps (2)–(6) gives the following.

Definition9.5.1

Statement uses 4

Statement dependency previews

Preview

Definition 3.3.3

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

Used by 7

Reverse dependency previews

Preview

Theorem 9.5.2

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

The Coleman map is the composite \Col : \sU_\infty \xrightarrow{\ u\mapsto f_u\ } (\Zp[[T]]^{\times})^{\cN=\mathrm{id}} \xrightarrow{\ \partial\log\ } \Zp[[T]] \xrightarrow{\ 1-\varphi\circ\psi\ } \Zp[[T]]^{\psi=0} \xrightarrow{\ \partial^{-1}\ } \Zp[[T]]^{\psi=0} \xrightarrow{\ \cA^{-1}\ } \Lam(\Zpx), where the first map is Coleman's isomorphism Theorem 9.2.2, the second the logarithmic derivative of Proposition 9.3.3, the third measure-theoretic restriction from \Zp to \Zpx, the fourth multiplication by x^{-1}, and the last \cA^{-1} the inverse Mahler transform Definition 3.4.3 landing in the Iwasawa algebra Definition 3.3.3.

Lean code for Definition9.5.1●2 definitions

defdefined in PadicLFunctions/Coleman/Map.lean

complete

def PadicLFunctions.Coleman.Col (p : ℕ) [hp : Fact (Nat.Prime p)]
  (u : PadicLFunctions.Coleman.NormCompatUnits p) :
  PadicMeasure p ℤ_[p]ˣ

def PadicLFunctions.Coleman.Col (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (u :
    PadicLFunctions.Coleman.NormCompatUnits
      p) :
  PadicMeasure p ℤ_[p]ˣ

**RJW Def:coleman map (TeX 2826–2832)**: the Coleman map `Col : 𝒰_∞ → Λ(ℤ_p^×)`,
realised measure-side as `x⁻¹ · Res_{ℤ_p^×}(𝒜⁻¹(∂log f_u))`. Concretely (the §4
`zetaNum` pattern, `unitsCmul (invCM) ((·).comp (extendByZero))`): take the
`ℤ_p`-measure `𝒜⁻¹(∂log f_u)` with Mahler transform `∂log f_u = (1+T)·f_u′·f_u⁻¹`,
precompose with `extendByZero` to land on `ℤ_p^×` (restriction, the `(1−φψ)` arrow,
`iota_comp_extendByZero`), and multiply by `invCM = x⁻¹` (the `∂⁻¹` arrow).

defdefined in PadicLFunctions/Coleman/Map.lean

complete

def PadicLFunctions.Coleman.dlog (p : ℕ) [hp : Fact (Nat.Prime p)]
  (f : PowerSeries ℤ_[p]) : PowerSeries ℤ_[p]

def PadicLFunctions.Coleman.dlog (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (f : PowerSeries ℤ_[p]) :
  PowerSeries ℤ_[p]

The logarithmic derivative `∂log f = (1+T)·f′·f⁻¹` of a power series (RJW §10.2,
the second arrow of Def:coleman map, TeX 2829). For a *unit* `f` (the case of interest,
`colemanSeries_isUnit`) `Ring.inverse f = f⁻¹` is honest; off the units it is the
`Ring.inverse`-junk `0`, which is harmless (`Col` is only ever applied to Coleman
series, which are units).

Theorem9.5.2

uses 0used by 1✓L∃∀N

For any topological generator a of \Zpx, the Kubota–Leopoldt p-adic L-function is recovered as the pseudo-measure \zeta_p = \frac{\Col(c(a))}{\theta_a} \in Q(\Zpx).

Lean code for Theorem9.5.2●2 theorems

theoremdefined in PadicLFunctions/Coleman/Map.lean

complete

theorem PadicLFunctions.Coleman.coleman_to_kl (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) :
  (algebraMap (PadicMeasure p ℤ_[p]ˣ) (PadicMeasure.QuotientField p))
        (PadicMeasure.dirac p ⋯.choose - 1) *
      PadicMeasure.padicZeta p hp2 =
    -(algebraMap (PadicMeasure p ℤ_[p]ˣ) (PadicMeasure.QuotientField p))
        (PadicLFunctions.Coleman.Col p
          (PadicLFunctions.Coleman.cyclo p ⋯ hp2))

theorem PadicLFunctions.Coleman.coleman_to_kl
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (hp2 : p ≠ 2) :
  (algebraMap (PadicMeasure p ℤ_[p]ˣ)
          (PadicMeasure.QuotientField p))
        (PadicMeasure.dirac p ⋯.choose -
          1) *
      PadicMeasure.padicZeta p hp2 =
    -(algebraMap (PadicMeasure p ℤ_[p]ˣ)
          (PadicMeasure.QuotientField p))
        (PadicLFunctions.Coleman.Col p
          (PadicLFunctions.Coleman.cyclo p
            ⋯ hp2))

**RJW thm:coleman to kl (TeX 2836–2841)**, honest-sign form (see the module note and
errata #12): for the chosen integer topological generator `a` of `ℤ_p^×`, the
Kubota–Leopoldt `p`-adic `ζ`-function satisfies `ζ_p = −Col(c(a))/θ_a`, i.e.
`([a] − [1]) · ζ_p = −Col(c(a))` in `Q(ℤ_p^×)`, where `θ_a = [a] − [1]`.

The display at TeX 2839 reads `ζ_p = Col(c(a))/θ_a` (no sign); combined with the notes'
own lem:relate cyclo to mua (TeX 2614, `Res(μ_{∂log f}) = −Res(μ_a)`) and DefZetap (TeX
1568, `ζ_p = (x⁻¹Res μ_a)/θ_a`) this forces the corrected sign — the source drops a
minus (errata #12).

Proof: the defining relation of `ζ_p = mk'(zetaNum a, [a]−1)` is
`([a]−1)·ζ_p = zetaNum a` (`IsLocalization.mk'_spec'`), and `Col(c(a)) = −zetaNum a`
(`Col_cyclo`).

theoremdefined in PadicLFunctions/Coleman/Map.lean

complete

theorem PadicLFunctions.Coleman.Col_cyclo (p : ℕ) [hp : Fact (Nat.Prime p)]
  {a : ℕ} (ha : ¬p ∣ a) (hp2 : p ≠ 2) :
  PadicLFunctions.Coleman.Col p
      (PadicLFunctions.Coleman.cyclo p ha hp2) =
    -PadicMeasure.zetaNum p a

theorem PadicLFunctions.Coleman.Col_cyclo (p : ℕ)
  [hp : Fact (Nat.Prime p)] {a : ℕ}
  (ha : ¬p ∣ a) (hp2 : p ≠ 2) :
  PadicLFunctions.Coleman.Col p
      (PadicLFunctions.Coleman.cyclo p ha
        hp2) =
    -PadicMeasure.zetaNum p a

**The provable core of RJW thm:coleman to kl**: `Col(c(a)) = −zetaNum a`, where
`zetaNum a = x⁻¹·Res_{ℤ_p^×}(μ_a)` is the numerator of `ζ_p`. The Mahler-inverse of
`∂log f_{c(a)} = (a−1) − F_a` (`colemanSeries_cyclo`, `dlog_geomSum`) has units-measure
`(𝒜⁻¹((a−1)−F_a)).comp extendByZero = −muAUnits a` (its `ι`-image is
`Res(𝒜⁻¹((a−1)−F_a)) = −Res(μ_a) = ι(−muAUnits a)` by `iota_comp_extendByZero` +
`res_derivative_log_geomSum` + `iota_muAUnits`, and `ι` is injective); then `unitsCmul`
linearity (`unitsCmul_neg`) gives `Col(c(a)) = unitsCmul invCM (−muAUnits a) = −zetaNum a`.
The minus is RJW lem:relate cyclo to mua (TeX 2614).

Proof for Theorem 9.5.2

Proof uses 8

Proof dependency previews

Preview

Definition 3.6.1

Loading preview

Proof dependency preview content is loaded from the Blueprint HTML cache.

Track the cyclotomic tower c(a) Definition 9.3.1 through the Coleman map Definition 9.5.1 one step at a time. Its Coleman series is f_{c(a)} = ((1+T)^a-1)/T Lemma 9.3.2, and applying \partial\log produces the series a - 1 - F_a Proposition 9.3.3, the measure-theoretic incarnation of \mu_{\partial\log f_{c(a)}}. Restricting to \Zpx by 1 - \varphi\circ\psi and using \Res_{\Zpx}(\mu_{\partial\log f_{c(a)}}) = -\Res_{\Zpx}(\mu_a) Lemma 9.3.4 turns this into -\Res_{\Zpx}(\mu_a). The fourth step \partial^{-1} is multiplication by x^{-1} on measures, so after inverting the Mahler transform we arrive at \Col(c(a)) = -\,x^{-1}\,\Res_{\Zpx}(\mu_a) \in \Lam(\Zpx). Comparing with the construction \zeta_p = x^{-1}\Res_{\Zpx}(\mu_a)/\theta_a Definition 4.1.4 Definition 4.3.2, the single accumulated sign is the very factor of -1 carried by the normaliser \theta_a, so dividing \Col(c(a)) by \theta_a yields exactly \zeta_p. Since \theta_a is not a unit, the quotient lives only in the fraction field Q(\Zpx), exhibiting \zeta_p as a pseudo-measure Definition 3.6.1 with its pole at s=1; the division also cancels the dependence on the choice of topological generator a.