Fredholm operators of index zero are the finite-rank and the compact perturbations of isomorphisms

Proved

FredholmBanach.index_eq_zero_tfae

by Mazecto · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

banach-spacescompact-operatorsfredholm-operatorsfunctional-analysisoperator-theory

Let $\mathbb{K}$ be $\mathbb{R}$ or $\mathbb{C}$ and let $E$ , $F$ be Banach spaces over $\mathbb{K}$ . For a bounded linear map $u:E\to F$ the following are equivalent:

$u$ is a Fredholm operator and $\operatorname{ind}u=0$ , where $\operatorname{ind}u=\dim\operatorname{Ker}u-\dim(F/\operatorname{Im}u)$ ;
there is an isomorphism $e:E\to F$ (a continuous linear bijection with continuous inverse) such that $u-e$ has finite-dimensional range;
there is an isomorphism $e:E\to F$ such that $u-e$ is a compact operator.

Preamble

import Definitions.Def_FredholmBanach_Setting

Formal statement

namespace FredholmBanach

open Topology

/-- Bourbaki, *Théories spectrales*, III, § 5, n° 3, Corollaire 2 (TS III.74), for Banach spaces:
the following are equivalent: `u` is Fredholm of index `0`; `u` differs from an isomorphism
`E ≃L[𝕜] F` by an operator of finite rank; `u` differs from an isomorphism by a compact
operator. -/
theorem index_eq_zero_tfae {𝕜 E F : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F]
    (u : E →L[𝕜] F) :
    [u.IsFredholm ∧ index u = 0,
      ∃ e : E ≃L[𝕜] F, FiniteDimensional 𝕜 (u - (e : E →L[𝕜] F)).range,
      ∃ e : E ≃L[𝕜] F, IsCompactOperator (u - (e : E →L[𝕜] F))].TFAE := by sorry

end FredholmBanach

Source

N. Bourbaki, Théories spectrales, Chapitres III à V, Springer (2023), https://doi.org/10.1007/978-3-031-19505-1, Chapitre III, § 5, n° 3, Corollaire 2, pp. TS III.74–III.75 (stated there for separated locally convex spaces)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back: `FredholmBanach.index_eq_zero_tfae`

Setting. $\mathbb{K}$ is $\mathbb{R}$ or $\mathbb{C}$ (RCLike). $E$ , $F$ are Banach spaces over $\mathbb{K}$ . $u : E \to F$ is a bounded linear map.

Definitions used.

u.IsFredholm: $u$ is a strict map (quotient map onto its range), has closed range, finite-dimensional kernel, finite-dimensional algebraic cokernel $F/u(E)$ , and topologically complemented kernel.
index u $= \dim\ker u - \dim(F/u(E))$ (finrank, $0$ on infinite-dimensional spaces).
E ≃L[𝕜] F: a continuous linear equivalence, i.e. a linear bijection $e$ with $e$ and $e^{-1}$ both bounded (a topological isomorphism). (e : E →L[𝕜] F) is $e$ viewed as a bounded map.
FiniteDimensional 𝕜 (u - e).range: the (algebraic) range of $u - e$ is finite-dimensional, i.e. $u-e$ has finite rank.
IsCompactOperator (u - e): $u-e$ maps some neighbourhood of $0$ into a compact set.
List.TFAE [P₁, P₂, P₃]: the three propositions are pairwise equivalent.

Assertion. The following are equivalent:

$u$ is Fredholm and $\operatorname{ind} u = 0$ ;
there is a topological isomorphism $e : E \to F$ such that $u - e$ has finite rank;
there is a topological isomorphism $e : E \to F$ such that $u - e$ is compact.

Degenerate cases / remarks.

If $E$ and $F$ are not isomorphic as Banach spaces, (2) and (3) are false, so the theorem asserts that no Fredholm operator of index $0$ exists from $E$ to $F$ . (Consistent: an index-0 Fredholm map yields such an isomorphism.)
$E = F = 0$ : all three hold. Finite-dimensional $E$ , $F$ : (1) says $\dim E = \dim F$ , as do (2) and (3).
In (1), index u = 0 is only read for Fredholm $u$ (conjoined), so the junk value does not matter; index $0$ is sign-convention independent.
"Finite rank" is stated as the algebraic range being finite-dimensional, with no closedness or continuity issue (the map is already bounded).

No mis-formalization detected.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Fredholm operators of index zero are the finite-rank and the compact perturbations of isomorphisms

Read-back: FredholmBanach.index_eq_zero_tfae

Read-back: `FredholmBanach.index_eq_zero_tfae`