Triangular perturbations of the identity of C₀(ℕ, E)

Let R be a seminormed ring and E a complete ultrametric normed R-module with contractive action. A matrix A over R with null columns and bounded entries defines a continuous linear map A.toZeroAtInftySMulCLM S on the model space C₀(ℕ, E), acting by (A x) i = ∑ j, A i j • x j (output index first). This file shows that A is an isometric automorphism as soon as

• every entry has norm at most one,
• every diagonal entry is a unit d of R acting isometrically, ‖d • e‖ = ‖e‖ for all e, and
• the entries strictly below the diagonal have norm at most a constant c < 1.

The isometry needs only that each entry below the diagonal has norm < 1, and holds for an arbitrary linearly ordered discrete index type: at the last coordinate where x attains its norm, the diagonal term of (A x) i strictly dominates all the others. For surjectivity, write A as its upper triangular part U plus a strictly lower triangular part of entries of norm at most c. The columns of U are finite, so back substitution solves U x = y for every finitely supported y; since U is an isometry its range is closed, hence U is onto. Then U⁻¹ A is within max c 0 < 1 of the identity, so it is onto by the contraction principle (TauCeti.surjective_of_norm_sub_apply_le).

No torsion-freeness of E is needed. Under a contractive action, a unit d with ‖d‖ ≤ 1 and ‖d⁻¹‖ ≤ 1, such as a unit of ℤ_p, acts isometrically on every such module. The map Matrix.toZeroAtInftyCLM on C₀(ℕ, R) itself, which multiplies by the entries on the right, is the action of the matrix over the opposite ring Rᵐᵒᵖ (Matrix.toZeroAtInftySMulCLM_map_op), so the same results hold for it, with the diagonal condition ‖r * d‖ = ‖r‖ for all r.

A matrix all of whose columns are finite satisfies the null-column hypothesis through tendsto_nhds_of_eventually_eq; the bidiagonal matrix 1 + ϖ S, with S the shift and ‖ϖ‖ < 1, is an example. The null-column hypothesis does not follow from the bounds on the entries: the matrix with constant entry ϖ ≠ 0 below the diagonal has no null column.

Main definitions

• Matrix.toZeroAtInftySMulLinearIsometryEquiv: the isometric automorphism of C₀(ℕ, E) defined by such a matrix.
• Matrix.toZeroAtInftyLinearIsometryEquiv: the isometric automorphism of C₀(ℕ, R) defined by such a matrix acting by right multiplication.

Main results

• Matrix.norm_toZeroAtInftySMulCLM_apply, Matrix.isometry_toZeroAtInftySMulCLM: the map defined by a matrix with entries of norm at most one, isometrically acting diagonal and entries of norm < 1 below the diagonal preserves norms.
• Matrix.surjective_toZeroAtInftySMulCLM: on C₀(ℕ, E) it is onto when moreover the diagonal entries are units and the entries below the diagonal are bounded by some c < 1.
• Matrix.norm_toZeroAtInftyCLM_apply, Matrix.isometry_toZeroAtInftyCLM, Matrix.surjective_toZeroAtInftyCLM: the same results for C₀(ℕ, R).

References

• P. Colmez, Fonctions d'une variable p-adique, Astérisque 330 (2010), §I.4 (Amice's theorem on the basis of locally analytic functions).
• P. Schneider, Nonarchimedean Functional Analysis, Springer, 2002, §10.

theorem Matrix.norm_toZeroAtInftySMulCLM_apply {I : Type u_1} {R : Type u_2} {E : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [LinearOrder I] [SeminormedRing R] [NormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [IsUltrametricDist E] [CompleteSpace E] (S : Type u_4) [Semiring S] [Module S E] [ContinuousConstSMul S E] [SMulCommClass R S E] (A : Matrix I I R) (hcol : ∀ (j : I), Filter.Tendsto (fun (i : I) => A i j) Filter.cofinite (nhds 0)) (hle : ∀ (i j : I), ‖A i j‖ ≤ 1) (hdiag : ∀ (i : I) (e : E), ‖A i i • e‖ = ‖e‖) (hlow : ∀ (i j : I), j < i → ‖A i j‖ < 1) (x : ZeroAtInftyContinuousMap I E) : ‖(toZeroAtInftySMulCLM S A hcol ⋯) x‖ = ‖x‖

Triangular isometries. Let A be a matrix with null columns over a seminormed ring R whose entries have norm at most one, whose diagonal entries d act isometrically on a complete ultrametric normed R-module E, and whose entries strictly below the diagonal have norm less than one. Then the map C₀(I, E) → C₀(I, E) defined by A preserves norms.

theorem Matrix.isometry_toZeroAtInftySMulCLM {I : Type u_1} {R : Type u_2} {E : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [LinearOrder I] [SeminormedRing R] [NormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [IsUltrametricDist E] [CompleteSpace E] (S : Type u_4) [Semiring S] [Module S E] [ContinuousConstSMul S E] [SMulCommClass R S E] (A : Matrix I I R) (hcol : ∀ (j : I), Filter.Tendsto (fun (i : I) => A i j) Filter.cofinite (nhds 0)) (hle : ∀ (i j : I), ‖A i j‖ ≤ 1) (hdiag : ∀ (i : I) (e : E), ‖A i i • e‖ = ‖e‖) (hlow : ∀ (i j : I), j < i → ‖A i j‖ < 1) : Isometry ⇑(toZeroAtInftySMulCLM S A hcol ⋯)

Triangular isometries. The map defined by a matrix as in norm_toZeroAtInftySMulCLM_apply is an isometry.

theorem Matrix.surjective_toZeroAtInftySMulCLM {R : Type u_1} {E : Type u_2} [SeminormedRing R] [NormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [IsUltrametricDist E] [CompleteSpace E] (S : Type u_3) [Semiring S] [Module S E] [ContinuousConstSMul S E] [SMulCommClass R S E] (A : Matrix ℕ ℕ R) (hcol : ∀ (j : ℕ), Filter.Tendsto (fun (i : ℕ) => A i j) Filter.cofinite (nhds 0)) (hle : ∀ (i j : ℕ), ‖A i j‖ ≤ 1) (hunit : ∀ (i : ℕ), IsUnit (A i i)) (hdiag : ∀ (i : ℕ) (e : E), ‖A i i • e‖ = ‖e‖) {c : ℝ} (hc : c < 1) (hlow : ∀ (i j : ℕ), j < i → ‖A i j‖ ≤ c) : Function.Surjective ⇑(toZeroAtInftySMulCLM S A hcol ⋯)

Triangular perturbations are onto. Let A be a matrix with null columns over a seminormed ring R, whose entries have norm at most one, whose diagonal entries are units acting isometrically on a complete ultrametric normed R-module E, and whose entries strictly below the diagonal have norm at most c < 1. Then the map C₀(ℕ, E) → C₀(ℕ, E) defined by A is surjective.

noncomputable def Matrix.toZeroAtInftySMulLinearIsometryEquiv {R : Type u_1} {E : Type u_2} [SeminormedRing R] [NormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [IsUltrametricDist E] [CompleteSpace E] (S : Type u_3) [Semiring S] [Module S E] [ContinuousConstSMul S E] [SMulCommClass R S E] (A : Matrix ℕ ℕ R) (hcol : ∀ (j : ℕ), Filter.Tendsto (fun (i : ℕ) => A i j) Filter.cofinite (nhds 0)) (hle : ∀ (i j : ℕ), ‖A i j‖ ≤ 1) (hunit : ∀ (i : ℕ), IsUnit (A i i)) (hdiag : ∀ (i : ℕ) (e : E), ‖A i i • e‖ = ‖e‖) {c : ℝ} (hc : c < 1) (hlow : ∀ (i j : ℕ), j < i → ‖A i j‖ ≤ c) : ZeroAtInftyContinuousMap ℕ E ≃ₗᵢ[S] ZeroAtInftyContinuousMap ℕ E

The isometric automorphism of C₀(ℕ, E) defined by a matrix with null columns, entries of norm at most one, isometrically acting units on the diagonal and entries of norm at most c < 1 below the diagonal.

@[simp]

theorem Matrix.toZeroAtInftySMulLinearIsometryEquiv_apply {R : Type u_1} {E : Type u_2} [SeminormedRing R] [NormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [IsUltrametricDist E] [CompleteSpace E] (S : Type u_3) [Semiring S] [Module S E] [ContinuousConstSMul S E] [SMulCommClass R S E] (A : Matrix ℕ ℕ R) (hcol : ∀ (j : ℕ), Filter.Tendsto (fun (i : ℕ) => A i j) Filter.cofinite (nhds 0)) (hle : ∀ (i j : ℕ), ‖A i j‖ ≤ 1) (hunit : ∀ (i : ℕ), IsUnit (A i i)) (hdiag : ∀ (i : ℕ) (e : E), ‖A i i • e‖ = ‖e‖) {c : ℝ} (hc : c < 1) (hlow : ∀ (i j : ℕ), j < i → ‖A i j‖ ≤ c) (x : ZeroAtInftyContinuousMap ℕ E) : (toZeroAtInftySMulLinearIsometryEquiv S A hcol hle hunit hdiag hc hlow) x = (toZeroAtInftySMulCLM S A hcol ⋯) x

The automorphism toZeroAtInftySMulLinearIsometryEquiv is the map defined by the matrix.

Right multiplication on C₀(ℕ, R)

theorem Matrix.norm_toZeroAtInftyCLM_apply {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [NormedRing R] [IsUltrametricDist R] [CompleteSpace R] [LinearOrder I] (A : Matrix I I R) (hcol : ∀ (j : I), Filter.Tendsto (fun (i : I) => A i j) Filter.cofinite (nhds 0)) (hle : ∀ (i j : I), ‖A i j‖ ≤ 1) (hdiag : ∀ (i : I) (r : R), ‖r * A i i‖ = ‖r‖) (hlow : ∀ (i j : I), j < i → ‖A i j‖ < 1) (x : ZeroAtInftyContinuousMap I R) : ‖(A.toZeroAtInftyCLM hcol ⋯) x‖ = ‖x‖

Triangular isometries. Let A be a matrix with null columns over a complete ultrametric normed ring whose entries have norm at most one, whose diagonal entries d satisfy ‖r * d‖ = ‖r‖, and whose entries strictly below the diagonal have norm less than one. Then the map C₀(I, R) → C₀(I, R) defined by A preserves norms.

theorem Matrix.isometry_toZeroAtInftyCLM {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [NormedRing R] [IsUltrametricDist R] [CompleteSpace R] [LinearOrder I] (A : Matrix I I R) (hcol : ∀ (j : I), Filter.Tendsto (fun (i : I) => A i j) Filter.cofinite (nhds 0)) (hle : ∀ (i j : I), ‖A i j‖ ≤ 1) (hdiag : ∀ (i : I) (r : R), ‖r * A i i‖ = ‖r‖) (hlow : ∀ (i j : I), j < i → ‖A i j‖ < 1) : Isometry ⇑(A.toZeroAtInftyCLM hcol ⋯)

Triangular isometries. The map defined by a matrix as in norm_toZeroAtInftyCLM_apply is an isometry.

theorem Matrix.surjective_toZeroAtInftyCLM {R : Type u_2} [NormedRing R] [IsUltrametricDist R] [CompleteSpace R] (A : Matrix ℕ ℕ R) (hcol : ∀ (j : ℕ), Filter.Tendsto (fun (i : ℕ) => A i j) Filter.cofinite (nhds 0)) (hle : ∀ (i j : ℕ), ‖A i j‖ ≤ 1) (hunit : ∀ (i : ℕ), IsUnit (A i i)) (hdiag : ∀ (i : ℕ) (r : R), ‖r * A i i‖ = ‖r‖) {c : ℝ} (hc : c < 1) (hlow : ∀ (i j : ℕ), j < i → ‖A i j‖ ≤ c) : Function.Surjective ⇑(A.toZeroAtInftyCLM hcol ⋯)

Triangular perturbations are onto. Let A be a matrix with null columns over a complete ultrametric normed ring, whose entries have norm at most one, whose diagonal entries are units d with ‖r * d‖ = ‖r‖, and whose entries strictly below the diagonal have norm at most c < 1. Then the map C₀(ℕ, R) → C₀(ℕ, R) defined by A is surjective.

noncomputable def Matrix.toZeroAtInftyLinearIsometryEquiv {R : Type u_2} [NormedRing R] [IsUltrametricDist R] [CompleteSpace R] (A : Matrix ℕ ℕ R) (hcol : ∀ (j : ℕ), Filter.Tendsto (fun (i : ℕ) => A i j) Filter.cofinite (nhds 0)) (hle : ∀ (i j : ℕ), ‖A i j‖ ≤ 1) (hunit : ∀ (i : ℕ), IsUnit (A i i)) (hdiag : ∀ (i : ℕ) (r : R), ‖r * A i i‖ = ‖r‖) {c : ℝ} (hc : c < 1) (hlow : ∀ (i j : ℕ), j < i → ‖A i j‖ ≤ c) : ZeroAtInftyContinuousMap ℕ R ≃ₗᵢ[R] ZeroAtInftyContinuousMap ℕ R

The isometric automorphism of C₀(ℕ, R) defined by a matrix with null columns, entries of norm at most one, units d with ‖r * d‖ = ‖r‖ on the diagonal and entries of norm at most c < 1 below the diagonal.

@[simp]

theorem Matrix.toZeroAtInftyLinearIsometryEquiv_apply {R : Type u_2} [NormedRing R] [IsUltrametricDist R] [CompleteSpace R] (A : Matrix ℕ ℕ R) (hcol : ∀ (j : ℕ), Filter.Tendsto (fun (i : ℕ) => A i j) Filter.cofinite (nhds 0)) (hle : ∀ (i j : ℕ), ‖A i j‖ ≤ 1) (hunit : ∀ (i : ℕ), IsUnit (A i i)) (hdiag : ∀ (i : ℕ) (r : R), ‖r * A i i‖ = ‖r‖) {c : ℝ} (hc : c < 1) (hlow : ∀ (i j : ℕ), j < i → ‖A i j‖ ≤ c) (x : ZeroAtInftyContinuousMap ℕ R) : (A.toZeroAtInftyLinearIsometryEquiv hcol hle hunit hdiag hc hlow) x = (A.toZeroAtInftyCLM hcol ⋯) x

The automorphism toZeroAtInftyLinearIsometryEquiv is the map defined by the matrix.