⚜ PRINCIPIA ORTHOGONA · Book XXVIII · ch 1 ← contents
Book XXVIII · chapter 1 · rung 28

An Operator With a One-Sided Inverse

The index, computed from actual kernels and cokernels, with no analysis anywhere in the file — and a plain statement of everything that is therefore not proved.
SourceShiftIndex.lean
report shiftindex.axioms.txt
Checked4 theorems, no sorryAx
nothing outside [propext, Classical.choice, Quot.sound]
Toolchainlean 4.33.0-rc1 · Mathlib v4.33.0-rc1
the repository pins v4.32.0; see the audit log
On a finite-dimensional space, an injective map is surjective. That is the fact infinite dimensions take away, and the index is the number that measures exactly how much it takes.

1 · The space and the two maps

Let V be the finitely supported sequences over a field F: the free F-module with basis e₀, e₁, e₂, … The forward shift Sₖ sends eₙ to eₙ₊ₖ. The backward shift Bₖ sends eₙ₊ₖ to eₙ and kills the first k basis vectors.

Sₖ is injective and misses exactly k dimensions. Bₖ is surjective and kills exactly k. And bshift_comp_shift records Bₖ ∘ Sₖ = id — each is a one-sided inverse of the other, on the side that fails.

2 · The index

shift_index : dim ker Sₖ − dim coker Sₖ = 0 − k = −k bshift_index : dim ker Bₖ − dim coker Bₖ = k − 0 = +k

These are computed, not stipulated. ker_shift shows the kernel is ⊥; ker_trunc identifies the range of Sₖ with the kernel of truncation, which gives an explicit isomorphism from the cokernel onto Fin k →₀ F, whose finrank is k. The same argument on the other side gives the kernel of Bₖ.

The payload 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. A reader can check that with a basis and no limits anywhere.

3 · What is not here

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. That −k agrees with the winding number of zᵏ is, in this file, an observation about two numbers and not a proof that they are one theorem.

Closing that gap is chapter 3's job, and it is a real piece of work rather than a formality: it needs the Hardy space, the Toeplitz operator as a compression of multiplication, and the homotopy invariance of the index.

4 · Where this volume sits, and why the file moved twice

WP-82 ordered the rungs by field and found the corpus citing rung 33 thirty-one times and rung 28 twice — K-theory and index theory being the one it leaned on least and grounded least. Rung 28 was named the volume with no core.

The file was committed first to book11/, on a placement map that called Volume XI “the algebraic floor”, then to book33/, on the reading that the floor ladder's top rung was 33. Two documents were numbering the same word differently. The rule now is that the rung number is the volume number: index theory is XXVIII, and book33 is reserved for noncommutative geometry. tools/ladder_check.py is what stops the next such move being silent.

Proved · kernel-checked
bshift_comp_shift book28/ShiftIndex.lean:140
bshift_index book28/ShiftIndex.lean:200
shift_index book28/ShiftIndex.lean:130 Each name above is declared in this repository at the line shown and appears in an axiom report with no sorryAx. A clean axiom report is not a reading of the statement: per R20, a theorem can assume its conclusion and still report clean. Follow the link before citing one as evidence.