Book XXVIII · Index Theory — Principia Orthogona

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	Infinity Minus Infinity — why finite dimensions give index zero, and how the shift escapes it (Zois Lecture 1; Mathlib `LinearMap.index`; 7 theorems)	live
3	The Winding Number — Ind T_f = −wn(f) read through Zois, observed on eleven symbols, and what Mathlib lacks to formalise the bridge (Noether's own 1921 paper, Math. Ann. 82, now held)	live
4	Riemann–Roch and the Letter K — why K-theory exists; the even-dimensional index, on the sphere and on curves of genus 0–4 (Blackadar, Rosenberg, Dugger; RiemannRoch.lean)	live
5	The Space of Fredholm Operators — kernels jump, the index does not; Atiyah’s appendix and why the word “index” (FredholmSpace.lean)	live
6	The Circle Comes Back — Bott periodicity, and why its generator is a winding number (CliffordSmall.lean)	live
7	One Number, Two Ways — the Atiyah–Singer index theorem, stated from Blackadar; its odd and even cases are ch 3 and ch 4; tested on line bundles over projective space (IndexTwoWays.lean)	live