Prove2Me

The Fredholm index is additive under composition

Proved
FredholmBanach.index_comp

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

banach-spacescompact-operatorsfredholm-operatorsfunctional-analysisoperator-theory

Let K\mathbb{K} be R\mathbb{R} or C\mathbb{C} and let EE, FF, GG be Banach spaces over K\mathbb{K}. If u:E→Fu:E\to F and v:F→Gv:F\to G are Fredholm operators, then

ind⁡(v∘u)=ind⁡v+ind⁡u,\operatorname{ind}(v\circ u)=\operatorname{ind}v+\operatorname{ind}u,

where ind⁡u=dim⁡Ker⁡u−dim⁡(F/Im⁡u)\operatorname{ind}u=\dim\operatorname{Ker}u-\dim(F/\operatorname{Im}u) and likewise for vv and v∘uv\circ u.

Preamble
import Definitions.Def_FredholmBanach_Setting
Formal statement
namespace FredholmBanach

open Topology

/-- Bourbaki, *Théories spectrales*, III, § 3, n° 3, formula (2) (TS III.43): the index is
additive under composition, `ind (v ∘ u) = ind v + ind u`. -/
theorem index_comp {𝕜 E F G : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F]
    [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CompleteSpace G]
    {u : E →L[𝕜] F} {v : F →L[𝕜] G} (hu : u.IsFredholm) (hv : v.IsFredholm) :
    index (v.comp u) = index v + index u := 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° 3, formula (2), p. TS III.43
Read-back

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

Read-back: FredholmBanach.index_comp

Setting. K∈{R,C}\mathbb{K} \in \{\mathbb{R}, \mathbb{C}\} (RCLike 𝕜). E,F,GE, F, G Banach spaces over K\mathbb{K} (normed and complete). u:E→Fu : E \to F, v:F→Gv : F \to G continuous linear maps.

Definitions used.

  • index w (from Def_FredholmBanach_Setting) for w:X→Yw : X \to Y: index⁡(w)=finrank⁡(ker⁡w)−finrank⁡(Y/w(X))∈Z\operatorname{index}(w) = \operatorname{finrank}(\ker w) - \operatorname{finrank}(Y / w(X)) \in \mathbb{Z}, with Y/w(X)Y/w(X) the algebraic quotient and finrank =0=0 on infinite-dimensional spaces. Sign: dim⁡ker⁡−dim⁡coker⁡\dim\ker - \dim\operatorname{coker} (opposite to Bourbaki's formula (1)).
  • IsFredholm (Mathlib): strict map, closed range, finite-dimensional kernel, finite-dimensional algebraic cokernel, topologically complemented kernel.

Hypotheses. uu Fredholm and vv Fredholm.

Conclusion.

index⁡(v∘u)=index⁡(v)+index⁡(u).\operatorname{index}(v \circ u) = \operatorname{index}(v) + \operatorname{index}(u).

Since u,vu, v are Fredholm, both index values on the right are genuine dim⁡ker⁡−dim⁡coker⁡\dim\ker - \dim\operatorname{coker}. The left side is a genuine index only if v∘uv \circ u is Fredholm; this is not a hypothesis, but follows from the companion statement isFredholm_comp. Even without that, the equation is a statement about the finrank-based integers and is unambiguous as written.

Degenerate cases.

  • u=idu = \mathrm{id} or v=idv = \mathrm{id}: trivially consistent.
  • Finite-dimensional spaces: index =dim⁡X−dim⁡Y= \dim X - \dim Y by rank–nullity, and the formula reduces to (dim⁡E−dim⁡G)=(dim⁡F−dim⁡G)+(dim⁡E−dim⁡F)(\dim E - \dim G) = (\dim F - \dim G) + (\dim E - \dim F).
  • Additivity is symmetric in sign, so the sign-convention difference with Bourbaki does not affect this statement.

Remarks. Hypotheses are the natural ones; nothing vacuous or mis-formalized observed.

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