Fredholm operators between Banach spaces are those with finite-dimensional kernel and cokernel

Proved

FredholmBanach.isFredholm_iff_finiteDimensional

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}$ . A bounded linear map $u:E\to F$ is Fredholm (in the sense of Mathlib's ContinuousLinearMap.IsFredholm) if and only if $\operatorname{Ker}u$ and $F/\operatorname{Im}u$ are finite-dimensional.

Preamble

import Definitions.Def_FredholmBanach_Setting

Formal statement

namespace FredholmBanach

open Topology

/-- Bourbaki, *Théories spectrales*, III, § 3, n° 5, Proposition 11 (TS III.52), for Banach
spaces: `u` is Fredholm if and only if its kernel and its cokernel `F ⧸ Im u` are
finite-dimensional. -/
theorem isFredholm_iff_finiteDimensional {𝕜 E F : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F]
    (u : E →L[𝕜] F) :
    u.IsFredholm ↔ FiniteDimensional 𝕜 u.ker ∧ FiniteDimensional 𝕜 (F ⧸ u.range) := 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, § 3, n° 5, Proposition 11, p. TS III.52 (stated there for Fréchet spaces)

Read-back

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

Read-back: `FredholmBanach.isFredholm_iff_finiteDimensional`

Setting. $\mathbb{K} \in \{\mathbb{R}, \mathbb{C}\}$ (RCLike 𝕜); $E, F$ Banach spaces over $\mathbb{K}$ (normed, complete); $u : E \to F$ a continuous linear map. No further hypotheses.

Definition used: u.IsFredholm (Mathlib ContinuousLinearMap.IsFredholm) is the conjunction of five fields:

isStrictMap: $u$ is strict, i.e. the corestriction $E \to u(E)$ is a topological quotient map ( $u$ is open onto its range with the subspace topology);
isClosed_range: $u(E)$ is closed in $F$ ;
finite_ker: $\ker u$ is finite-dimensional;
finite_coker: u.range.CoFG, i.e. the algebraic quotient $F/u(E)$ is finitely generated, i.e. finite-dimensional;
closedComplemented_ker: $\ker u$ is topologically complemented, i.e. there is a continuous linear projection $E \to \ker u$ restricting to the identity on $\ker u$ .

Assertion.

u \text{ is Fredholm} \iff \dim_{\mathbb{K}} \ker u < \infty \ \text{ and } \ \dim_{\mathbb{K}} \bigl(F/u(E)\bigr) < \infty,

where $F/u(E)$ is the algebraic quotient by the (a priori not closed) range.

So for Banach spaces over $\mathbb{R}$ or $\mathbb{C}$ , the three topological conditions (strictness, closed range, complemented kernel) are claimed to be automatic once kernel and algebraic cokernel are finite-dimensional. The forward direction is essentially a projection of fields 3 and 4; the content is the backward direction.

Degenerate cases.

$E, F$ finite-dimensional: right side always true, so every linear map is claimed Fredholm (correct).
$E = 0$ : $u = 0$ , Fredholm iff $F$ finite-dimensional.
Isomorphisms: both sides true.

Remarks. Completeness of both spaces is assumed, and is needed. The cokernel is algebraic, matching Bourbaki Prop. 11. The statement is a genuine biconditional, not vacuous. No mis-formalization spotted.

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 between Banach spaces are those with finite-dimensional kernel and cokernel

Read-back: FredholmBanach.isFredholm_iff_finiteDimensional

Read-back: `FredholmBanach.isFredholm_iff_finiteDimensional`