Complete continuity implies row compactness

Every row-compact map u : C₀(J, R) →L[R] C₀(I, R) between model spaces is completely continuous (ContinuousLinearMap.IsRowCompact.isCompletelyContinuous). This file proves the converse, Serre's criterion, whenever the finitely generated submodules of the target C₀(I, R) are closed. In particular it holds over every complete ultrametric nontrivially normed field, with no discreteness or spherical completeness assumption: there the matrix of a continuous linear map between model spaces has row norms tending to zero exactly when the map is a limit of maps of finite rank in operator norm.

The key step is that a map whose columns u (single j 1) are combinations of finitely many fixed vectors w k, with uniformly bounded coefficients, has row decay: its i-th row is bounded by a multiple of ∑ k, ‖w k i‖, which tends to zero along the cofinite filter (ContinuousLinearMap.isRowCompact_of_apply_single_eq_sum). The coefficient bound is where the closedness hypothesis enters. A closed finitely generated submodule is a complete normed module, so the quantitative open mapping theorem over Tate rings (TauCeti.exists_linearCombination_eq_and_norm_le) writes each of its vectors in terms of a finite generating family with coefficients bounded linearly by the norm of the vector. Hence maps with range in a closed finitely generated submodule are row compact (ContinuousLinearMap.isRowCompact_of_fg_of_isClosed_of_range_le), and closedness of row compactness under operator-norm limits gives the criterion.

Over a general coefficient ring, closedness of finitely generated submodules is a genuine hypothesis rather than a formal consequence of completeness, so it is kept explicit. The row-decay theory itself, and the implication from row compactness to complete continuity, do not use it.

Main results

• ContinuousLinearMap.isRowCompact_of_fg_of_isClosed_of_range_le: a continuous map whose range lies in a closed finitely generated submodule of C₀(I, R) is row compact.
• ContinuousLinearMap.IsCompletelyContinuous.isRowCompact_of_forall_fg_isClosed, ContinuousLinearMap.isRowCompact_iff_isCompletelyContinuous_of_forall_fg_isClosed: if finitely generated submodules of C₀(I, R) are closed, complete continuity is equivalent to row compactness.
• ContinuousLinearMap.isRowCompact_iff_isCompletelyContinuous: Serre's criterion over a complete ultrametric nontrivially normed field.

References

• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §3, Proposition 4 and its corollary.
• C. Johansson and J. Newton, Extended eigenvarieties for overconvergent cohomology, arXiv:1604.07739, §2.1.

theorem ContinuousLinearMap.isRowCompact_of_fg_of_isClosed_of_range_le {I : Type u_1} {J : Type u_2} {R : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedRing R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] {L : Submodule R (ZeroAtInftyContinuousMap I R)} (hL : L.FG) (hLc : IsClosed ↑L) {u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R} (hu : (↑u).range ≤ L) : u.IsRowCompact

Maps with range in a closed finitely generated submodule are row compact over a complete ultrametric Tate ring. In particular, a map of finite rank is row compact as soon as some finitely generated submodule containing its range is closed.

theorem ContinuousLinearMap.IsCompletelyContinuous.isRowCompact_of_forall_fg_isClosed {I : Type u_1} {J : Type u_2} {R : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedRing R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] {u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R} (hu : u.IsCompletelyContinuous) (hclosed : ∀ (L : Submodule R (ZeroAtInftyContinuousMap I R)), L.FG → IsClosed ↑L) : u.IsRowCompact

Serre's criterion: if the finitely generated submodules of the target model space are closed, every completely continuous map between model spaces over a complete ultrametric Tate ring is row compact.

theorem ContinuousLinearMap.isRowCompact_iff_isCompletelyContinuous_of_forall_fg_isClosed {I : Type u_1} {J : Type u_2} {R : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedRing R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] (hclosed : ∀ (L : Submodule R (ZeroAtInftyContinuousMap I R)), L.FG → IsClosed ↑L) {u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R} : u.IsRowCompact ↔ u.IsCompletelyContinuous

If the finitely generated submodules of the target model space are closed, a map between model spaces over a complete ultrametric Tate ring is row compact exactly when it is completely continuous.

theorem ContinuousLinearMap.isRowCompact_iff_isCompletelyContinuous {I : Type u_1} {J : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] {K : Type u_4} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {u : ZeroAtInftyContinuousMap J K →L[K] ZeroAtInftyContinuousMap I K} : u.IsRowCompact ↔ u.IsCompletelyContinuous

Serre's criterion over a field: over a complete ultrametric nontrivially normed field K, a continuous linear map between model spaces is row compact exactly when it is completely continuous. Neither a discrete valuation nor spherical completeness is needed.