Completely continuous operators over a coefficient ring

A continuous linear map u : M →L[R] N between seminormed modules over a ring R is completely continuous (ContinuousLinearMap.IsCompletelyContinuous) if it can be approximated uniformly by continuous maps of finite rank: for every ε > 0 there is a continuous v whose range lies in a finitely generated submodule (LinearMap.IsFiniteRank) with ‖u x - v x‖ ≤ ε * ‖x‖ for all x. These are the operators of Serre's and Coleman's Fredholm theory over Banach algebras such as affinoid algebras, where the scalar ring is not a field and finite rank must be read relative to that ring.

The approximation is phrased through uniform bounds rather than through the operator norm, so that the definition carries no junk value over scalar rings where continuous maps need not be bounded. Over Tate scalars (TauCeti.NormedRing.IsTate), in particular over every nontrivially normed field, it is approximation in the operator norm ContinuousLinearMap.ringOpNorm (ContinuousLinearMap.isCompletelyContinuous_iff_ringOpNorm).

Over Tate scalars complete continuity is also a condition on lattices rather than norms: for a bounded neighbourhood M₀ of zero in the source, such as a bounded open lattice, u is completely continuous exactly when for every neighbourhood V of zero in the target some continuous map g of finite rank satisfies (u - g)(M₀) ⊆ V. This is the form in which complete continuity is stated for Banach modules given by lattices rather than by norms. The condition involves only the set M₀ and the neighbourhoods of zero in the target, so different bounded open lattices give the same notion, and so do equivalent norms (complete continuity is invariant under continuous linear equivalences).

Completely continuous maps are closed under addition, scalar multiplication and uniform approximation, under composition on either side with bounded continuous linear maps, and over Tate scalars under composition on either side with arbitrary continuous linear maps. The identity of a complete normed module is completely continuous exactly when the module is finitely generated: an approximant of finite rank within distance 1 / 2 of the identity is surjective (TauCeti.surjective_of_norm_sub_apply_le), so its range, which lies in a finitely generated submodule, is everything. Consequently a completely continuous u with (1 - u) ^ n = 0 forces the module to be finitely generated.

Main definitions

• ContinuousLinearMap.IsCompletelyContinuous: uniform approximability by continuous linear maps of finite rank, characterized by ContinuousLinearMap.isCompletelyContinuous_iff.

Main results

• LinearMap.IsFiniteRank.isCompletelyContinuous: continuous maps of finite rank are completely continuous.
• ContinuousLinearMap.isCompletelyContinuous_of_forall_approx, ContinuousLinearMap.isCompletelyContinuous_of_tendsto, ContinuousLinearMap.isClosed_setOf_isCompletelyContinuous: complete continuity is closed under uniform approximation, under operator-norm limits over Tate scalars, and is a closed condition over a nontrivially normed field.
• ContinuousLinearMap.isCompletelyContinuous_iff_forall_mapsTo, Filter.HasBasis.isCompletelyContinuous_iff_forall_mapsTo: the lattice criterion over Tate scalars, for a bounded neighbourhood of zero in the source and all (or a basis of) neighbourhoods of zero in the target.
• ContinuousLinearMap.IsCompletelyContinuous.clm_comp, ContinuousLinearMap.IsCompletelyContinuous.comp_clm: the ideal property over Tate scalars, and ContinuousLinearEquiv.comp_isCompletelyContinuous_iff, ContinuousLinearEquiv.isCompletelyContinuous_comp_iff: invariance under continuous linear equivalences, hence under equivalent norms.
• ContinuousLinearMap.IsCompletelyContinuous.clm_comp_of_bound, ContinuousLinearMap.IsCompletelyContinuous.comp_clm_of_bound: composition on either side with a bounded continuous linear map, over any ring.
• ContinuousLinearMap.isCompletelyContinuous_id_iff: the identity of a complete normed module is completely continuous if and only if the module is finitely generated.
• ContinuousLinearMap.IsCompletelyContinuous.finite_of_one_sub_pow_eq_zero: a completely continuous u with (1 - u) ^ n = 0 forces the module to be finitely generated.

References

• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §§2–3.
• R. Coleman, p-adic Banach spaces and families of modular forms, Invent. Math. 127 (1997), 417–479, Appendix A.
• C. Johansson and J. Newton, Extended eigenvarieties for overconvergent cohomology, arXiv:1604.07739, §2.1.

def ContinuousLinearMap.IsCompletelyContinuous {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] (u : M →L[R] N) : Prop

A continuous linear map u is completely continuous if it is a uniform limit of continuous linear maps of finite rank: for every ε > 0 there is a continuous linear v whose range lies in a finitely generated submodule with ‖u x - v x‖ ≤ ε * ‖x‖ for every x.

theorem ContinuousLinearMap.isCompletelyContinuous_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {u : M →L[R] N} : u.IsCompletelyContinuous ↔ ∀ (ε : ℝ), 0 < ε → ∃ (v : M →L[R] N), (↑v).IsFiniteRank ∧ ∀ (x : M), ‖u x - v x‖ ≤ ε * ‖x‖

Unfolding ContinuousLinearMap.IsCompletelyContinuous: u is completely continuous iff for every ε > 0 some continuous linear map of finite rank is uniformly ε-close to u.

theorem LinearMap.IsFiniteRank.isCompletelyContinuous {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {u : M →L[R] N} (hu : (↑u).IsFiniteRank) : u.IsCompletelyContinuous

A continuous linear map of finite rank is completely continuous.

@[simp]

theorem ContinuousLinearMap.isCompletelyContinuous_zero {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] : IsCompletelyContinuous 0

theorem ContinuousLinearMap.isCompletelyContinuous_of_finite {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] [Module.Finite R N] (u : M →L[R] N) : u.IsCompletelyContinuous

Every continuous linear map into a finitely generated module is completely continuous.

theorem ContinuousLinearMap.isCompletelyContinuous_of_forall_approx {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {u : M →L[R] N} (h : ∀ (ε : ℝ), 0 < ε → ∃ (v : M →L[R] N), v.IsCompletelyContinuous ∧ ∀ (x : M), ‖u x - v x‖ ≤ ε * ‖x‖) : u.IsCompletelyContinuous

Complete continuity is closed under uniform approximation. A continuous linear map that is, for every ε > 0, uniformly ε-close to a completely continuous map is completely continuous.

theorem ContinuousLinearMap.IsCompletelyContinuous.add {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {u u' : M →L[R] N} (hu : u.IsCompletelyContinuous) (hu' : u'.IsCompletelyContinuous) : (u + u').IsCompletelyContinuous

theorem ContinuousLinearMap.IsCompletelyContinuous.neg {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {u : M →L[R] N} (hu : u.IsCompletelyContinuous) : (-u).IsCompletelyContinuous

@[simp]

theorem ContinuousLinearMap.IsCompletelyContinuous.neg_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {u : M →L[R] N} : (-u).IsCompletelyContinuous ↔ u.IsCompletelyContinuous

Complete continuity is invariant under negation.

theorem ContinuousLinearMap.IsCompletelyContinuous.sub {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {u u' : M →L[R] N} (hu : u.IsCompletelyContinuous) (hu' : u'.IsCompletelyContinuous) : (u - u').IsCompletelyContinuous

theorem ContinuousLinearMap.IsCompletelyContinuous.smul {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {S : Type u_4} [SeminormedRing S] [DistribMulAction S N] [IsBoundedSMul S N] [SMulCommClass R S N] {u : M →L[R] N} (hu : u.IsCompletelyContinuous) (c : S) : (c • u).IsCompletelyContinuous

theorem ContinuousLinearMap.IsCompletelyContinuous.exists_isFiniteRank_mapsTo {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {u : M →L[R] N} (hu : u.IsCompletelyContinuous) {M₀ : Set M} (hM₀ : Bornology.IsBounded M₀) {V : Set N} (hV : V ∈ nhds 0) : ∃ (g : M →L[R] N), (↑g).IsFiniteRank ∧ Set.MapsTo (⇑(u - g)) M₀ V

A completely continuous map is approximated on every bounded set M₀ by continuous maps of finite rank, up to an arbitrary neighbourhood V of zero: some g of finite rank maps M₀ into V after subtraction from u.

theorem ContinuousLinearMap.IsCompletelyContinuous.clm_comp_of_bound {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {P : Type u_4} [SeminormedAddCommGroup P] [Module R P] {u : M →L[R] N} (hu : u.IsCompletelyContinuous) (g : N →L[R] P) {C : ℝ} (hC : 0 < C) (hg : ∀ (y : N), ‖g y‖ ≤ C * ‖y‖) : (g ∘SL u).IsCompletelyContinuous

Postcomposing a completely continuous map with a continuous linear map bounded by C, that is with ‖g y‖ ≤ C * ‖y‖, gives a completely continuous map. Over Tate scalars every continuous linear map is bounded (ContinuousLinearMap.IsCompletelyContinuous.clm_comp).

theorem ContinuousLinearMap.IsCompletelyContinuous.comp_clm_of_bound {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {L : Type u_4} [SeminormedAddCommGroup L] [Module R L] {u : M →L[R] N} (hu : u.IsCompletelyContinuous) (f : L →L[R] M) {C : ℝ} (hC : 0 < C) (hf : ∀ (x : L), ‖f x‖ ≤ C * ‖x‖) : (u ∘SL f).IsCompletelyContinuous

Precomposing a completely continuous map with a continuous linear map bounded by C, that is with ‖f x‖ ≤ C * ‖x‖, gives a completely continuous map. Over Tate scalars every continuous linear map is bounded (ContinuousLinearMap.IsCompletelyContinuous.comp_clm).

theorem ContinuousLinearMap.isCompletelyContinuous_iff_ringOpNorm {R : Type u_1} {M : Type u_3} {N : Type u_4} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [Module R N] [IsBoundedSMul R N] {u : M →L[R] N} : u.IsCompletelyContinuous ↔ ∀ (ε : ℝ), 0 < ε → ∃ (v : M →L[R] N), (↑v).IsFiniteRank ∧ ‖u - v‖ < ε

Over Tate scalars, a continuous linear map is completely continuous if and only if it is a limit of continuous maps of finite rank in the operator norm.

theorem ContinuousLinearMap.isCompletelyContinuous_of_tendsto {R : Type u_1} {M : Type u_3} {N : Type u_4} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [Module R N] [IsBoundedSMul R N] {ι : Type u_6} {l : Filter ι} [l.NeBot] {u : M →L[R] N} {v : ι → M →L[R] N} (h : Filter.Tendsto (fun (i : ι) => ‖u - v i‖) l (nhds 0)) (hv : ∀ᶠ (i : ι) in l, (v i).IsCompletelyContinuous) : u.IsCompletelyContinuous

Over Tate scalars, an operator-norm limit of completely continuous maps is completely continuous.

theorem ContinuousLinearMap.isCompletelyContinuous_iff_forall_mapsTo {R : Type u_1} {M : Type u_3} {N : Type u_4} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [Module R N] [IsBoundedSMul R N] {u : M →L[R] N} {M₀ : Set M} (hM₀ : M₀ ∈ nhds 0) (hbdd : Bornology.IsBounded M₀) : u.IsCompletelyContinuous ↔ ∀ V ∈ nhds 0, ∃ (g : M →L[R] N), (↑g).IsFiniteRank ∧ Set.MapsTo (⇑(u - g)) M₀ V

The lattice criterion for complete continuity. Over Tate scalars, let M₀ be a bounded neighbourhood of zero in M, such as a bounded open lattice. A continuous linear map u is completely continuous if and only if for every neighbourhood V of zero in N some continuous map g of finite rank satisfies (u - g)(M₀) ⊆ V.

The condition only involves the neighbourhoods of zero in N and the set M₀, so replacing M₀ by another bounded neighbourhood of zero does not change it.

theorem Filter.HasBasis.isCompletelyContinuous_iff_forall_mapsTo {R : Type u_1} {M : Type u_3} {N : Type u_4} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [Module R N] [IsBoundedSMul R N] {ι : Sort u_6} {p : ι → Prop} {V : ι → Set N} (hV : (nhds 0).HasBasis p V) {u : M →L[R] N} {M₀ : Set M} (hM₀ : M₀ ∈ nhds 0) (hbdd : Bornology.IsBounded M₀) : u.IsCompletelyContinuous ↔ ∀ (i : ι), p i → ∃ (g : M →L[R] N), (↑g).IsFiniteRank ∧ Set.MapsTo (⇑(u - g)) M₀ (V i)

The lattice criterion ContinuousLinearMap.isCompletelyContinuous_iff_forall_mapsTo with the neighbourhoods of zero in N restricted to a basis, such as a basis of open lattices.

theorem ContinuousLinearMap.IsCompletelyContinuous.clm_comp {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] [IsBoundedSMul R N] [SeminormedAddCommGroup P] [Module R P] [IsBoundedSMul R P] {u : M →L[R] N} (hu : u.IsCompletelyContinuous) (g : N →L[R] P) : (g ∘SL u).IsCompletelyContinuous

Over Tate scalars, postcomposing a completely continuous map with a continuous linear map gives a completely continuous map.

theorem ContinuousLinearMap.IsCompletelyContinuous.comp_clm {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup L] [Module R L] [IsBoundedSMul R L] [SeminormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [Module R N] {u : M →L[R] N} (hu : u.IsCompletelyContinuous) (f : L →L[R] M) : (u ∘SL f).IsCompletelyContinuous

Over Tate scalars, precomposing a completely continuous map with a continuous linear map gives a completely continuous map.

@[simp]

theorem ContinuousLinearEquiv.comp_isCompletelyContinuous_iff {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] [IsBoundedSMul R N] [SeminormedAddCommGroup P] [Module R P] [IsBoundedSMul R P] (e : N ≃L[R] P) {u : M →L[R] N} : (↑e ∘SL u).IsCompletelyContinuous ↔ u.IsCompletelyContinuous

Over Tate scalars, complete continuity is unchanged by postcomposition with a continuous linear equivalence; in particular it does not depend on the choice of an equivalent norm on the target.

@[simp]

theorem ContinuousLinearEquiv.isCompletelyContinuous_comp_iff {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup L] [Module R L] [IsBoundedSMul R L] [SeminormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [Module R N] (e : L ≃L[R] M) {u : M →L[R] N} : (u ∘SL ↑e).IsCompletelyContinuous ↔ u.IsCompletelyContinuous

Over Tate scalars, complete continuity is unchanged by precomposition with a continuous linear equivalence; in particular it does not depend on the choice of an equivalent norm on the source.

theorem ContinuousLinearMap.isClosed_setOf_isCompletelyContinuous {K : Type u_1} {M : Type u_2} {N : Type u_3} [NontriviallyNormedField K] [SeminormedAddCommGroup M] [NormedSpace K M] [SeminormedAddCommGroup N] [NormedSpace K N] : IsClosed {u : M →L[K] N | u.IsCompletelyContinuous}

Over a nontrivially normed field, the completely continuous maps form a closed subset of the space of continuous linear maps.

theorem ContinuousLinearMap.isCompletelyContinuous_id_iff {R : Type u_1} {M : Type u_2} [Ring R] [NormedAddCommGroup M] [Module R M] [CompleteSpace M] : (ContinuousLinearMap.id R M).IsCompletelyContinuous ↔ Module.Finite R M

The identity criterion. The identity of a complete normed module is completely continuous if and only if the module is finitely generated.

theorem ContinuousLinearMap.IsCompletelyContinuous.finite_of_one_sub_pow_eq_zero {R : Type u_1} {M : Type u_2} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [CompleteSpace M] {u : M →L[R] M} (hu : u.IsCompletelyContinuous) {n : ℕ} (hn : (1 - u) ^ n = 0) : Module.Finite R M

Over Tate scalars, a completely continuous endomorphism u of a complete normed module with (1 - u) ^ n = 0 forces the module to be finitely generated, since u then has the right inverse ∑_{k < n} (1 - u) ^ k.