Atkinson's theorem: Fredholm operators are the operators invertible modulo compact operators

Proved

FredholmBanach.isFredholm_iff_exists_compact_quasiInverse

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 a Fredholm operator if and only if there is a bounded linear map $v:F\to E$ such that both

1_E-v\circ u\quad\text{and}\quad 1_F-u\circ v

are compact operators (each maps some neighbourhood of $0$ into a compact set).

This identifies the Fredholm operators with the operators that are invertible modulo the compact operators.

Preamble

import Definitions.Def_FredholmBanach_Setting

Formal statement

namespace FredholmBanach

open Topology

/-- Bourbaki, *Théories spectrales*, III, § 5, n° 3, Corollaire 1 (TS III.74), for Banach spaces
(Atkinson's theorem): `u` is Fredholm if and only if there is `v : F →L[𝕜] E` such that
`1_E - v ∘ u` and `1_F - u ∘ v` are compact operators. -/
theorem isFredholm_iff_exists_compact_quasiInverse {𝕜 E F : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F]
    (u : E →L[𝕜] F) :
    u.IsFredholm ↔ ∃ v : F →L[𝕜] E,
      IsCompactOperator (ContinuousLinearMap.id 𝕜 E - v.comp u) ∧
        IsCompactOperator (ContinuousLinearMap.id 𝕜 F - u.comp v) := 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 1, p. TS III.74 (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.isFredholm_iff_exists_compact_quasiInverse`

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 (Mathlib): (i) strict map, i.e. $E \to u(E)$ is a topological quotient map; (ii) $u(E)$ closed; (iii) $\dim\ker u<\infty$ ; (iv) the algebraic quotient $F/u(E)$ is finite-dimensional; (v) there is a continuous linear projection of $E$ onto $\ker u$ .
v : F →L[𝕜] E: a bounded linear map in the reverse direction. v.comp u $= v\circ u : E\to E$ , u.comp v $= u\circ v : F \to F$ . ContinuousLinearMap.id 𝕜 E is $1_E$ .
IsCompactOperator T: $T$ maps some neighbourhood of $0$ into a compact set (standard compact operator).

Assertion. $u$ is Fredholm if and only if there exists a bounded linear $v : F \to E$ such that both

1_E - v\circ u \quad\text{and}\quad 1_F - u\circ v

are compact operators.

(Atkinson-type characterization: $u$ is invertible modulo compact operators on both sides by the same $v$ .)

Degenerate cases / remarks.

If $E$ and $F$ are finite-dimensional, every operator is compact and every $u$ is Fredholm; both sides are true (take $v=0$ ).
If $E$ is finite-dimensional and $F$ infinite-dimensional: $u$ is never Fredholm (cokernel infinite-dimensional), and the right side fails since $1_F - u\circ v$ is $1_F$ minus a finite-rank map, not compact. Consistent.
A single $v$ is required for both one-sided conditions; this is the standard form and not stronger than the two-sided-separately form (a left and a right quasi-inverse modulo compacts can be taken equal).
index is not used.

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

Atkinson's theorem: Fredholm operators are the operators invertible modulo compact operators

Read-back: FredholmBanach.isFredholm_iff_exists_compact_quasiInverse

Read-back: `FredholmBanach.isFredholm_iff_exists_compact_quasiInverse`