That is the question with which Zois, 18 Lectures on K-Theory opens the analytic part of the subject. For a linear map T : V₀ → V₁ between finite-dimensional spaces he states, as Theorem 1 (Linear Algebra), that [Ker T] − [V₀] + [V₁] − [coker T] = 0, and rewrites it as
In infinite dimensions, he notes, “the LHS has no meaning since it gives ∞ − ∞”, but the right side may still make sense for a good operator: “the difference ∞ − ∞ may give, in some cases, a finite result.” That finite result is the index, Ind T := dim Ker T − dim coker T (his Definition 5). He calls the index theorems it led to “arguably the most central result in mathematics during the second half of the 20th century.” CITED
The script builds 127 matrices over ℚ, one of every shape from 1×1 to 6×6 at every rank that shape allows, and computes kernel and cokernel exactly. For T : ℚⁿ → ℚᵐ the difference dim ker − dim coker is n − m every time, whatever the rank. The 27 square ones have index 0 at every rank, invertible or not. COMPUTED
In Lean the same statement is zois_theorem1, and endo_index_zero is the square case: an endomorphism of a finite-dimensional space has index 0. Both rest on Mathlib's LinearMap.index, which uses the same sign convention as Zois, “index = dim ker - dim coker”. KERNEL-CHECKED
The forward shift Sₖ of Chapter 1 has kernel 0 and cokernel k, so its index is −k. Cut it to its top-left N×N block and the block is square, so by §2 its index must be 0. The script computes the block exactly. It has a kernel of dimension k (the last k basis vectors are pushed off the edge) and a cokernel of dimension k (the first k are never reached). The index is 0 for every k = 1, 2, 3 and N = 5, 10, 20. COMPUTED
| k | N | ker | coker | index of the N×N block | index of Sₖ |
|---|---|---|---|---|---|
| 1 | 5, 10, 20 | 1 | 1 | 0 | −1 |
| 2 | 5, 10, 20 | 2 | 2 | 0 | −2 |
| 3 | 5, 10, 20 | 3 | 3 | 0 | −3 |
Zois' first example is this operator, U e₀ = e₁, U e₁ = e₂, …: “Then KerU = {0} and dim(cokerU) = 1. Hence IndU = −1.” He adds that “the index depends much on the spaces H0, H1 and little on the operator between them.” The table shows why. No finite block of the shift has its index, because the index comes from the space being infinite. CITED
Zois gives the basic property Ind(T₀T₁) = Ind T₀ + Ind T₁ and derives it from the six-term exact sequence of the snake lemma. Mathlib's index_comp is proved from the same six-term sequence. On the shifts, bshift_shift_index gives Ind(Bₖ∘Sₖ) = k + (−k), and shift_bshift_index gives Ind(Sₖ∘Bₖ) = 0. KERNEL-CHECKED
Zois reads the index as a measure of “how far an operator is from being invertible since for invertible operators the index vanishes.” The converse is false, and shift_bshift_ne_id gives the counterexample. Sₖ∘Bₖ has index 0, yet for k ≥ 1 it sends e₀ to 0, so it is not the identity. It differs from the identity by a map of rank k, and that is the algebraic shadow of “invertible modulo compacts” in Atkinson's theorem, which Zois states and this chapter does not prove. KERNEL-CHECKED
The letter K is German, and it is Grothendieck's. Zois names Atiyah and Grothendieck as the “fathers” of K-theory and says “The name was given by Grothendieck”. In his account the letter stands for “(die) Klasse”, the class, and the K-theory of a point “is Z and not zero”. That is why K-theory fails the dimension axiom. CITED
The notes are older than they look. Zois says they began at a 1995 summer school at the University of Lancaster, where the analytic lectures were given by John Roe and the algebraic ones by Daniel Quillen. CITED
Mathlib gained LinearMap.index in 2026, in a file by Oliver Nash. It has twelve declarations. index_eq_of_finiteDimensional is Zois' Theorem 1 and index_comp is his basic property. The pinned revision has no Fredholm operators yet (Chapter 3). COMPUTED
Mathlib/Algebra/Module/LinearMap/Index.lean (O. Nash, 2026), at the revision pinned in lake-manifest.json.ShiftIndex.lean); Book XIX on reading Lean.