Operators with compactoid image

A continuous linear map u : E →L[K] F between normed spaces over a normed field K has compactoid image (ContinuousLinearMap.HasCompactoidImage) if it maps the closed unit ball of E to a compactoid subset of F. These are the compact operators of nonarchimedean Banach space theory in the sense of Schikhof: over a field such as ℂ_p, which is not locally compact, the topological notion IsCompactOperator is too restrictive (the identity of a line has finite rank but is not a compact operator), and compactoidness of the image of the unit ball replaces relative compactness.

Over a nontrivially normed field, an operator has compactoid image exactly when it maps every bounded set to a compactoid set (ContinuousLinearMap.hasCompactoidImage_iff_forall_isBounded). Operators with compactoid image form a closed two-sided operator ideal: they are stable under sums, scalar multiples and composition on either side with continuous linear maps, and under limits in operator norm (ContinuousLinearMap.isClosed_setOf_hasCompactoidImage). Topologically compact operators have compactoid image (IsCompactOperator.hasCompactoidImage). Over a complete nontrivially normed field, so do completely continuous operators, the operator-norm limits of maps of finite rank (ContinuousLinearMap.IsCompletelyContinuous.hasCompactoidImage); over a locally compact field these are moreover compact operators (ContinuousLinearMap.IsCompletelyContinuous.isCompactOperator). For maps into an ultrametric Banach space the converse holds too (ContinuousLinearMap.hasCompactoidImage_iff_isCompletelyContinuous, in TauCeti.Analysis.Normed.Operator.Compactoid.CompletelyContinuous).

Main definitions

• ContinuousLinearMap.HasCompactoidImage: the image of the closed unit ball is compactoid.

Main results

• ContinuousLinearMap.hasCompactoidImage_iff_forall_isBounded: compactoid image of every bounded set.
• ContinuousLinearMap.HasCompactoidImage.add, ContinuousLinearMap.HasCompactoidImage.smul, ContinuousLinearMap.HasCompactoidImage.clm_comp, ContinuousLinearMap.HasCompactoidImage.comp_clm, ContinuousLinearMap.isClosed_setOf_hasCompactoidImage: the closed operator ideal.
• IsCompactOperator.hasCompactoidImage: compact operators have compactoid image.
• LinearMap.IsFiniteRank.hasCompactoidImage, ContinuousLinearMap.IsCompletelyContinuous.hasCompactoidImage: over a complete field, maps of finite rank and completely continuous maps have compactoid image.
• ContinuousLinearMap.IsCompletelyContinuous.isCompactOperator: over a locally compact field, completely continuous maps into a Banach space are compact operators.

References

• W. H. Schikhof, Banach spaces over nonarchimedean valued fields, Topology Proceedings 24 (1999), 547–581, §2.15.
• N. De Grande-De Kimpe, Non-archimedean nuclearity, Groupe de travail d'analyse ultramétrique 9, no. 3 (1981–1982), exp. J4, §2.1.

def ContinuousLinearMap.HasCompactoidImage {K : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] [SeminormedAddCommGroup F] [NormedSpace K F] (u : E →L[K] F) : Prop

A continuous linear map has compactoid image if it maps the closed unit ball to a compactoid set.

theorem ContinuousLinearMap.hasCompactoidImage_iff {K : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] [SeminormedAddCommGroup F] [NormedSpace K F] {u : E →L[K] F} : u.HasCompactoidImage ↔ TauCeti.IsCompactoidSet K (⇑u '' Metric.closedBall 0 1)

@[simp]

theorem ContinuousLinearMap.hasCompactoidImage_zero {K : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] [SeminormedAddCommGroup F] [NormedSpace K F] : HasCompactoidImage 0

theorem ContinuousLinearMap.HasCompactoidImage.add {K : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] [SeminormedAddCommGroup F] [NormedSpace K F] {u v : E →L[K] F} (hu : u.HasCompactoidImage) (hv : v.HasCompactoidImage) : (u + v).HasCompactoidImage

The sum of two maps with compactoid image has compactoid image.

theorem ContinuousLinearMap.HasCompactoidImage.smul {K : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] [SeminormedAddCommGroup F] [NormedSpace K F] {u : E →L[K] F} (hu : u.HasCompactoidImage) (c : K) : (c • u).HasCompactoidImage

A scalar multiple of a map with compactoid image has compactoid image.

theorem ContinuousLinearMap.HasCompactoidImage.neg {K : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] [SeminormedAddCommGroup F] [NormedSpace K F] {u : E →L[K] F} (hu : u.HasCompactoidImage) : (-u).HasCompactoidImage

The negation of a map with compactoid image has compactoid image.

@[simp]

theorem ContinuousLinearMap.hasCompactoidImage_neg_iff {K : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] [SeminormedAddCommGroup F] [NormedSpace K F] {u : E →L[K] F} : (-u).HasCompactoidImage ↔ u.HasCompactoidImage

A map has compactoid image exactly when its negation does.

theorem ContinuousLinearMap.HasCompactoidImage.sub {K : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] [SeminormedAddCommGroup F] [NormedSpace K F] {u v : E →L[K] F} (hu : u.HasCompactoidImage) (hv : v.HasCompactoidImage) : (u - v).HasCompactoidImage

The difference of two maps with compactoid image has compactoid image.

theorem ContinuousLinearMap.HasCompactoidImage.clm_comp {K : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] [SeminormedAddCommGroup F] [NormedSpace K F] [SeminormedAddCommGroup G] [NormedSpace K G] {u : E →L[K] F} (hu : u.HasCompactoidImage) (v : F →L[K] G) : (v ∘SL u).HasCompactoidImage

Postcomposing a map with compactoid image with a continuous linear map gives a map with compactoid image.

theorem ContinuousLinearMap.hasCompactoidImage_of_forall_approx {K : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] [SeminormedAddCommGroup F] [NormedSpace K F] {u : E →L[K] F} (h : ∀ (ε : ℝ), 0 < ε → ∃ (v : E →L[K] F), v.HasCompactoidImage ∧ ∀ (x : E), ‖u x - v x‖ ≤ ε * ‖x‖) : u.HasCompactoidImage

Compactoid image is closed under uniform approximation. A continuous linear map that is, for every ε > 0, uniformly ε-close to a map with compactoid image has compactoid image.

theorem ContinuousLinearMap.hasCompactoidImage_iff_forall_isBounded {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] [SeminormedAddCommGroup F] [NormedSpace K F] {u : E →L[K] F} : u.HasCompactoidImage ↔ ∀ (S : Set E), Bornology.IsBounded S → TauCeti.IsCompactoidSet K (⇑u '' S)

Over a nontrivially normed field, a continuous linear map has compactoid image exactly when it maps every bounded set to a compactoid set.

theorem ContinuousLinearMap.HasCompactoidImage.comp_clm {K : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] [SeminormedAddCommGroup F] [NormedSpace K F] [SeminormedAddCommGroup G] [NormedSpace K G] {u : F →L[K] G} (hu : u.HasCompactoidImage) (v : E →L[K] F) : (u ∘SL v).HasCompactoidImage

Precomposing a map with compactoid image with a continuous linear map gives a map with compactoid image.

theorem ContinuousLinearMap.isClosed_setOf_hasCompactoidImage {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] [SeminormedAddCommGroup F] [NormedSpace K F] : IsClosed {u : E →L[K] F | u.HasCompactoidImage}

Compactoid image is closed in operator norm.

theorem IsCompactOperator.hasCompactoidImage {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] [SeminormedAddCommGroup F] [NormedSpace K F] {u : E →L[K] F} (hu : IsCompactOperator ⇑u) : u.HasCompactoidImage

Compact operators have compactoid image. A continuous linear map that is a compact operator in the topological sense maps the closed unit ball into a compact set, which is compactoid.

theorem LinearMap.IsFiniteRank.hasCompactoidImage {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] {u : E →L[K] F} (hu : (↑u).IsFiniteRank) : u.HasCompactoidImage

Over a complete nontrivially normed field, a map of finite rank has compactoid image: the image of the closed unit ball is a bounded subset of a finite-dimensional subspace.

theorem ContinuousLinearMap.IsCompletelyContinuous.hasCompactoidImage {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] {u : E →L[K] F} (hu : u.IsCompletelyContinuous) : u.HasCompactoidImage

Over a complete nontrivially normed field, completely continuous maps have compactoid image.

theorem ContinuousLinearMap.IsCompletelyContinuous.isCompactOperator {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] [ProperSpace K] [CompleteSpace F] {u : E →L[K] F} (hu : u.IsCompletelyContinuous) : IsCompactOperator ⇑u

Over a locally compact nontrivially normed field, such as ℚ_p, completely continuous maps into a Banach space are compact operators: the image of the closed unit ball is compactoid, hence totally bounded, so its closure is compact.