Amice's theorem on the analytic stages

For a complete ultrametric normed ℤ_p-module E with contractive action, Amice's map

TauCeti.AnalyticStage.amiceMap p h S : C₀(ℕ, E) → LA_h(E), (cₙ) ↦ ∑ₙ e_{h,n} • cₙ,

built from the polynomials e_{h,n}(x) = ⌊n / pʰ⌋! (x choose n), is an isometric isomorphism (TauCeti.AnalyticStage.amiceEquiv). Every coefficient vector in the analytic stage LA_h(E) = C₀(ZMod (pʰ) × ℕ, E) is therefore the expansion of a unique series ∑ₙ e_{h,n} • cₙ with cₙ → 0, and its norm is supₙ ‖cₙ‖. No torsion-freeness of E is needed.

The proof writes Amice's map as a matrix over ℤ_p and applies the criterion Matrix.toZeroAtInftySMulLinearIsometryEquiv for triangular perturbations of the identity. Write n = pʰ q + r with r < pʰ. Modulo p, the expansion of e_{h,n} on the disc of a natural centre a < pʰ vanishes in degrees above q (TauCeti.norm_coeff_amicePolynomial_lt_one_of_div_lt), vanishes entirely when a < r (TauCeti.norm_coeff_amicePolynomial_lt_one_of_mod_lt), and has a unit coefficient in degree q when a = r (TauCeti.norm_coeff_amicePolynomial_mod_div). Order the coordinates (a, j) of LA_h(E) by the degree j first and then by decreasing centre a, so that (a, j) comes at position pʰ j + (pʰ - 1 - a); this reversal of the centres is the passage from Colmez's centres -a, 1 ≤ a ≤ pʰ, to the natural residue representatives used by LA_h. Reindex Amice's index n in the same way. In these coordinates the coefficient of e_{h,n} at its own position (r, q) is a unit, and every coefficient below the diagonal is divisible by p.

Main definitions

• TauCeti.AnalyticStage.amiceEquiv p h S: Amice's map as an S-linear isometric equivalence C₀(ℕ, E) ≃ₗᵢ[S] LA_h(E).

Main results

• TauCeti.AnalyticStage.amiceEquiv_apply: amiceEquiv is amiceMap.
• TauCeti.AnalyticStage.norm_amiceMap: Amice's map preserves norms.

References

• Y. Amice, Interpolation p-adique, Bull. Soc. Math. France 92 (1964), 117–180.
• P. Colmez, Fonctions d'une variable p-adique, Astérisque 330 (2010), §I.4.

Reordering the coordinates

The matrix of Amice's map

Amice's isometry

noncomputable def TauCeti.AnalyticStage.amiceEquiv (p : ℕ) [hp : Fact (Nat.Prime p)] (h : ℕ) {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] (S : Type u_2) [Semiring S] [Module S E] [ContinuousConstSMul S E] [SMulCommClass ℤ_[p] S E] : ZeroAtInftyContinuousMap ℕ E ≃ₗᵢ[S] AnalyticStage p h E

Amice's theorem. Amice's map (cₙ) ↦ ∑ₙ e_{h,n} • cₙ, where e_{h,n}(x) = ⌊n / pʰ⌋! (x choose n), is an isometric isomorphism from the null sequences in E onto the analytic stage LA_h(E).

@[simp]

theorem TauCeti.AnalyticStage.amiceEquiv_apply {p : ℕ} [hp : Fact (Nat.Prime p)] {h : ℕ} {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] (S : Type u_2) [Semiring S] [Module S E] [ContinuousConstSMul S E] [SMulCommClass ℤ_[p] S E] (c : ZeroAtInftyContinuousMap ℕ E) : (amiceEquiv p h S) c = (amiceMap p h S) c

The isometric equivalence amiceEquiv is Amice's map.

@[simp]

theorem TauCeti.AnalyticStage.norm_amiceMap {p : ℕ} [hp : Fact (Nat.Prime p)] {h : ℕ} {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] (S : Type u_2) [Semiring S] [Module S E] [ContinuousConstSMul S E] [SMulCommClass ℤ_[p] S E] (c : ZeroAtInftyContinuousMap ℕ E) : ‖(amiceMap p h S) c‖ = ‖c‖

Amice's theorem. Amice's map preserves norms: ‖∑ₙ e_{h,n} • cₙ‖ = supₙ ‖cₙ‖.

theorem TauCeti.AnalyticStage.amiceMap_surjective (p : ℕ) [hp : Fact (Nat.Prime p)] (h : ℕ) {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] (S : Type u_2) [Semiring S] [Module S E] [ContinuousConstSMul S E] [SMulCommClass ℤ_[p] S E] : Function.Surjective ⇑(amiceMap p h S)

Amice's theorem: surjectivity. Every coefficient vector of LA_h(E) is the expansion of a series ∑ₙ e_{h,n} • cₙ with cₙ → 0.

@[simp]

theorem TauCeti.AnalyticStage.amiceEquiv_symm_amiceTerm {p : ℕ} [hp : Fact (Nat.Prime p)] {h : ℕ} {E : Type u_1} [NormedAddCommGroup E] [Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] (S : Type u_2) [Semiring S] [Module S E] [ContinuousConstSMul S E] [SMulCommClass ℤ_[p] S E] (n : ℕ) (e : E) : (amiceEquiv p h S).symm (amiceTerm p h n e) = ZeroAtInftyContinuousMap.single n e

The inverse of Amice's isomorphism sends Amice's vector e_{h,n} • e to the coordinate vector single n e.

theorem TauCeti.AnalyticStage.isOrthonormalBasis_amiceTerm (p : ℕ) [hp : Fact (Nat.Prime p)] (h : ℕ) : IsOrthonormalBasis ℤ_[p] fun (n : ℕ) => amiceTerm p h n 1

Amice's basis theorem. The disc expansions amiceTerm p h n 1 of Amice's polynomials e_{h,n}(x) = ⌊n / pʰ⌋! (x choose n) form an orthonormal basis of LA_h(ℤ_p).

theorem TauCeti.AnalyticStage.continuousLinearMap_ext_amiceTerm {p : ℕ} [hp : Fact (Nat.Prime p)] {h : ℕ} {R : Type u_3} {M : Type u_4} [NormedCommRing R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R] [IsUltrametricDist R] [CompleteSpace R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [T2Space M] {φ ψ : AnalyticStage p h R →L[R] M} (H : ∀ (n : ℕ), φ (amiceTerm p h n 1) = ψ (amiceTerm p h n 1)) : φ = ψ

Continuous linear maps out of an analytic stage agreeing on Amice's polynomials are equal.