Alphabeta Math
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.

Atkinson

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:XY be a bounded linear operator (A bounded linear operator between normed spaces). Then T is Fredholm (Fredholm operator cokernel and index) if and only if there is a bounded linear S:YX such that both STIX and TSIY are compact (Compact linear operator).

Facts & Assumptions

[A1]

If T is Fredholm, the splitting lemma provides a bounded S:YX for which STIX has finite-dimensional range of dimension at most dimkerT and TSIY has finite-dimensional range of dimension at most dimcokerT (Fredholm splitting and parametrix); a bounded finite-rank operator is compact (Bounded finite rank operators are compact, Fredholm operator cokernel and index).

[A2]

Under DC, if xCTx+Kx for a compact K and some real C>0, then kerT is finite dimensional and ranT is closed (A compact remainder estimate forces closed range, The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain, Banach space); AC supplies DC (AC supplies the countable and dependent choices used in Banach integration).

[A3]

Transposition is additive with (BA)=AB and I=I (Transposition reverses composition, The transpose of a bounded operator); a compact operator between Banach spaces has compact transpose (Schauder compact adjoint theorem); the kernel of IC with C compact is finite dimensional (Kernel of identity minus compact is finite dimensional).

[A4]

For a bounded T, (ranT)=kerT and ranT=(kerT) (Elementary kernel and range annihilator identities); for closed MY the map (Y/M)M, hhq, is a linear isometric bijection (The dual of a quotient is its annihilator, The quotient vector space (X/M), its cosets, and the quotient map (q:X\to X/M)).

Proof

technique · direct

Given: AC, Banach spaces X,Y over one scalar field, and a bounded linear T:XY.

1.1

If T is Fredholm, then the operator S of [A1] satisfies: STIX and TSIY have finite-dimensional ranges, hence are compact.

A1
1.2

Conversely assume there is a bounded S:YX with F:=STIX and G:=TSIY compact. By boundedness choose a real b0 such that Syby for every yY, and put C:=max(b,1)>0.

assume-hyp
2.1

For every xX one has x=STxFx, hence xSTx+FxbTx+FxCTx+Fx.

step 1.2algebra
2.2

By [A3] the transpose of G=TSIY is G=STIY, so ST=IY+G=IY(G); for gY with Tg=0 one has STg=S(Tg)=0 by linearity of S, hence (IY(G))g=STg=0 and kerTker(IY(G)).

step 1.2A3
3.1

Under the hypothesis of [step 1.2], kerT is finite dimensional and ranT is closed, by [A2] applied to the estimate of [step 2.1] with the compact operator F.

step 2.1A2
3.2

Under the hypothesis of [step 1.2] the operator G:=TSIY is compact, so its transpose G is compact by [A3]; the negative G is compact as well, because the image of a bounded set under G is the negative of its image under G and negating a set preserves the compactness of its closure. So [A3] applies to the compact operator G and makes ker(IY(G)) finite dimensional; by [step 2.2] the subspace kerT is finite dimensional.

step 1.2step 2.2A3
4.1

Under the hypothesis of [step 1.2], the dual of the cokernel is finite dimensional: since ranT is closed by [step 3.1], [A4] gives (cokerT)=(Y/ranT)(ranT)=kerT, which is finite dimensional by [step 3.2].

step 3.1step 3.2A4
5.1

Under the hypothesis of [step 1.2], the cokernel is finite dimensional: if Z is a normed space whose dual has ordered basis h1,,hn, then Ψ(z):=(h1(z),,hn(z)) is linear and injective, because a nonzero z has by [A5] a norm-one functional h, and h=icihi forces Ψ(z)0; the inverse bijection carries an ordered basis of the finite-dimensional image Ψ(Z) to an ordered basis of Z by [A5].

step 4.1A5
6.1

Under the hypothesis of [step 1.2] the operator T is Fredholm, since its kernel is finite dimensional by [step 3.1], its range is closed by [step 3.1] and its cokernel is finite dimensional by [step 5.1]; with [step 1.1] this is the asserted equivalence.

step 1.1step 3.1step 5.1

Depends on

Used by

Dependency tree · two levels

107 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