Fredholm operators between topological vector spaces #

Fix 𝕜 a complete NontriviallyNormedField, and let E, F be two Hausdorff topological vector spaces over 𝕜.

We say that a continuous linear map T : E →L[𝕜] F is a Fredholm operator if it satisfies the following four equivalent conditions:

T is strict, its range is closed and has finite codimension, and its kernel is (topologically) complemented and has finite dimension. This is chosen as the definition, see IsFredholm.
T admits a continuous quasi-inverse, in the sense of LinearMap.IsQuasiInverse.
There are closed finite-codimension subspaces E₁ and F₁ of E and F between which T induces an isomorphism.
T admits a FredholmPackage: there are topological decompositions E = E₁ ⊕ E₀, F = F₁ ⊕ F₀, where E₀ and F₀ are finite dimensional, and an isomorphism Φ : E₁ ≃L[𝕜] F₁ such that T is zero on E₀ and coincides with Φ on E₁; in other words, in these decompositions, T is given by the matrix $\begin{pmatrix} Φ & 0 \cr 0 & 0 \end{pmatrix}$.

Main definitions #

ContinuousLinearMap.IsFredholm: a continuous linear map u : E →L[𝕜] F is a Fredholm operator if it is strict, its range is closed and has finite codimension, and its kernel is (topologically) complemented and has finite dimension.
FredholmDecomposition: a Fredholm decomposition of a topological vector space E is the data of two subspaces X₀ and X₁ which are topological complements, and where X₀ is finite dimensional.
ContinuousLinearMap.FredholmPackage: a Fredholm package for u : E →L[𝕜] F is the data of Fredholm decompositions decDom and decCodom of E and F respectively, together with a continuous linear equivalence equiv : decDom.X₁ ≃L[𝕜] decCodom.X₁ between the "essential" (i.e. finite codimension) parts of these decompositions, such that u equals the composition decCodom.X₁.subtypeL ∘L equiv ∘L decDom.proj.

Note that the data of a FredholmPackage for an operator is morally the strongest of the equivalent ways to assume that u is Fredholm (for example, it is clear how to build a canonical continuous quasi-inverse of u from such a package).

Hence, you should not typically prove that an operator is Fredholm by building a Fredholm package (consider using IsFredholm.of_isInvertible_restrict); instead, when you know that an operator is Fredholm, you can obtain a FredholmPackage from IsFredholm.nonempty_fredholmPackage in order to conveniently use the full strength of Fredholmness.

Main statements #

Equivalent criteria #

ContinuousLinearMap.isFredholm_tfae: the equivalence between conditions 1, 2, 3 and 4 above. In practice, most of the interesting directions should be covered by specific API lemmas.
ContinuousLinearMap.FredholmPackage.isQuasiInverse: given a FredholmPackage for u, one can build a canonical continuous quasi-inverse of u.
ContinuousLinearMap.IsFredholm.of_isInvertible_restrict: if a continuous linear map induces an isomorphism between finite codimension subspaces, then it is Fredholm.
ContinuousLinearMap.IsFredholm.of_restrict (not in Mathlib yet) is a generalization of the above: if a continuous linear map induces a Fredholm operator between finite codimension subspaces, then the original map is Fredholm as well.
IsFredholm.nonempty_fredholmPackage: every Fredholm operator admits a Fredholm package. This is the primary way to obtain Fredholm packages.

Implementation details #

We largely follow N. Bourbaki, Théories Spectrales, Chapitre III, § 3, n° 2, in particular for the proof of equivalence of the four conditions above. Here are some notable changes:

Bourbaki restricts itself to locally convex spaces over ℝ or ℂ. Yet, under close inspection, this assumption plays very little role in the beginning of the theory. In fact, at the very mild cost of assuming that the kernel is complemented in the definition of IsFredholm (which follows from the finiteness assumption if Hahn-Banach is available), we generalize the beginning of the theory to topological vector spaces over any complete nontrivially normed field. In particular, our theory naturally captures p-adic Fredholm operators.
Bourbaki chooses the existence of a continuous quasi-inverse as the definition of being Fredholm. Our choice differs for a very practical reason: it is much simpler to spell out formally "u has a continuous quasi-inverse" than "u is strict, its range is closed and has finite codimension, and its kernel is complemented and has finite dimension". Hence we prefer to give a name to the latter.

References #