Define Fredholm operators

[ADedecker]

Bourbaki, Théories Spectrales, Chapitres 3 à 5 contains a (imo) very nice presentation of Fredholm operators, which I think is very suitable for Mathlib. Hence, instead of the more common definition given on Wikipedia, I suggest the following start for the theory:

• Define a predicate LinearMap.FiniteRank expressing that the range of a linear map is finite. Show that it's stable under addition and composition by an arbitrary linear map.
• Define a predicate ContinuousLinearMap.EqModFinite (probably with a fancy notation like ≡ᶠ) saying that the difference between two operators E →L[𝕜] F has finite rank. Show that it behaves well under composition and addition of operators.
• Define a Fredholm pair to be a pair of bounded operator T : E →L[𝕜] F and S : F →L[𝕜] E between TVSs such that both (S ∘L T) ≡ᶠ ContinuousLinearMap.id 𝕜 E and (T ∘L S) ≡ᶠ ContinuousLinearMap.id 𝕜 F. Show that being a Fredholm pair is symmetric, and behaves well with composition of operators.
• An operator T is Fredholm if there exists S such that (T, S) is a Fredholm pair. The composition of two Fredholm operators is Fredholm;
  adding a finite rank operator to a Fredholm operator gives a Fredholm operator.
• A Fredholm operator has finite dimensional kernel and cokernel

The next important theorem will be to prove that an operator is Fredholm if and only if it is strict, has finite dimensional kernel and cokernel, and has closed range. This will rely crucially on #38471.

Some design decisions I'd be happy to discuss :

• The relation ≡ᶠ is just equality modulo the submodule of finite rank operators. Is that a better definition? Note that we can't use the Ideal API because we don't want to force E = F.
• I made up the name "Fredholm pair". We could also say that S is a "Fredholm inverse" or "quasi-inverse" to T. Note that, after much work, we will get that an operator is Fredholm if and only if it admits an inverse modulo compact operators, so there are really two notions of "almost inverse" interacting.

[CoolRmal]

I saw on Wikipedia that there's a notion of Semi-Fredholm operator. Do you know whether the framework you proposed also allows us to define this notion? Admittedly I know nothing about Semi-Fredholm operators so I am also not sure whether it is worth to include this notion in Mathlib.

[ADedecker]

@CoolRmal I finally found some time to think about your question. Unfortunately I think the answer is no: if S is a closed submodule of a banach space E, then the inclusion map S -> E is semi-fredholm according to Wikipedia's definition, but if S is not complemented I don't see how you would build a "left-inverse-up-to-finite-rank".

I'm tempted to say it's not too bad, because in any case we want to have different definitions for the three notions, so it's not a big deal if the definitions look a bit different. What do you think?

[CoolRmal]

I did some literature review and I found the following theorem in this book (Theorem 13, 14, 15 in Chapter 16): if T has closed range and finite dimensional kernel, then the range of T is complemented iff there exists an operator S such that (S ∘ T) ≡ᶠ id.

Based on this theorem and its analogue for the lower semi-Fredholm operators, I propose the following modifications to your framework:

1. We define 4 types of semi-Fredholm operators.
   • An operator T : E →L[𝕜] F is said to be left essentially invertible (the name left semi-Fredholm is also used in the literature) if there exists S : F →L[𝕜] E such that (S ∘L T) ≡ᶠ ContinuousLinearMap.id 𝕜 E. Right essentially invertiable operators are defined in a similar way.
   • An operator T : E →L[𝕜] F is said to be upper semi-Fredholm if it has closed range and finite dimensional kernel. It is said to be lower semi-Fredholm if it has finite dimensional cokernel. It is said to be semi-Fredholm if it is either upper semi-Fredholm or lower semi-Fredholm.
2. We say that an operator is Fredholm if it is both left and right essentially invertible (so basically the same definition you mentioned above).
3. We prove that an operator is left essentially invertible iff it is upper semi-Fredholm and its range is complemented. At least according to the book it is true for Banach spaces, we can check what we should do for more general tvs.
4. We prove that an operator is right essentially invertible iff it is lower semi-Fredholm and its kernel is complemented.
5. Then it follows from 3 and 4 that an operator is Fredholm iff it is both upper and lower semi-Fredholm (as finite (co)dim subspaces are complemented).
6. We prove that the property of being left essentially invertible is stable under finite/compact pertubations.
7. We prove that the property of being right essentially invertible is stable under finite/compact pertubations.
8. Then it follows from 6 and 7 that being Fredholm is stable under finite/compact pertubations.
9. We prove that the set of upper semi-Fredholm operators is open by showing that dim(ker T) does not increase after being pertubed by an operator of sufficiently small norm.
10. We prove that the set of low semi-Fredholm operators is open by showing that codim(range T) does not increase after being pertubed by an operator of sufficiently small norm.
11. The it follows from 9 and 10 that the set of Fredholm operators is open as it is the intersection of two open sets. The set of semi-Fredholm operators is also open as it is the union of two open sets.
12. ...

My main point is that after we define all these different notions of semi-Fredholm operators, we can obtain properties of Fredholm operators easily from the ones of semi-Fredholm operators, and along the way we generate many more APIs.

One main concern I have now is that we also want to define index for a semi-Fredholm operator and show that it is locally constant, which is naturally an element of the type EInt, and I don't think we have a lot APIs for that.

What do you think?

[ADedecker]

Indeed the precise question was complementedness of the kernel/cokernel when we no longer assume it has finite dimension. If you assume it, then indeed there is no trouble (even in the locally convex setting, and in fact I think even in the TVS setting) with the left/right inverse approach.

But it seemed like people don't usually put complementedness in the definition of semi-Fredholm, which is why I concluded that my approach didn't work satisfyingly in the semi-Fredholm case.

I'll make more comments tomorrow (if I get time for it, otherwise we can discuss all of this at ICERM).

[ADedecker]

Re: generating more API

Of course I completely agree! But when doing so we have to match what people actually care about, not just what allows us to write more theorems. So restricting to semi-Fredholm operators with complemented range and kernel just because this is what we get from the usual theory is a bit sad if it means people can't then apply these results to their favorite semi-Fredholm operator.

[CoolRmal]

I think there's a bit misunderstanding here. I am not saying that we should define semi-Fredholm operators with complemented range and kernel. I am suggesting that we should define all these different notions of semi-Fredholm operators and prove that some of them are equivalent under an additional assumption that the range/kernel is complemented.

There are basically two approaches for the semi-Fredholm operators: the left-right one and the upper-lower one. The left-right one (the one you suggested) allows us to get some sort of inverses easily and it seems like that it is easy to prove that being Fredholm is stable under finite pertubations in this setting. The upper-lower one is the natural setting to define the index and it seems like that it is easy to prove that the set of Fredholm operators is open in this setting (by showing that dim (ker T) and codim (range T) are upper semicontinuous functions in the natural domains). We then create a connection between these two approaches with an additional assumption that the range/kernel is complemented.