Book XXVIII · rung 28 · opened 2026-09-19 · the core WP-82 left open
Index Theory
WP-82 measured the corpus citing rung 33 thirty-one times and rung 28 twice, and named rung 28 the volume with no core. This is the core.
A reader who skips to the end of the ladder lands here, so the payload is stated before anything else: an operator with a one-sided inverse on an infinite-dimensional space has an index, the index is not zero, and which side the inverse is on decides the sign.
1 · The two numbers
Let V be the finitely supported sequences over a field F — the free module with basis e₀, e₁, e₂, … The forward shift Sₖ sends eₙ to eₙ₊ₖ; the backward shift Bₖ sends eₙ₊ₖ to eₙ and kills e₀ … eₖ₋₁.
ind(Sₖ) = dim ker − dim coker = 0 − k = −k
ind(Bₖ) = dim ker − dim coker = k − 0 = +k
Actual kernels and cokernels: LinearMap.ker, the quotient by LinearMap.range, and Module.finrank — not a count kept by hand. bshift_comp_shift records that Bₖ ∘ Sₖ = id, which is why one is injective and not surjective and the other surjective and not injective.
What is not here, and must not be read in
This is the algebraic index. There is no topology in the file: no norm, no completion, no boundedness, no compactness, no Fredholm theory in the analytic sense, and no Toeplitz operator on a Hardy space. F. Noether's 1921 theorem — that the index of a Toeplitz operator is minus the winding number of its symbol — is not formalised, and the agreement between −k and the winding number of zᵏ is here an observation about two numbers, not a proof that they are one theorem.
2 · Why the file moved twice
It was committed first to book11/, on the strength of a placement map that gave Volume XI the role “the algebraic floor”; then to book33/, on the reading that the floor ladder's top rung was 33. Neither was right. Two documents were numbering the same word differently, and a file cannot be addressed correctly until that is settled. The rule now is that the rung number is the volume number, so index theory is XXVIII and book33 is reserved for noncommutative geometry — a different subject, with its own source on the shelf.
Where this sits on the ladder
The rung number is the volume number.
docs/floor-ladder.tsv holds the map and
tools/ladder_check.py refuses a rung whose volume disagrees in any of the three places it is written — the ladder, the directory, and the Lean file's own header.
11 what a numeral names ·
12 counting ·
14 the repairs ·
16 order, powers, roots ·
17 statistics ·
18 the chain rule ·
19 AXLE and the manual ·
20 polynomials and the circle ·
21 planar linear systems ·
28 index theory ·
33 noncommutative geometry
3 · Chapters
| ch | title | state |
|---|
| 1 | An Operator With a One-Sided Inverse — the shift, its kernel, its cokernel, and the sign | live |
| 2 | Why odd dimensions give index zero, and how Toeplitz escapes it | planned |
| 3 | F. Noether 1921 — the winding number, and what it would take to formalise the bridge | planned |