Continuous operators of finite rank are compact

A continuous linear map T : E →L[𝕜] F with finite-dimensional range is compact whenever F is a topological vector space over a locally compact nontrivially normed field. It factors through its range, which is locally compact. No norm or compatibility between the topology and module structure on E is needed.

In particular, operator-norm limits of finite-rank maps into a Banach space are compact, by isCompactOperator_of_tendsto.

Finiteness of the rank is spelled with Mathlib's LinearMap.HasFiniteRange.

Main declarations

• LinearMap.HasFiniteRange.isCompactOperator: over a locally compact nontrivially normed field, a continuous linear map of finite rank is a compact operator.

Mathlib sources

Scalar completeness and finite-dimensional local compactness come from IsLeftUniformAddGroup.completeSpace_of_weaklyLocallyCompactSpace and LocallyCompactSpace.of_finiteDimensional_of_complete, respectively. Compactness of maps into the range is provided by isCompactOperator_of_locallyCompactSpace_dom.

theorem LinearMap.HasFiniteRange.isCompactOperator {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [LocallyCompactSpace 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] {T : E →L[𝕜] F} (hT : (↑T).HasFiniteRange) : IsCompactOperator ⇑T

Over a locally compact nontrivially normed field, a continuous linear map into a topological vector space with finite-dimensional range is a compact operator.