Row compactness is compactoid image

Let K be a nontrivially normed field and I, J discrete index types. For a continuous linear map u : C₀(J, K) →L[K] C₀(I, K) between model spaces, the i-th coordinates of the vectors u x with ‖x‖ ≤ 1 include the entries u.matrixCoeff i j = u (single j 1) i of the i-th row of its matrix, and over an ultrametric field they are bounded by the row norm rᵢ(u). A subset of C₀(I, K) is compactoid exactly when it is bounded and its coordinates decay uniformly (TauCeti.isCompactoidSet_iff_isBounded_and_exists_finset_forall_norm_lt), so over an ultrametric field u is row compact exactly when it maps the closed unit ball to a compactoid set (ContinuousLinearMap.isRowCompact_iff_hasCompactoidImage). Neither completeness, nor discreteness of the valuation, nor spherical completeness is used.

Together with Serre's criterion ContinuousLinearMap.isRowCompact_iff_isCompletelyContinuous this identifies, between model spaces over a complete ultrametric field, the three notions of compact operator: row compactness, compactoid image and complete continuity. Every topologically compact operator between model spaces is row compact (IsCompactOperator.isRowCompact), while over a field such as ℂ_p, which is not locally compact, the converse fails already for the identity of C₀(I, K) with I a singleton.

The ultrametric inequality is needed for the converse direction: over ℝ, the operator on C₀(ℕ, ℝ) with entries aᵢⱼ = 1 / (i + 1) for j ≤ i and 0 otherwise has row norms 1 / (i + 1), but maps the vectors that are 1 on {0, …, n} and 0 elsewhere to vectors whose first n + 1 coordinates are 1.

Main results

• ContinuousLinearMap.HasCompactoidImage.isRowCompact: a map between model spaces with compactoid image is row compact.
• ContinuousLinearMap.IsRowCompact.hasCompactoidImage: over an ultrametric field, a row-compact map has compactoid image.
• ContinuousLinearMap.isRowCompact_iff_hasCompactoidImage: the equivalence.
• IsCompactOperator.isRowCompact: compact operators between model spaces are row compact.

References

• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §3.
• W. H. Schikhof, Banach spaces over nonarchimedean valued fields, Topology Proceedings 24 (1999), 547–581, §2.15.

theorem ContinuousLinearMap.HasCompactoidImage.isRowCompact {I : Type u_1} {J : Type u_2} {K : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NontriviallyNormedField K] {u : ZeroAtInftyContinuousMap J K →L[K] ZeroAtInftyContinuousMap I K} (hu : u.HasCompactoidImage) : u.IsRowCompact

A map between model spaces with compactoid image is row compact: the entries of a row are coordinates of images of the unit vectors, which lie in the closed unit ball.

theorem ContinuousLinearMap.IsRowCompact.hasCompactoidImage {I : Type u_1} {J : Type u_2} {K : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NontriviallyNormedField K] [IsUltrametricDist K] {u : ZeroAtInftyContinuousMap J K →L[K] ZeroAtInftyContinuousMap I K} (hu : u.IsRowCompact) : u.HasCompactoidImage

A row-compact map between model spaces over an ultrametric field has compactoid image: the coordinates of the images of vectors of norm at most one are bounded by the row norms.

theorem ContinuousLinearMap.isRowCompact_iff_hasCompactoidImage {I : Type u_1} {J : Type u_2} {K : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NontriviallyNormedField K] [IsUltrametricDist K] {u : ZeroAtInftyContinuousMap J K →L[K] ZeroAtInftyContinuousMap I K} : u.IsRowCompact ↔ u.HasCompactoidImage

Row compactness is compactoid image: over an ultrametric nontrivially normed field, a map between model spaces is row compact exactly when it maps the closed unit ball to a compactoid set.

theorem IsCompactOperator.isRowCompact {I : Type u_1} {J : Type u_2} {K : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NontriviallyNormedField K] {u : ZeroAtInftyContinuousMap J K →L[K] ZeroAtInftyContinuousMap I K} (hu : IsCompactOperator ⇑u) : u.IsRowCompact

Compact operators between model spaces are row compact.