Restricting an operator to closed subspaces of finite codimension preserves the Fredholm property and shifts the index by the codimensions

Proved

FredholmBanach.isFredholm_restrict_iff

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}$ . Let $u:E\to F$ be a bounded linear map, and let $E_1\subset E$ and $F_1\subset F$ be closed linear subspaces with $E/E_1$ and $F/F_1$ finite-dimensional and $u(E_1)\subset F_1$ . Let $u_1:E_1\to F_1$ be the restriction of $u$ . Then $u$ is Fredholm if and only if $u_1$ is Fredholm, and in that case

\operatorname{ind}u-\operatorname{ind}u_1=\dim(E/E_1)-\dim(F/F_1),

where $\operatorname{ind}u=\dim\operatorname{Ker}u-\dim(F/\operatorname{Im}u)$ and likewise for $u_1$ .

Preamble

import Definitions.Def_FredholmBanach_Setting

Formal statement

namespace FredholmBanach

open Topology

/-- Bourbaki, *Théories spectrales*, III, § 3, n° 3, Proposition 3 and formula (5) (TS III.44):
let `E₁ ⊆ E`, `F₁ ⊆ F` be closed subspaces of finite codimension with `u (E₁) ⊆ F₁`, and let
`u₁ : E₁ → F₁` be the restriction. Then `u` is Fredholm if and only if `u₁` is, and then
`ind u - ind u₁ = codim E₁ - codim F₁` (with the sign convention `ind = dim Ker - dim Coker`). -/
theorem isFredholm_restrict_iff {𝕜 E F : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F]
    (u : E →L[𝕜] F) (E₁ : Submodule 𝕜 E) (F₁ : Submodule 𝕜 F)
    (hE₁ : IsClosed (E₁ : Set E)) (hF₁ : IsClosed (F₁ : Set F))
    (hE₁f : FiniteDimensional 𝕜 (E ⧸ E₁)) (hF₁f : FiniteDimensional 𝕜 (F ⧸ F₁))
    (h : Set.MapsTo u E₁ F₁) :
    (u.IsFredholm ↔ (u.restrict h).IsFredholm) ∧
      (u.IsFredholm → index u - index (u.restrict h) =
        (Module.finrank 𝕜 (E ⧸ E₁) : ℤ) - (Module.finrank 𝕜 (F ⧸ F₁) : ℤ)) := 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, Proposition 3 and formula (5), p. TS III.44 (with the opposite sign of the index)

Read-back

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

Read-back: `FredholmBanach.isFredholm_restrict_iff`

Setting. $\mathbb{K} \in \{\mathbb{R}, \mathbb{C}\}$ (RCLike 𝕜). $E, F$ Banach spaces over $\mathbb{K}$ (normed, complete). $u : E \to F$ continuous linear. $E_1 \subseteq E$ and $F_1 \subseteq F$ are $\mathbb{K}$ -linear subspaces (Submodule).

Hypotheses.

hE₁, hF₁: $E_1$ is closed in $E$ and $F_1$ is closed in $F$ .
hE₁f, hF₁f: the algebraic quotients $E/E_1$ and $F/F_1$ are finite-dimensional (finite codimension).
h : Set.MapsTo u E₁ F₁: $u(E_1) \subseteq F_1$ .

Definitions used.

u.restrict h : E₁ →L[𝕜] F₁ is $u_1(x) = u(x)$ for $x \in E_1$ , viewed as a continuous linear map between the subspaces with their induced norms (the subspaces are again Banach, being closed).
IsFredholm (Mathlib): strict map (corestriction onto range is a topological quotient map), closed range, finite-dimensional kernel, finite-dimensional algebraic cokernel, topologically complemented kernel.
index w $= \operatorname{finrank}\ker w - \operatorname{finrank}(\text{target}/\operatorname{range} w)$ in $\mathbb{Z}$ , finrank $=0$ if infinite-dimensional.

Conclusion (a conjunction).

$u$ is Fredholm $\iff$ $u_1$ is Fredholm.
If $u$ is Fredholm, then

\operatorname{index}(u) - \operatorname{index}(u_1) = \operatorname{codim}_E E_1 - \operatorname{codim}_F F_1,

with $\operatorname{codim} =$ finrank of the quotient (finite by hypothesis, so a true dimension).

Sign check. With $E_1 = E$ and $F_1 = F$ the identity reads $0 = 0$ . With $u = \mathrm{id}_E$ , $F_1 = F = E$ , $E_1$ a closed hyperplane: $u_1$ is the inclusion with index $-1$ , so left side $0 - (-1) = 1 = 1 - 0$ . Consistent with the $\dim\ker - \dim\operatorname{coker}$ convention (Bourbaki's formula (5) would carry the opposite sign under his convention; the docstring flags this).

Degenerate cases. If $E, F$ are finite-dimensional, every map is Fredholm and the formula reduces to rank–nullity. Part 2 is stated only under Fredholmness of $u$ , which by part 1 is equivalent to that of $u_1$ , so it does not lose generality.

Remarks. Closedness of $E_1, F_1$ is assumed (needed for the restricted spaces to be Banach). No mis-formalization 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

Restricting an operator to closed subspaces of finite codimension preserves the Fredholm property and shifts the index by the codimensions

Read-back: FredholmBanach.isFredholm_restrict_iff

Read-back: `FredholmBanach.isFredholm_restrict_iff`