Operators with compactoid image are completely continuous

Let K be a complete nontrivially normed field and F an ultrametric Banach space over K. A continuous linear map u : E →L[K] F maps the closed unit ball to a compactoid set exactly when it is a limit in operator norm of continuous linear maps of finite rank (ContinuousLinearMap.hasCompactoidImage_iff_isCompletelyContinuous). This is the comparison of Schikhof's compact operators with Serre's completely continuous operators on arbitrary Banach spaces; neither a discrete valuation nor spherical completeness of K is assumed.

The direction from complete continuity to compactoid image is ContinuousLinearMap.IsCompletelyContinuous.hasCompactoidImage. For the converse, a compactoid set is approximated by the initial pieces of a single sequence (TauCeti.IsCompactoidSet.exists_seq_forall_exists_finset), so the image of u lies in the closed subspace D spanned by a sequence. This subspace is of countable type, hence continuously linearly equivalent to a model space C₀(I, K) (TauCeti.isPotentiallyONable_of_dense_span). In such coordinates a compactoid set has uniformly decaying coordinates, so the coordinate projections onto finite sets of indices approximate u in operator norm (ContinuousLinearMap.HasCompactoidImage.isCompletelyContinuous_of_zeroAtInfty). The argument never projects onto a finite-dimensional subspace of the ambient space F, which over a field that is not spherically complete need not be complemented.

Consequently every topologically compact operator is completely continuous (IsCompactOperator.isCompletelyContinuous), and over a locally compact field the two notions agree (ContinuousLinearMap.isCompactOperator_iff_isCompletelyContinuous). Over ℂ_p they differ: the identity of a line has finite rank but is not a compact operator (isCompactOperator_id_iff_locallyCompactSpace).

Main results

• ContinuousLinearMap.HasCompactoidImage.isCompletelyContinuous_of_zeroAtInfty: a map into a model space with compactoid image is completely continuous.
• ContinuousLinearMap.HasCompactoidImage.isCompletelyContinuous, ContinuousLinearMap.hasCompactoidImage_iff_isCompletelyContinuous: the comparison on ultrametric Banach spaces.
• IsCompactOperator.isCompletelyContinuous, ContinuousLinearMap.isCompactOperator_iff_isCompletelyContinuous: the comparison with topologically compact operators.

References

• W. H. Schikhof, Banach spaces over nonarchimedean valued fields, Topology Proceedings 24 (1999), 547–581, §§2.7, 2.15.
• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §§1–3.
• C. Perez-Garcia and W. H. Schikhof, Locally Convex Spaces over Non-Archimedean Valued Fields, Cambridge Studies in Advanced Mathematics 119, Cambridge University Press, 2010, Chapter 2.

theorem ContinuousLinearMap.HasCompactoidImage.isCompletelyContinuous_of_zeroAtInfty {K : Type u_1} {E : Type u_2} [NontriviallyNormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] {I : Type u_4} [TopologicalSpace I] [DiscreteTopology I] {u : E →L[K] ZeroAtInftyContinuousMap I K} (hu : u.HasCompactoidImage) : u.IsCompletelyContinuous

A map into a model space with compactoid image is completely continuous: since the coordinates of a compactoid subset of C₀(I, K) decay uniformly, the coordinate projections onto finite sets of indices approximate the map in operator norm. Neither completeness of K nor the ultrametric inequality is needed.

theorem ContinuousLinearMap.HasCompactoidImage.isCompletelyContinuous {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [CompleteSpace K] [SeminormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] [IsUltrametricDist F] [CompleteSpace F] {u : E →L[K] F} (hu : u.HasCompactoidImage) : u.IsCompletelyContinuous

Compactoid image implies complete continuity. Over a complete nontrivially normed field, a continuous linear map into an ultrametric Banach space that maps the closed unit ball to a compactoid set is a limit in operator norm of continuous linear maps of finite rank. The image lies in a closed subspace of countable type, which has a model space C₀(I, K) as coordinates.

theorem ContinuousLinearMap.hasCompactoidImage_iff_isCompletelyContinuous {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [CompleteSpace K] [SeminormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] [IsUltrametricDist F] [CompleteSpace F] {u : E →L[K] F} : u.HasCompactoidImage ↔ u.IsCompletelyContinuous

Compactoid image is complete continuity for maps into an ultrametric Banach space over a complete nontrivially normed field.

theorem ContinuousLinearMap.isCompactOperator_iff_isCompletelyContinuous {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [CompleteSpace K] [SeminormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] [IsUltrametricDist F] [CompleteSpace F] [ProperSpace K] {u : E →L[K] F} : IsCompactOperator ⇑u ↔ u.IsCompletelyContinuous

Over a locally compact nontrivially normed field, such as ℚ_p, a continuous linear map into an ultrametric Banach space is a compact operator exactly when it is completely continuous.

theorem IsCompactOperator.isCompletelyContinuous {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [CompleteSpace K] [SeminormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] [IsUltrametricDist F] [CompleteSpace F] {u : E →L[K] F} (hu : IsCompactOperator ⇑u) : u.IsCompletelyContinuous

Compact operators are completely continuous. Over a complete nontrivially normed field, every compact operator into an ultrametric Banach space is a limit in operator norm of continuous linear maps of finite rank.