LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 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 splitting and parametrix

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $X$ and $Y$ be Banach spaces over the same scalar field and let $T : X \to Y$ be a Fredholm operator (Fredholm operator cokernel and index, A bounded linear operator between normed spaces). Then there are a closed linear subspace $X_{1} \leq X$ and a finite-dimensional closed linear subspace $Y_{0} \leq Y$ with

$X = \ker T \oplus X_{1}, Y = ran T \oplus Y_{0},$

the coordinate projections of both decompositions being bounded (A complemented closed subspace of a normed space), with $\dim Y_{0} = \dim coker T$ (Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis), and such that with $U : = (T ∣_{X_{1}})^{- 1} : ran T \to X_{1}$ , which is bounded, the operator

$S : Y ⟶ X, S (y) : = U (y_{1}) for y = y_{1} + y_{0}, y_{1} \in ran T, y_{0} \in Y_{0},$

is bounded and satisfies: $S T - I_{X}$ has finite-dimensional range of dimension at most $\dim \ker T$ , and $T S - I_{Y}$ has finite-dimensional range of dimension at most $\dim Y_{0}$ .

Facts & Assumptions

[A1]

A finite-dimensional linear subspace of a normed space is complemented, and a closed finite-codimensional linear subspace is complemented; a complemented subspace has a closed complement with bounded coordinate projections (Finite-dimensional subspaces are complemented, Closed finite-codimensional subspaces are complemented, A complemented closed subspace of a normed space, Linear subspace of a vector space).

[A2]

A closed linear subspace of a Banach space is a Banach space (A closed subspace of a Banach space is Banach, Banach space), and by the bounded inverse theorem, under DC, a bounded bijection between Banach spaces has a bounded inverse (Bounded inverse theorem); $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).

[A3]

If $q : Z \to Z / W$ is the quotient map and a linear bijection $Z_{0} \to Z / W$ is given, then choosing preimages of a finite basis is a finite selection (Every natural-number-indexed list of nonempty sets has a choice function on its family of values, Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, The quotient vector space (X/M), its cosets, and the quotient map (q:X\to X/M), Linear map between vector spaces over the same field): a linearly independent spanning list pulls back to a linearly independent spanning list, because a linear bijection preserves the vanishing of finite linear combinations in both directions.

Proof

technique · direct

Given: $A C$ , Banach spaces $X, Y$ over one scalar field, a Fredholm operator $T : X \to Y$ with $N : = \ker T$ finite dimensional and $ran T$ closed with finite-dimensional cokernel.

1.1

There is a closed subspace $X_{1} \leq X$ with $X = N \oplus X_{1}$ and bounded projections.

1.2

There is a closed subspace $Y_{0} \leq Y$ with $Y = ran T \oplus Y_{0}$ and bounded projections; the quotient map $q : Y \to coker T = Y / ran T$ restricts to a linear bijection $q ∣_{Y_{0}} : Y_{0} \to coker T$ , which is injective because $Y_{0} \cap ran T = {0}$ and surjective because $y = y_{1} + y_{0}$ gives $q (y) = q (y_{0})$ .

2.1

The restriction $T_{1} : = T ∣_{X_{1}} : X_{1} \to ran T$ is a bounded linear bijection: it is injective because $X_{1} \cap \ker T = {0}$ , and surjective because $T (X) = T (N + X_{1}) = T (X_{1})$ .

step 1.1

2.2

The subspace $Y_{0}$ is finite dimensional with $\dim Y_{0} = \dim coker T$ : pulling back an ordered basis of the finite-dimensional quotient $coker T$ along the bijection $q ∣_{Y_{0}}$ of [step 1.2] gives an ordered basis of $Y_{0}$ , by the finite selection and independence argument of [A3].

step 1.2A3

3.1

The spaces $X_{1}$ and $ran T$ are Banach, so $U : = T_{1}^{- 1}$ is bounded by [A2].

step 2.1A2

4.1

The operator $S : Y \to X$ that equals $U$ on $ran T$ and $0$ on $Y_{0}$ is $U \circ P$ for the bounded projection $P : Y \to ran T$ of [step 1.2], hence bounded as a composite of bounded operators.

step 1.2step 3.1

4.2

For $x = n + x_{1}$ with $n \in N$ , $x_{1} \in X_{1}$ one has $S T x = S (T x_{1}) = U (T_{1} x_{1}) = x_{1}$ , so $S T$ is the bounded projection $P_{X_{1}}$ onto $X_{1}$ along $N$ and $S T - I_{X} = - P_{N}$ has range $N$ , of dimension $\dim \ker T$ .

step 1.1step 3.1

4.3

For $y = y_{1} + y_{0}$ one has $T S y = T (U y_{1}) = y_{1}$ , so $T S$ is the bounded projection $P$ onto $ran T$ along $Y_{0}$ and $T S - I_{Y}$ has range $Y_{0}$ , of dimension $\dim Y_{0}$ .

step 1.2step 3.1step 2.2

5.1

The decompositions, the boundedness of $U$ and $S$ and the two finite-rank defects are exactly the assertions, with $\dim Y_{0} = \dim coker T$ from [step 2.2].

step 4.1step 4.2step 2.2step 4.3∎

Depends on

Used by

Local finite-dimensional reduction for a Fredholm map Lemma
Atkinson Theorem
Fredholm index is locally constant Theorem

Dependency tree · two levels

59 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, equations (6.65)–(6.67) (standard reference, not scraped)
Theo Bühler and Dietmar Salamon, Functional Analysis — §4.3, splitting of a Fredholm operator (standard reference, not scraped)