9.4. Proof of Coleman's theorem🔗

We prove the precise form of Theorem 9.2.2. The strategy: identify the image as the \cN-invariants, where \cN is a norm operator on power series that mirrors the field norm; then a continuity property of \cN lets a diagonal argument produce the interpolating series.

Lemma9.4.1

uses 0

Used by 4

Reverse dependency previews

Preview

Theorem 9.2.2

Loading preview

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

✓L∃∀N

Suppose u = (u_n) \in \sU_\infty and f, g \in \Zp[[T]]^{\times} both satisfy f(\pi_n) = g(\pi_n) = u_n for all n \ge 1. Then f = g.

Lean code for Lemma9.4.1●1 theorem

theoremdefined in PadicLFunctions/Coleman/Theorem.lean

complete

theorem PadicLFunctions.Coleman.evalPi_injective (p : ℕ)
  [hp : Fact (Nat.Prime p)] {f g : PowerSeries ℤ_[p]}
  (h :
    ∀ (n : ℕ),
      1 ≤ n →
        PadicLFunctions.Coleman.evalPi p f n =
          PadicLFunctions.Coleman.evalPi p g n) :
  f = g

theorem PadicLFunctions.Coleman.evalPi_injective
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  {f g : PowerSeries ℤ_[p]}
  (h :
    ∀ (n : ℕ),
      1 ≤ n →
        PadicLFunctions.Coleman.evalPi p f
            n =
          PadicLFunctions.Coleman.evalPi p
            g n) :
  f = g

**Uniqueness of the interpolating series** (RJW lem:unique-coleman, TeX 2635–2642):
a `ℤ_p`-power series is determined by its values at the uniformisers `π_n`, `n ≥ 1`.

Proof (the source's Weierstrass argument, TeX 2641): suppose `d := f − g ≠ 0`. By
`evalPi`-linearity (`evalPi_sub`) `d(π_n) = 0` for all `n ≥ 1`. Normalise
`d = C(p^m) · d'` with `d' mod p ≠ 0` (`exists_C_pow_mul`), then apply mathlib's
Weierstrass preparation (`exists_isWeierstrassFactorization`, available since `ℤ_p`
is a complete local ring with maximal ideal `(p)`) to factor `d' = r · u` with `r`
a distinguished (monic) polynomial and `u` a unit. Evaluating at `π_n`: the
constant `toCp(p^m) ≠ 0` and the unit value `u(π_n) ≠ 0` peel off, so the mapped
polynomial `r.map toCp ∈ ℂ_p[X]` (nonzero, being monic) vanishes at every `π_n`.
But the `π_n` (`n ≥ 1`) are infinitely many distinct points (`pi_norm_injective`),
so the polynomial has infinitely many roots, hence is zero — contradiction.

Proof for Lemma 9.4.1

uses 0

By the Weierstrass preparation theorem any nonzero h \in \Zp[[T]] factors as h = p^m\,u(T)\,r(T) with u a unit and r a distinguished polynomial. Such an h converges on the maximal ideal of the ring of integers of \Qpbar, and since the unit factor has no zeros there, h has only finitely many zeros in that maximal ideal. Apply this to h = f - g: it vanishes at the infinitely many distinct points \pi_n (which lie in the maximal ideal), forcing f - g = 0.

We now build the norm operator. Recall \varphi acts on \Zp[[T]] by \varphi(f)(T) = f((1+T)^p - 1), is injective, and satisfies the key identity \varphi(f)(\pi_{n+1}) = f((\pi_{n+1}+1)^p - 1) = f(\xi_{p^{n+1}}^p - 1) = f(\pi_n). Its measure-theoretic adjoint \psi satisfies (\varphi\circ\psi)(f)(T) = \tfrac1p\sum_{\eta \in \mu_p} f(\eta(1+T) - 1); we call \psi the trace operator.

Lemma9.4.2

uses 0used by 1✓L∃∀N

There is a unique multiplicative operator \cN on \Zp[[T]], the norm operator, such that (\varphi\circ\cN)(f)(T) = \prod_{\eta \in \mu_p} f(\eta(1+T) - 1). Being multiplicative, \cN preserves \Zp[[T]]^{\times}.

Lean code for Lemma9.4.2●3 declarations

defdefined in PadicLFunctions/Coleman/NormOperator.lean

complete

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

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

W6b/T906: the norm operator `𝒩 : ℤ_p⟦T⟧ → ℤ_p⟦T⟧`, defined as the relative
norm `N_{B/A}` of the free rank-`p` φ-algebra `B = ℤ_p⟦T⟧` over `A = φ(ℤ_p⟦T⟧)`
(`Algebra.norm` along `PhiAlg`). RJW TeX 2654–2660.

The norm lands in the base ring `A`, which (under the φ-iso `A ≅ ℤ_p⟦T⟧`) we
identify with `ℤ_p⟦T⟧`: no `φ⁻¹` is needed here — the source's `φ⁻¹` is an
artifact of viewing `A` as a subring of `B`, whereas `Algebra.norm` already
takes values in the abstract base.

theoremdefined in PadicLFunctions/Coleman/NormOperator.lean

complete

theorem PadicLFunctions.Coleman.normOp_mul {p : ℕ} [hp : Fact (Nat.Prime p)]
  (f g : PowerSeries ℤ_[p]) :
  PadicLFunctions.Coleman.normOp (f * g) =
    PadicLFunctions.Coleman.normOp f * PadicLFunctions.Coleman.normOp g

theorem PadicLFunctions.Coleman.normOp_mul {p : ℕ}
  [hp : Fact (Nat.Prime p)]
  (f g : PowerSeries ℤ_[p]) :
  PadicLFunctions.Coleman.normOp (f * g) =
    PadicLFunctions.Coleman.normOp f *
      PadicLFunctions.Coleman.normOp g

`𝒩` is multiplicative (the relative norm is a monoid hom). RJW TeX 2660.

theoremdefined in PadicLFunctions/Coleman/NormOperator.lean

complete

theorem PadicLFunctions.Coleman.normOp_eq_det {p : ℕ} [hp : Fact (Nat.Prime p)]
  (f : PowerSeries ℤ_[p]) :
  PadicLFunctions.Coleman.normOp f =
    (PadicLFunctions.Coleman.digitMatrix f).det

theorem PadicLFunctions.Coleman.normOp_eq_det
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  (f : PowerSeries ℤ_[p]) :
  PadicLFunctions.Coleman.normOp f =
    (PadicLFunctions.Coleman.digitMatrix
        f).det

W6b/T906 (the determinant characterisation, replan R10.4): `𝒩f` is the
determinant of the multiplication-by-`f` matrix in the digit basis. (The
`μ_p`-product formula `φ(𝒩f) = ∏_ξ f((1+T)ξ−1)` is NOT a formal identity — the
substitution `(1+T)ξ−1` has non-nilpotent constant term for `ξ ≠ 1`; the
evaluated form is the commuting square of T907.)

Proof for Lemma 9.4.2

uses 0

Let B = \Zp[[T]] and A = \varphi(\Zp[[T]]) = \Zp[[(1+T)^p - 1]]. Then B/A is a degree-p extension, obtained by adjoining a pth root of (1+T)^p to A; its automorphisms over A are T \mapsto \eta(1+T) - 1 for \eta \in \mu_p. The field/ring norm N_{B/A}(f) = \prod_{\eta\in\mu_p} f(\eta(1+T)-1) lands in A = \varphi(\Zp[[T]]), so we may set \cN := \varphi^{-1}\circ N_{B/A}, using injectivity of \varphi. Uniqueness and multiplicativity follow from those of N_{B/A} and injectivity of \varphi.

Analogously \psi = p^{-1}\varphi^{-1}\circ\Tr_{B/A} is built from the trace of B/A, explaining the terminology. The point of \cN is that it mirrors the field norm N_{n+1,n} defining \sU_\infty.

Lemma9.4.3

uses 0

Used by 2

Reverse dependency previews

Preview

Proposition 9.4.4

Loading preview

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

✓L∃∀N

The square \begin{array}{ccc} \Zp[[T]]^{\times} & \xrightarrow{\ f\mapsto f(\pi_{n+1})\ } & \sU_{n+1} \\ \downarrow{\scriptstyle\cN} & & \downarrow{\scriptstyle N_{n+1,n}} \\ \Zp[[T]]^{\times} & \xrightarrow{\ f\mapsto f(\pi_n)\ } & \sU_n \end{array} commutes; i.e. N_{n+1,n}(f(\pi_{n+1})) = (\cN f)(\pi_n) for all f \in \Zp[[T]]^{\times}.

Lean code for Lemma9.4.3●1 theorem

theoremdefined in PadicLFunctions/Coleman/Theorem.lean

complete

theorem PadicLFunctions.Coleman.evalPi_normOp {p : ℕ} [hp : Fact (Nat.Prime p)]
  (f : PowerSeries ℤ_[p]) {n : ℕ} (hn : 1 ≤ n) :
  PadicLFunctions.Coleman.evalPi p (PadicLFunctions.Coleman.normOp f)
      n =
    PadicLFunctions.Coleman.levelNorm p n
      (PadicLFunctions.Coleman.evalPi p f (n + 1))

theorem PadicLFunctions.Coleman.evalPi_normOp
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  (f : PowerSeries ℤ_[p]) {n : ℕ}
  (hn : 1 ≤ n) :
  PadicLFunctions.Coleman.evalPi p
      (PadicLFunctions.Coleman.normOp f)
      n =
    PadicLFunctions.Coleman.levelNorm p n
      (PadicLFunctions.Coleman.evalPi p f
        (n + 1))

**The evaluation/norm commuting square** (T907, RJW lem:norm power series vs units,
TeX 2673–2692): for `n ≥ 1`,
`evalPi (𝒩 f) n = N_{n+1,n}(evalPi f (n+1))` — i.e. evaluating the norm operator at
`π_n` equals the level-norm of the value at `π_{n+1}`. The determinant route (R10.4):
`evalPi (𝒩 f) n = evalPi (det (digitMatrix f)) n = det ((evalPiHom).mapMatrix M)`
(`RingHom.map_det`); the mapped matrix is (entrywise, by `leftMulMatrix_zetaBasis_coe`)
the `K_n ↪ ℂ_p`-image of the multiplication-by-`evalPi f (n+1)` matrix in the
`ξ_{n+1}`-power basis, whose determinant is `Algebra.norm (= levelNorm)`. No `p`-odd
hypothesis is needed.

Proof for Lemma 9.4.3

uses 1

For f \in \Zp[[T]]^{\times} we have f(\pi_n) \in \sU_n (its inverse is f^{-1}(\pi_n), also integral), so the horizontal maps land in units. Since the minimal polynomial of \xi_{p^{n+1}} over K_n is X^p - \xi_{p^n}, the conjugates of \xi_{p^{n+1}} are \eta\,\xi_{p^{n+1}}, \eta \in \mu_p. Hence N_{n+1,n}(f(\pi_{n+1})) = \prod_{\eta\in\mu_p} f(\eta\xi_{p^{n+1}} - 1) = (\varphi\circ\cN)(f)(\pi_{n+1}) = (\cN f)(\pi_n), using Lemma 9.4.2 for the middle equality and \varphi(g)(\pi_{n+1}) = g(\pi_n) for the last.

Proposition9.4.4

uses 0used by 1✓L∃∀N

The map R : (\Zp[[T]]^{\times})^{\cN = \mathrm{id}} \hookrightarrow \sU_\infty, \qquad f \mapsto (f(\pi_n))_n is well defined and injective.

Lean code for Proposition9.4.4●2 theorems

theoremdefined in PadicLFunctions/Coleman/Theorem.lean

complete

theorem PadicLFunctions.Coleman.evalPi_mem_O (p : ℕ) [hp : Fact (Nat.Prime p)]
  (f : PowerSeries ℤ_[p]) {n : ℕ} (hn : 1 ≤ n) :
  PadicLFunctions.Coleman.evalPi p f n ∈ PadicLFunctions.Coleman.O p n

theorem PadicLFunctions.Coleman.evalPi_mem_O
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (f : PowerSeries ℤ_[p]) {n : ℕ}
  (hn : 1 ≤ n) :
  PadicLFunctions.Coleman.evalPi p f n ∈
    PadicLFunctions.Coleman.O p n

**Integrality** (RJW §9): `f(π_n) ∈ 𝒪_n` for `n ≥ 1`. Two halves:
`‖f(π_n)‖ ≤ 1` (ultrametric `tsum` bound, each term `‖coeff_k · π_n^k‖ ≤ 1`) and
`f(π_n) ∈ K_n` (limit of the `K_n`-valued partial sums, `K_n` being closed).

theoremdefined in PadicLFunctions/Coleman/Theorem.lean

complete

theorem PadicLFunctions.Coleman.evalPi_injective (p : ℕ)
  [hp : Fact (Nat.Prime p)] {f g : PowerSeries ℤ_[p]}
  (h :
    ∀ (n : ℕ),
      1 ≤ n →
        PadicLFunctions.Coleman.evalPi p f n =
          PadicLFunctions.Coleman.evalPi p g n) :
  f = g

theorem PadicLFunctions.Coleman.evalPi_injective
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  {f g : PowerSeries ℤ_[p]}
  (h :
    ∀ (n : ℕ),
      1 ≤ n →
        PadicLFunctions.Coleman.evalPi p f
            n =
          PadicLFunctions.Coleman.evalPi p
            g n) :
  f = g

**Uniqueness of the interpolating series** (RJW lem:unique-coleman, TeX 2635–2642):
a `ℤ_p`-power series is determined by its values at the uniformisers `π_n`, `n ≥ 1`.

Proof (the source's Weierstrass argument, TeX 2641): suppose `d := f − g ≠ 0`. By
`evalPi`-linearity (`evalPi_sub`) `d(π_n) = 0` for all `n ≥ 1`. Normalise
`d = C(p^m) · d'` with `d' mod p ≠ 0` (`exists_C_pow_mul`), then apply mathlib's
Weierstrass preparation (`exists_isWeierstrassFactorization`, available since `ℤ_p`
is a complete local ring with maximal ideal `(p)`) to factor `d' = r · u` with `r`
a distinguished (monic) polynomial and `u` a unit. Evaluating at `π_n`: the
constant `toCp(p^m) ≠ 0` and the unit value `u(π_n) ≠ 0` peel off, so the mapped
polynomial `r.map toCp ∈ ℂ_p[X]` (nonzero, being monic) vanishes at every `π_n`.
But the `π_n` (`n ≥ 1`) are infinitely many distinct points (`pi_norm_injective`),
so the polynomial has infinitely many roots, hence is zero — contradiction.

Proof for Proposition 9.4.4

Proof uses 2

Proof dependency previews

Preview

Lemma 9.4.1

Loading preview

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

If \cN(f) = f, then Lemma 9.4.3 gives N_{n+1,n}(f(\pi_{n+1})) = (\cN f)(\pi_n) = f(\pi_n), so the sequence (f(\pi_n))_n is norm-compatible and lies in \sU_\infty; thus R is well defined. Injectivity is Lemma 9.4.1: two \cN-invariant series with the same image agree at every \pi_n, hence are equal.

Surjectivity of R is the crux. It rests on how \cN behaves modulo powers of p.

Lemma9.4.5

uses 0used by 1✓L∃∀N

Let f \in \Zp[[T]]. Then:

(i) if \varphi(f) \equiv 1 \pmod{p^k} then f \equiv 1 \pmod{p^k};

(ii) \cN(f) \equiv f \pmod{p}.

If moreover f \in \Zp[[T]]^{\times}, then:

(iii) if f \equiv 1 \pmod{p^k} with k \ge 1 then \cN(f) \equiv 1 \pmod{p^{k+1}};

(iv) if k_2 \ge k_1 \ge 0 then \cN^{k_2}(f) \equiv \cN^{k_1}(f) \pmod{p^{k_1+1}}.

Lean code for Lemma9.4.5●4 theorems

theoremdefined in PadicLFunctions/Coleman/NormOperator.lean

complete

theorem PadicLFunctions.Coleman.phi_injective_mod {p : ℕ}
  [hp : Fact (Nat.Prime p)] {k : ℕ} {f : PowerSeries ℤ_[p]}
  (h :
    PadicLFunctions.Coleman.ModEqPow p k (PadicLFunctions.phiSeries p f)
      1) :
  PadicLFunctions.Coleman.ModEqPow p k f 1

theorem PadicLFunctions.Coleman.phi_injective_mod
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  {k : ℕ} {f : PowerSeries ℤ_[p]}
  (h :
    PadicLFunctions.Coleman.ModEqPow p k
      (PadicLFunctions.phiSeries p f) 1) :
  PadicLFunctions.Coleman.ModEqPow p k f 1

T908 (i), RJW TeX 2729: if `φ(f) ≡ 1 mod p^k` then `f ≡ 1 mod p^k`. The
Frobenius `φ` is coefficientwise-injective mod `p^k`. Route: the retraction
`ψ ∘ φ = id` is `ℤ_[p]`-linear, so it cancels the `C(p^k)` factor
(`psiSeries_phi_padicInt` + `psiSeries_C_mul_padicInt`; CS06 Lem 2.3.1).

theoremdefined in PadicLFunctions/Coleman/NormOperator.lean

complete

theorem PadicLFunctions.Coleman.normOp_modEq_self {p : ℕ}
  [hp : Fact (Nat.Prime p)] (f : PowerSeries ℤ_[p]) :
  PadicLFunctions.Coleman.ModEqPow p 1
    (PadicLFunctions.Coleman.normOp f) f

theorem PadicLFunctions.Coleman.normOp_modEq_self
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  (f : PowerSeries ℤ_[p]) :
  PadicLFunctions.Coleman.ModEqPow p 1
    (PadicLFunctions.Coleman.normOp f) f

T908 (ii), RJW TeX 2731: `𝒩 f ≡ f mod p`. Determinant route over `𝔽_p`: reducing
`𝒩 f = det (digitMatrix f)` mod `p`, the matrix `M̄` squares to the scalar
`(p-th power) M̄^p = digitMatrix(f^p) ≡ diagonal f̄ mod p`
(`digitMatrix_pow_p_modEq_diagonal`), so `(det M̄)^p = det (diagonal f̄) = f̄^p`; the
Frobenius `x ↦ x^p` is injective on the domain `𝔽_p⟦T⟧`, giving `det M̄ = f̄`, i.e.
`𝒩 f ≡ f mod p`. (This avoids the `μ_p`-product/twisted-circulant computation: a
replan note for R10.5 — the abstract `Algebra.norm` over `𝔽_p` is the `p`-th power for
the purely inseparable degree-`p` step `B̄/φ(B̄)`.)

theoremdefined in PadicLFunctions/Coleman/NormOperator.lean

complete

theorem PadicLFunctions.Coleman.normOp_modEq_one {p : ℕ}
  [hp : Fact (Nat.Prime p)] {k : ℕ} (hk : 1 ≤ k) {f : PowerSeries ℤ_[p]}
  (_hf : IsUnit f) (h : PadicLFunctions.Coleman.ModEqPow p k f 1) :
  PadicLFunctions.Coleman.ModEqPow p (k + 1)
    (PadicLFunctions.Coleman.normOp f) 1

theorem PadicLFunctions.Coleman.normOp_modEq_one
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  {k : ℕ} (hk : 1 ≤ k)
  {f : PowerSeries ℤ_[p]} (_hf : IsUnit f)
  (h :
    PadicLFunctions.Coleman.ModEqPow p k f
      1) :
  PadicLFunctions.Coleman.ModEqPow p
    (k + 1)
    (PadicLFunctions.Coleman.normOp f) 1

T908 (iii), RJW TeX 2735: for a unit `f ≡ 1 mod p^k` (`k ≥ 1`),
`𝒩 f ≡ 1 mod p^{k+1}`. Determinant route: write `f = 1 + C(p^k)·h`, so
`digitMatrix f = 1 + C(p^k) • digitMatrix h` and (Taylor expansion,
`Matrix.det_one_add_smul`)
`𝒩 f = det = 1 + (trace (digitMatrix h))·C(p^k) + R·C(p^k)²`. The linear term is
`p·ψ(h)·C(p^k) = C(p^{k+1})·ψ(h)` (`trace_digitMatrix`), the quadratic term carries
`C(p^{2k})` with `2k ≥ k+1`; both are `≡ 0 mod p^{k+1}`. (The unit hypothesis is not
needed for this part — it is recorded to match the source's statement grouping.)

theoremdefined in PadicLFunctions/Coleman/NormOperator.lean

complete

theorem PadicLFunctions.Coleman.normOp_iterate_modEq {p : ℕ}
  [hp : Fact (Nat.Prime p)] {k₁ k₂ : ℕ} (h : k₁ ≤ k₂)
  {f : PowerSeries ℤ_[p]} (hf : IsUnit f) :
  PadicLFunctions.Coleman.ModEqPow p (k₁ + 1)
    (PadicLFunctions.Coleman.normOp^[k₂] f)
    (PadicLFunctions.Coleman.normOp^[k₁] f)

theorem PadicLFunctions.Coleman.normOp_iterate_modEq
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  {k₁ k₂ : ℕ} (h : k₁ ≤ k₂)
  {f : PowerSeries ℤ_[p]}
  (hf : IsUnit f) :
  PadicLFunctions.Coleman.ModEqPow p
    (k₁ + 1)
    (PadicLFunctions.Coleman.normOp^[k₂]
      f)
    (PadicLFunctions.Coleman.normOp^[k₁]
      f)

T908 (iv), RJW TeX 2737: for a unit `f` and `k₁ ≤ k₂`,
`𝒩^{[k₂]} f ≡ 𝒩^{[k₁]} f mod p^{k₁+1}`. From part (ii), the unit
`g := 𝒩^{[k₂−k₁]} f · f⁻¹ ≡ 1 mod p`; iterating part (iii) `k₁` times gives
`𝒩^{[k₁]} g ≡ 1 mod p^{k₁+1}`; unfolding `𝒩^{[k₁]} g = 𝒩^{[k₂]} f · (𝒩^{[k₁]} f)⁻¹`
(`𝒩` multiplicative) and multiplying by `𝒩^{[k₁]} f` finishes.

Proof for Lemma 9.4.5

uses 0

For (i), reduce mod p: since (1+T)^p - 1 \equiv T^p \pmod p, the reduction of \varphi is the Frobenius substitution \bar f(T) \mapsto \bar f(T^p) on \Fp[[T]], which is injective; a dévissage up the filtration p^k\Zp[[T]] \supset p^{k+1}\Zp[[T]] promotes this to: \varphi(f) \equiv 1 forces f \equiv 1 \pmod{p^k}. For (ii), every \eta \in \mu_p satisfies \eta \equiv 1 modulo the maximal ideal \mathfrak p_1 of \cO_{K_1}, so (\varphi\circ\cN)(f) = \prod_{\eta}f(\eta(1+T)-1) \equiv f(T)^p \pmod{\mathfrak p_1}; as the two sides lie in \Zp[[T]] this is a congruence mod p, and combined with the Frobenius relation f^p \equiv \varphi(f) \pmod p it gives \varphi(\cN f) \equiv \varphi(f) \pmod p, whence \cN f \equiv f \pmod p by (i). For (iii), let \mathfrak p_1 be the maximal ideal of \cO_{K_1}. Since (\eta-1)(1+T) \in \mathfrak p_1\Zp[[T]], we have \eta(1+T) - 1 \equiv T \pmod{\mathfrak p_1\Zp[[T]]}, so term-by-term f(\eta(1+T)-1) \equiv f(T) \pmod{\mathfrak p_1 p^k\Zp[[T]]} when f \equiv 1 \pmod{p^k}. Multiplying over \eta \in \mu_p gives (\varphi\circ\cN)(f) \equiv f^p \pmod{\mathfrak p_1 p^k}; as both sides lie in \Zp[[T]], this holds modulo \mathfrak p_1 p^k \cap \Zp = p^{k+1}. But f \equiv 1 \pmod{p^k} gives f^p \equiv 1 \pmod{p^{k+1}}, so \varphi(\cN f) \equiv 1 \pmod{p^{k+1}} and (i) yields \cN(f) \equiv 1 \pmod{p^{k+1}}. Part (iv) follows: by (ii), \cN^{k_2 - k_1}f/f \equiv 1 \pmod p, and applying (iii) while iterating \cN a further k_1 times upgrades the congruence to modulus p^{k_1+1}.

Proposition9.4.6

uses 0used by 1✓L∃∀N

The map R : (\Zp[[T]]^{\times})^{\cN = \mathrm{id}} \to \sU_\infty is surjective.

Lean code for Proposition9.4.6●2 theorems

theoremdefined in PadicLFunctions/Coleman/Theorem.lean

complete

theorem PadicLFunctions.Coleman.coleman_existsUnique (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (u : PadicLFunctions.Coleman.NormCompatUnits p) :
  ∃! f,
    IsUnit f ∧
      PadicLFunctions.Coleman.normOp f = f ∧
        ∀ (n : ℕ),
          1 ≤ n → PadicLFunctions.Coleman.evalPi p f n = ↑(u.elems n)

theorem PadicLFunctions.Coleman.coleman_existsUnique
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (u :
    PadicLFunctions.Coleman.NormCompatUnits
      p) :
  ∃! f,
    IsUnit f ∧
      PadicLFunctions.Coleman.normOp f =
          f ∧
        ∀ (n : ℕ),
          1 ≤ n →
            PadicLFunctions.Coleman.evalPi
                p f n =
              ↑(u.elems n)

**Coleman's theorem** (RJW `thm:coleman power series`, TeX 2553–2560; `thm:coleman map 2`,
TeX 2796–2807): for every norm-compatible system of units `u = (u_n)_n ∈ 𝒰_∞`, there is a
*unique* unit power series `f ∈ ℤ_p⟦T⟧^×` that is `𝒩`-invariant (`𝒩 f = f`) and interpolates
`u` (`f(π_n) = u_n` for all `n ≥ 1`).

**Uniqueness** is the Weierstrass `evalPi_injective` (T905, RJW lem:unique-coleman): two such
`f, g` agree at every `π_n`, `n ≥ 1`, hence are equal (the `IsUnit`/`𝒩`-invariance clauses are
not needed for uniqueness).

**Existence** is the diagonal/compactness argument (TeX 2763–2791):
* (a) per-level interpolants `F_m` (`exists_evalPi_eq`, `‖u_m‖ = 1` from `norm_elems_eq_one`);
* (b) the norm-iterate evaluation `𝒩^{[k]} F_{n+k}(π_n) = u_n` (induction on `k`, via
  `evalPi_normOp` (T907) and `u.compat`);
* (c) the diagonal `g_m := 𝒩^{[m]} F_{2m}` and a coefficientwise-convergent subsequence
  `g_{φ j} → f_u` (`exists_subseq_tendsto`, T909/compactness);
* (d) `f_u(π_n) = u_n`: the value `g_{φ j}(π_n)` tends to `f_u(π_n)`
  (`tendsto_evalPi_of_tendsto`) *and* to `u_n` (the congruence `u_n ≡ g_m(π_n) mod p^{m+1}`
  from `normOp_iterate_modEq` (T908 iv) + `norm_evalPi_sub_le_of_modEqPow`, squeezed as
  `φ j → ∞`), so the two limits agree;
* (e) `IsUnit f_u`: each `g_m` is a unit (`normOp_iterate_isUnit`) and the units are closed
  (`isClosed_isUnit`, `IsClosed.mem_of_tendsto`);
* (f) `𝒩 f_u = f_u`: `𝒩 f_u` also interpolates `u` (`evalPi_normOp` + `u.compat`), so
  `evalPi_injective` forces `𝒩 f_u = f_u`.

theoremdefined in PadicLFunctions/Coleman/NormOperator.lean

complete

theorem PadicLFunctions.Coleman.exists_subseq_tendsto {p : ℕ}
  [hp : Fact (Nat.Prime p)] (g : ℕ → PowerSeries ℤ_[p]) :
  ∃ f φ, StrictMono φ ∧ Filter.Tendsto (g ∘ φ) Filter.atTop (nhds f)

theorem PadicLFunctions.Coleman.exists_subseq_tendsto
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  (g : ℕ → PowerSeries ℤ_[p]) :
  ∃ f φ,
    StrictMono φ ∧
      Filter.Tendsto (g ∘ φ) Filter.atTop
        (nhds f)

T909: every sequence in `ℤ_p⟦T⟧` has a coefficientwise-convergent
subsequence (the extraction feeding T910's diagonal argument).

Proof for Proposition 9.4.6

Proof uses 4

Proof dependency previews

Preview

Lemma 9.2.1

Loading preview

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

Let u = (u_n) \in \sU_\infty. For each n pick f_n \in \Zp[[T]]^{\times} with f_n(\pi_n) = u_n (possible by Lemma 9.2.1). Using Lemma 9.4.3 and norm-compatibility of u, one checks (\cN^k f_{n+k})(\pi_n) = u_n for all k \ge 0. Set g_n := \cN^{n} f_{2n}. For m \ge n, combining this identity (with k = 2m-n) and Lemma 9.4.5(iv) (with k_2 = 2m-n, k_1 = m) gives u_n = (\cN^{2m-n}f_{2m})(\pi_n) \equiv (\cN^m f_{2m})(\pi_n) = g_m(\pi_n) \pmod{p^{m+1}}, so g_m(\pi_n) \to u_n as m \to \infty, for every n. Since \Zp[[T]]^{\times} is compact, (g_m) has a convergent subsequence; let f_u be its limit. Then f_u(\pi_n) = u_n for all n. Finally, Lemma 9.4.3 and norm-compatibility give (\cN f_u)(\pi_n) = N_{n+1,n}f_u(\pi_{n+1}) = N_{n+1,n}(u_{n+1}) = u_n = f_u(\pi_n), so \cN f_u and f_u are both Coleman series for u; by Lemma 9.4.1 they coincide, i.e. \cN(f_u) = f_u.

Theorem9.4.7

uses 0used by 1✓L∃∀N

The map R of Proposition 9.4.4 is an isomorphism of groups R : (\Zp[[T]]^{\times})^{\cN = \mathrm{id}} \xrightarrow{\ \sim\ } \sU_\infty, and its inverse u \mapsto f_u is the unique map with f_u(\pi_n) = u_n for all u \in \sU_\infty, n \ge 1. In particular Coleman's power series f_u is always \cN-invariant.

Lean code for Theorem9.4.7●3 theorems

theoremdefined in PadicLFunctions/Coleman/Theorem.lean

complete

theorem PadicLFunctions.Coleman.coleman_existsUnique (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (u : PadicLFunctions.Coleman.NormCompatUnits p) :
  ∃! f,
    IsUnit f ∧
      PadicLFunctions.Coleman.normOp f = f ∧
        ∀ (n : ℕ),
          1 ≤ n → PadicLFunctions.Coleman.evalPi p f n = ↑(u.elems n)

theorem PadicLFunctions.Coleman.coleman_existsUnique
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (u :
    PadicLFunctions.Coleman.NormCompatUnits
      p) :
  ∃! f,
    IsUnit f ∧
      PadicLFunctions.Coleman.normOp f =
          f ∧
        ∀ (n : ℕ),
          1 ≤ n →
            PadicLFunctions.Coleman.evalPi
                p f n =
              ↑(u.elems n)

**Coleman's theorem** (RJW `thm:coleman power series`, TeX 2553–2560; `thm:coleman map 2`,
TeX 2796–2807): for every norm-compatible system of units `u = (u_n)_n ∈ 𝒰_∞`, there is a
*unique* unit power series `f ∈ ℤ_p⟦T⟧^×` that is `𝒩`-invariant (`𝒩 f = f`) and interpolates
`u` (`f(π_n) = u_n` for all `n ≥ 1`).

**Uniqueness** is the Weierstrass `evalPi_injective` (T905, RJW lem:unique-coleman): two such
`f, g` agree at every `π_n`, `n ≥ 1`, hence are equal (the `IsUnit`/`𝒩`-invariance clauses are
not needed for uniqueness).

**Existence** is the diagonal/compactness argument (TeX 2763–2791):
* (a) per-level interpolants `F_m` (`exists_evalPi_eq`, `‖u_m‖ = 1` from `norm_elems_eq_one`);
* (b) the norm-iterate evaluation `𝒩^{[k]} F_{n+k}(π_n) = u_n` (induction on `k`, via
  `evalPi_normOp` (T907) and `u.compat`);
* (c) the diagonal `g_m := 𝒩^{[m]} F_{2m}` and a coefficientwise-convergent subsequence
  `g_{φ j} → f_u` (`exists_subseq_tendsto`, T909/compactness);
* (d) `f_u(π_n) = u_n`: the value `g_{φ j}(π_n)` tends to `f_u(π_n)`
  (`tendsto_evalPi_of_tendsto`) *and* to `u_n` (the congruence `u_n ≡ g_m(π_n) mod p^{m+1}`
  from `normOp_iterate_modEq` (T908 iv) + `norm_evalPi_sub_le_of_modEqPow`, squeezed as
  `φ j → ∞`), so the two limits agree;
* (e) `IsUnit f_u`: each `g_m` is a unit (`normOp_iterate_isUnit`) and the units are closed
  (`isClosed_isUnit`, `IsClosed.mem_of_tendsto`);
* (f) `𝒩 f_u = f_u`: `𝒩 f_u` also interpolates `u` (`evalPi_normOp` + `u.compat`), so
  `evalPi_injective` forces `𝒩 f_u = f_u`.

theoremdefined in PadicLFunctions/Coleman/Theorem.lean

complete

theorem PadicLFunctions.Coleman.normOp_colemanSeries (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (u : PadicLFunctions.Coleman.NormCompatUnits p) :
  PadicLFunctions.Coleman.normOp
      (PadicLFunctions.Coleman.colemanSeries p u) =
    PadicLFunctions.Coleman.colemanSeries p u

theorem PadicLFunctions.Coleman.normOp_colemanSeries
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (u :
    PadicLFunctions.Coleman.NormCompatUnits
      p) :
  PadicLFunctions.Coleman.normOp
      (PadicLFunctions.Coleman.colemanSeries
        p u) =
    PadicLFunctions.Coleman.colemanSeries
      p u

`colemanSeries u` is `𝒩`-invariant (the second clause of `coleman_existsUnique`).

theoremdefined in PadicLFunctions/Coleman/Theorem.lean

complete

theorem PadicLFunctions.Coleman.evalPi_colemanSeries (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (u : PadicLFunctions.Coleman.NormCompatUnits p) {n : ℕ} (hn : 1 ≤ n) :
  PadicLFunctions.Coleman.evalPi p
      (PadicLFunctions.Coleman.colemanSeries p u) n =
    ↑(u.elems n)

theorem PadicLFunctions.Coleman.evalPi_colemanSeries
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (u :
    PadicLFunctions.Coleman.NormCompatUnits
      p)
  {n : ℕ} (hn : 1 ≤ n) :
  PadicLFunctions.Coleman.evalPi p
      (PadicLFunctions.Coleman.colemanSeries
        p u)
      n =
    ↑(u.elems n)

`colemanSeries u` interpolates `u`: `colemanSeries u (π_n) = u_n` for `n ≥ 1` (the third
clause of `coleman_existsUnique`).

Proof for Theorem 9.4.7

Proof uses 4

Proof dependency previews

Preview

Theorem 9.2.2

Loading preview

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

By Proposition 9.4.4 the map R is an injective homomorphism, and by Proposition 9.4.6 it is surjective; hence it is a group isomorphism. Its inverse sends u to the series f_u = R^{-1}(u), which satisfies f_u(\pi_n) = u_n by construction of R; uniqueness is Lemma 9.4.1. This is precisely the refined form of Theorem 9.2.2.