The index $\dim\operatorname{Ker}u-\dim\operatorname{Coker}u$ of a Fredholm operator

Definition

FredholmBanach_Setting

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

banach-spacescompact-operatorsfredholm-operatorsfunctional-analysisoperator-theory

The index of a Fredholm operator between normed spaces, following N. Bourbaki, Théories spectrales, Chapitre III, § 3, n° 3 (TS III.43).

Let $\mathbb{K}$ be $\mathbb{R}$ or $\mathbb{C}$ , let $E$ , $F$ be normed spaces over $\mathbb{K}$ and let $u:E\to F$ be a bounded linear map. Write $\operatorname{Ker}u\subset E$ for its kernel, $\operatorname{Im}u\subset F$ for its range and $\operatorname{Coker}u=F/\operatorname{Im}u$ for its cokernel (an algebraic quotient). The index of $u$ is the integer

\operatorname{ind}u=\dim\operatorname{Ker}u-\dim\operatorname{Coker}u .

Fredholm operators themselves are not defined here: they are Mathlib's ContinuousLinearMap.IsFredholm ( $u$ is a strict map, $\operatorname{Ker}u$ is finite-dimensional and topologically complemented, and $\operatorname{Im}u$ is closed and of finite codimension). For a Fredholm operator both dimensions are finite.

Formalization Note index u is Module.finrank 𝕜 u.ker - Module.finrank 𝕜 (F ⧸ u.range) in ℤ. Since Module.finrank is $0$ on infinite-dimensional spaces, index u is meaningful only when u.IsFredholm; every theorem about it assumes this. Bourbaki (TS III.43, formula (1)) uses the opposite sign, $\dim\operatorname{Coker}u-\dim\operatorname{Ker}u$ ; the sign here is the usual one in analysis and geometry. The scalar field is any RCLike field.

Definition code

import Mathlib.Analysis.Normed.Operator.Fredholm.Basic
import Mathlib.Analysis.Normed.Operator.Compact.Basic
import Mathlib.Analysis.RCLike.Basic

/-!
# The index of a Fredholm operator

N. Bourbaki, *Théories spectrales*, Chapitre III, § 3, n° 2–3 (pp. TS III.40–III.43).

Fredholm operators are Mathlib's `ContinuousLinearMap.IsFredholm`: `u : E →L[𝕜] F` is
Fredholm if it is a strict map with closed range of finite codimension whose kernel is
finite-dimensional and topologically complemented. For Banach spaces over `ℝ` or `ℂ` this
agrees with Bourbaki's Definition 1 (existence of a quasi-inverse modulo finite rank).

The index is `ind u = dim Ker u - dim Coker u`, with `Coker u = F ⧸ Im u`.
Bourbaki (TS III.43, formula (1)) uses the opposite sign, `dim Coker u - dim Ker u`.
-/

namespace FredholmBanach

noncomputable section

/-- The index `dim Ker u - dim (F ⧸ Im u)` of a continuous linear map. `Module.finrank` is `0`
on infinite-dimensional spaces, so the value is meaningful only for Fredholm `u`. -/
def index {𝕜 E F : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 F] (u : E →L[𝕜] F) : ℤ :=
  (Module.finrank 𝕜 u.ker : ℤ) - (Module.finrank 𝕜 (F ⧸ u.range) : ℤ)

end

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° 2-3, pp. TS III.40-III.43

Read-back

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

Read-back: `FredholmBanach_Setting` (Definitions/Def_FredholmBanach_Setting.lean)

Imports. Mathlib's Fredholm basics (ContinuousLinearMap.IsFredholm), compact operators (IsCompactOperator) and RCLike. Neither IsFredholm nor IsCompactOperator is used in this file; they are imported only for downstream files.

Setting of the definition. $\mathbb{K}$ is $\mathbb{R}$ or $\mathbb{C}$ (RCLike 𝕜). $E, F$ are normed vector spaces over $\mathbb{K}$ (NormedAddCommGroup + NormedSpace). No completeness is assumed here, and no Fredholm hypothesis.

Definition. For a continuous linear map $u : E \to F$ (E →L[𝕜] F),

\operatorname{index}(u) \;=\; \operatorname{finrank}_{\mathbb{K}}(\ker u) \;-\; \operatorname{finrank}_{\mathbb{K}}\bigl(F / \operatorname{range} u\bigr) \in \mathbb{Z}.

u.ker $= \{x \in E : u x = 0\}$ , u.range $= u(E)$ , both as $\mathbb{K}$ -linear subspaces.
$F/\operatorname{range} u$ is the algebraic quotient vector space (the range is not closed off first; no topology enters finrank).
Module.finrank is the dimension when finite and is $0$ when the space is infinite-dimensional. Both naturals are cast to $\mathbb{Z}$ before subtracting.

So the name is FredholmBanach.index, with sign convention $\dim\ker - \dim\operatorname{coker}$ .

Degenerate cases / remarks.

$E = 0$ or $F = 0$ behave as expected: e.g. $u : 0 \to F$ with $F$ finite-dimensional has index $-\dim F$ .
For non-Fredholm $u$ the value is junk: e.g. if $\ker u$ is infinite-dimensional and the cokernel is $0$ , index $=0$ ; an injective map with infinite-dimensional cokernel also gets index $0$ . The docstring acknowledges this.
Sign convention is opposite to Bourbaki (TS III.43 uses $\dim\operatorname{coker} - \dim\ker$ ); the docstring says so explicitly. It agrees with the common analysis convention.
The docstring's claim that IsFredholm agrees with Bourbaki's quasi-inverse definition is commentary, not part of the formal content.

Nothing looks mis-formalized; the only caveat is that the definition is meaningful only for Fredholm $u$ .

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

The index dim⁡Ker⁡u−dim⁡Coker⁡u\dim\operatorname{Ker}u-\dim\operatorname{Coker}udimKeru−dimCokeru of a Fredholm operator

Read-back: FredholmBanach_Setting (Definitions/Def_FredholmBanach_Setting.lean)

The index $\dim\operatorname{Ker}u-\dim\operatorname{Coker}u$ of a Fredholm operator

Read-back: `FredholmBanach_Setting` (Definitions/Def_FredholmBanach_Setting.lean)