Finite rank continuous linear map is compact

Stream: Is there code for X?

[Niels Voss]

Is there an easy way to prove something along these lines?

import Mathlib

-- A continuous linear map T between Banach spaces of rank n is a compact operator
example (𝕜 : Type*) [NontriviallyNormedField 𝕜] (X Y : Type*)
  [NormedAddCommGroup X] [NormedSpace 𝕜 X] [CompleteSpace X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [CompleteSpace Y]
  (T : X →L[𝕜] Y) (n : ℕ) (hT : T.rank = n) : IsCompactOperator T := by
  sorry

[Kevin Buzzard]

Looking at the definition of docs#IsCompactOperator I am slightly concerned that it is incorrect for fields which are not locally compact (for example for Banach spaces over the field $\mathbb{C}_p$, for which there's a well-established theory of compact operators). Are you sure that this result is true in the generality in which you've stated it?

[Kevin Buzzard]

For example I would ike the identity map from $\mathbb{C}_p$ (docs#PadicComplex) to itself to be a compact operator and I am not at all sure that it is with mathlib's definition, because 0 has no compact neighbourhood.

[Moritz Doll]

I am pretty sure you need [LocallyCompactSpace 𝕜]

[Kevin Buzzard]

Well in the nonarchimedean world I am 100% sure that you do not, if we are following the human literature, however we will need it with mathlib's current definition of IsCompactOperator.

[Kevin Buzzard]

One (correct) definition of a compact operator between Banach spaces over a nontrivially normed nonarchimedean field is a limit of finite rank operators.

[Moritz Doll]

Sorry, I meant to do the usual proof, I don't know anything about the non-archimedean world

[Moritz Doll]

and with the current definition

[Kevin Buzzard]

It might be best to split the theory as early as possible here; in the nonarchimedean world concepts like being trace class and compact all coincide, and they're all "limit of finite rank operators". In the local class field theory project we are not making any attempt to unify the arguments for nonarchimedean and archimedean local fields, for example, we just develop the two theories completely separately and then prove the same theorems.

[Moritz Doll]

Kevin Buzzard said:

One definition of a compact operator between Banach spaces over a nontrivially normed nonarchimedean field is a limit of finite rank operators.

Yes, this is also typically the definition in functional analysis (or at least one characterization)

[Kevin Buzzard]

But you just indicated that for non-locally-compact fields then these definitions do not coincide (consider the identity function $k\to k$). So what exactly is the definition in the archimedean world? Or is what's going on that you always assume your nontrivially normed fields are locally compact? This is definitely not true in the nonarchimedean world, there are no locally compact algebraically closed fields complete with respect to a nontrivial nonarchimdedean norm so local compactness is definitely something you want to avoid assuming when doing nonarchimedean functional analysis.

[Moritz Doll]

My fields are either the reals or the complex numbers

[Kevin Buzzard]

Oh wow, boy are you missing out ;-) OK interesting! I had not ever seen this definition of a compact operator before because I've only read the nonarchimedean literature. It's not right in the nonarchimedean case (in the sense that it doesn't agree with the literature, which in this case includes my papers).

[Kevin Buzzard]

For now Niels I would just add the locally compact assumption.

[Kevin Buzzard]

In Serre's foundational paper on the subject (reinterpreting Dwork's work which had just proved some parts of the Weil conjectures) he calls these operators "complètement continus" and it always struck me as odd why he didn't call them compact, I just figured that the term compact was not used in the French literature.. Now I'm wondering whether he was making a careful distinction.

[Niels Voss]

Once I make the locally compact assumption, is there a theorem in mathlib I can use to show that a finite rank operator is compact?

[Moritz Doll]

@Niels Voss I've tried to prove it, but there is a bit of weirdness in the IsCompactOperator file: the predicate is defined for any map, but then there are theorems only stated for linear maps, not the corresponding class so using continuous linear maps is a pain.

-- A continuous linear map T between Banach spaces of rank n is a compact operator
example (𝕜 : Type*) [NontriviallyNormedField 𝕜] [LocallyCompactSpace 𝕜] (X Y : Type*)
  [NormedAddCommGroup X] [NormedSpace 𝕜 X] [CompleteSpace X] [NormedAddCommGroup Y]
  [NormedSpace 𝕜 Y] [CompleteSpace Y]
  (T : X →L[𝕜] Y) (n : ℕ) (hT : T.rank = n) : IsCompactOperator T := by
  letI : FiniteDimensional 𝕜 (LinearMap.range T.toLinearMap) :=
    Module.finite_of_rank_eq_nat hT
  letI := FiniteDimensional.proper 𝕜 (LinearMap.range T.toLinearMap)
  let T₁ : X →L[𝕜] (LinearMap.range T.toLinearMap) :=
    T.codRestrict (LinearMap.range T.toLinearMap) (by simp)
  let T' : X →L[𝕜] Y := (LinearMap.range T.toLinearMap).subtypeL ∘L T₁
  have : IsCompactOperator T' := by
    apply (isCompactOperator_iff_image_closedBall_subset_compact T'.toLinearMap zero_lt_one).mpr
    sorry
  exact this

[Moritz Doll]

I think one can get around with enough apply foo.mpr nonsense, but it is not ideal
The above reduces to an easy to prove (hopefully) statement

[Jireh Loreaux]

@Kevin Buzzard the "completely continuous" terminology used to be the standard name for compact operators in functional analysis too. I'm fairly certain the reason for this is that they are still continuous when you equip the domain with the weak topology and the codomain with the norm topology (as opposed to norm on both).

[Sébastien Gouëzel]

Moritz Doll said:

Kevin Buzzard said:

One definition of a compact operator between Banach spaces over a nontrivially normed nonarchimedean field is a limit of finite rank operators.

Yes, this is also typically the definition in functional analysis (or at least one characterization)

I don't think that's true: there are compact operators (in the usual real or complex sense) which are not limits of finite rank operators (on exotic Banach spaces, though). The other direction is always true: a limit of finite rank operators is always compact.

[Sébastien Gouëzel]

So if it's not possible to unify the two variants of this notion in the literature, we should probably have two names. I'd claim IsCompact should be reserved for the notion that involves compactness (i.e., the image of the closed unit ball is compact), and for limits of finite rank operators IsFiniteRankLimit?

[Moritz Doll]

Oh no, you are right: that is exactly the Per Enflo theorem: https://en.wikipedia.org/wiki/Approximation_property

[Kevin Buzzard]

Yes it definitely sounds like we need two definitions. Another possibility is that we just namespace things (this might be my preference). This example will I think just be one of several. There are examples in the literature where people attempt to unify archimedean and nonarchimedean analysis and there are basic results which go through in both settings, but beyond some point every proof is of the form "in the archimedean case we do this, and in the nonarchimedean case we do that".

In the book by Jacquet and Langlands https://sunsite.ubc.ca/DigitalMathArchive/Langlands/pdf/jl-ps.pdf I remember having real trouble getting beyond the first line of p2 of the book (p6 of the pdf) because it says "let S(K) be the space of (complex-valued) Schwarz-Bruhat functions on K" where K is a finite-dimensional algebra over the local field F (so F can be the reals, complexes, or a finite extension of $\mathbb{Q}_p$ or of $\Z/p/Z((t))$) and they never define this concept. Ultimately I convinced myself that they must mean "a Schwarz function if $F$ is the reals or complexes, and a locally constant function with compact support if $F$ is nonarchimedean". When it comes to formalization I think there is very little point attempting to find some definition of Schwarz-Bruhat function which specialises to both of these things and then doing some contortions to prove the "theorem" that these functions are what I say they are in these two cases. If you look on page i of the book (p2 of the pdf) you will see that in "Chapter 1" there is only one section (the first section) where they attempt to develop the theory in parallel in the archimedean and nonarchimedean case; after that every section is either specific to the archimdedean or nonarchimedean case and they are basically confessing that the stories are analogous rather than special cases of one underlying collection of theorems which apply in both cases (the complex representation theory of GL_2(F) is far more subtle in the nonarchimedean case because of the existence of supercuspidal representations which have no analogue in the archimedean case).

Oh, in fact there is actually a Wikipedia article on Schwarz-Bruhat functions! And indeed it does attempt to give a very convoluted definition which works in the general case. I think that this is just ridiculous; I think that we should have IsROrC.SchwarzBruhatSpace, IsNonarchimedeanLocalField.SchwarzBruhatSpace etc. Maybe the same is true for compact operators -- one could attempt to jump through some hoops or one could suggest that there is an amicable divorce between the archimedean and nonarchimedean people and we retreat into our own namespaces. As a nonarchimedean person I could never stand your insistance of choosing a square root of $-1$ anyway -- you never seemed to understand that you can define complex conjugation perfectly well without making any such choice (and that this is important for people who want to complete a general number field at an infinite place).

[Sébastien Gouëzel]

Namespacing in this specific case does not look like a good idea to me, because the notion of limit of finite rank operators makes perfect sense over R or C, and it is interesting there: the famous Grothendieck question solved by Enflo is asking whether there are compact operators which are not limits of finite rank operators -- to state it, you need both notions in the real world, so having one of them called NonArchimedean.IsCompact would feel very strange.

[Kevin Buzzard]

Oh ok, if this distinction is important to you in the archimedean setting then we need different names.