TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-22

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Fredholm index is additive

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $X$ , $Y$ and $Z$ be Banach spaces over the same scalar field, and let $T : X \to Y$ and $U : Y \to Z$ be Fredholm operators (Fredholm operator cokernel and index, A bounded linear operator between normed spaces). Then $U T : X \to Z$ is Fredholm and

$ind (U T) = ind U + ind T .$

Facts & Assumptions

[A1]

By Atkinson's theorem a bounded $A$ is Fredholm exactly when there is a bounded $B$ with $A B - I$ and $B A - I$ compact (Atkinson); the compact operators are closed under sums, scalar multiples and composition with bounded operators (Linear combinations of compact operators are compact, Compositions with a compact operator are compact, Fredholm operator cokernel and index).

[A2]

Rank-nullity: for a linear map $f : V \to W$ with $V$ finite dimensional, $\dim V = \dim \ker f + \dim ran f$ (Rank-nullity: $\dim_{F} V = nullity T + rank T$ , Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis); and $\dim \ker f = \dim im g$ for an exact predecessor $g$ at that spot, so that a finite exact sequence $0 \to V_{1} \to V_{2} \to V_{3} \to V_{4} \to V_{5} \to V_{6} \to 0$ of finite-dimensional spaces satisfies $\sum_{i = 1}^{6} (- 1)^{i + 1} \dim V_{i} = 0$ (Linear map between vector spaces over the same field, Linear subspace of a vector space).

[A3]

For a bounded $T$ the cokernel is the quotient $coker T = Y / ran T$ with cosets written $y + ran T$ (The quotient vector space (X/M), its cosets, and the quotient map (q:X\to X/M), Fredholm operator cokernel and index); $A C$ supplies DC (AC supplies the countable and dependent choices used in Banach integration, The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain, Banach space).

Proof

technique · direct

Given: $A C$ , Banach spaces $X, Y, Z$ over one scalar field, Fredholm operators $T : X \to Y$ and $U : Y \to Z$ , and parametrices $S$ for $T$ and $R$ for $U$ as in [A1].

1.1

$U T$ is Fredholm: $S R$ is a parametrix for $U T$ , since $(S R) (U T) - I_{X} = S (R U - I_{Y}) T + (S T - I_{X})$ and $(U T) (S R) - I_{Z} = U (T S - I_{Y}) R + (U R - I_{Z})$ are compact by [A1], so Atkinson gives Fredholmness of $U T$ .

1.2

The maps $α : V_{1} \to V_{2}$ , $α (x) = x$ ; $β : V_{2} \to V_{3}$ , $β (x) = T x$ ; $γ : V_{3} \to V_{4}$ , $γ (y) = y + ran T$ ; $δ : V_{4} \to V_{5}$ , $δ (y + ran T) = U y + ran (U T)$ ; and $ε : V_{5} \to V_{6}$ , $ε (z + ran (U T)) = z + ran U$ are well-defined linear maps: $δ$ is well-defined because $y \in ran T$ gives $U y \in ran (U T)$ , and the other four are restrictions, inclusions or quotient maps of linear maps.

2.1

All six spaces $V_{1} : = \ker T$ , $V_{2} : = \ker (U T)$ , $V_{3} : = \ker U$ , $V_{4} : = coker T$ , $V_{5} : = coker (U T)$ , $V_{6} : = coker U$ are finite dimensional.

step 1.1A1

2.2

The sequence is exact at $V_{1}$ , $V_{2}$ and $V_{3}$ : $α$ is injective; $\ker β = {x \in V_{2} : T x = 0} = V_{1} = im α$ ; and $\ker γ = {y \in V_{3} : y \in ran T} = {T x : x \in V_{2}} = im β$ .

step 1.2

2.3

The sequence is exact at $V_{4}$ , $V_{5}$ and $V_{6}$ : $\ker δ = {y + ran T : U y \in ran (U T)} = {y + ran T : y - T x \in \ker U for some x} = im γ$ ; $im δ = {U y + ran (U T) : y \in Y} = {z + ran (U T) : z \in ran U} = \ker ε$ ; and $ε$ is surjective as the quotient map $Z / ran (U T) \to Z / ran U$ .

step 1.2

3.1

Rank-nullity telescopes the dimensions: with $f_{0} : 0 \to V_{1}$ , $f_{i} : V_{i} \to V_{i + 1}$ for $1 \leq i \leq 5$ and $f_{6} : V_{6} \to 0$ the maps of [step 1.2], exactness gives $\ker f_{i} = im f_{i - 1}$ , so $\dim V_{i} = \dim im f_{i - 1} + \dim im f_{i}$ , and summing with signs $(+, -, +, -, +, -)$ cancels to $\dim V_{1} - \dim V_{2} + \dim V_{3} - \dim V_{4} + \dim V_{5} - \dim V_{6} = 0$ , because $im f_{0} = 0$ and $im f_{6} = 0$ .

step 2.1step 2.2step 2.3A2

4.1

The index identity follows: $ind (U T) = \dim V_{2} - \dim V_{5} = (\dim V_{1} - \dim V_{4}) + (\dim V_{3} - \dim V_{6}) = ind T + ind U$ , by the telescoping identity of [step 3.1] and the definition of the index.

step 3.1A2A3∎

Depends on

Used by

Fredholm map between Banach manifolds Definition
The index of a Fredholm map is locally constant Proposition
Fredholm index is locally constant Theorem

Dependency tree · two levels

69 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §6.5 p.186, Lemma 6.25 (standard reference, not scraped)
Theo Bühler and Dietmar Salamon, Functional Analysis — §4.4 pp.195–196, Theorem 4.40 (standard reference, not scraped)