2 The Fredholm index pairing
This chapter develops the index attached to an even spectral triple. The graded-kernel index (Section 2.2) — the special case of the index pairing at the unit projection \(p = 1\) — is formalized, building on a minimal notion of Fredholm linear map (Section 2.1). The general index pairing against an arbitrary \(K_0\)-class \([p]\) (Section 2.3) is not yet formalized; it corresponds to Phase 2 of the project plan.
2.1 Fredholm operators
This section records a minimal, self-contained notion of Fredholm linear map, scoped to exactly what the index pairing needs. Mathlib has ongoing, as yet unmerged, work towards a general theory of Fredholm operators on topological vector spaces; the definitions here are deliberately narrower — stated for plain linear maps rather than continuous linear maps, so that they apply uniformly to bounded operators and to the restriction of an unbounded operator to its domain, as needed for the chiral Dirac operator \(D^{+}\) — and are expected to be replaced by an import once the upstream theory lands.
A linear map \(f \colon E \to F\) is Fredholm if \(\ker f\) is finite-dimensional, the range of \(f\) is closed, and the range of \(f\) has finite codimension (the cokernel \(F / \operatorname {ran} f\) is finite-dimensional).
The Fredholm index of a linear map \(f \colon E \to F\) is the integer
A bijective linear map with closed range is Fredholm, of index \(0\).
2.1.1 Compact perturbations of the identity
This subsection proves the structural part of the Hilbert-space case of the classical Riesz–Schauder theorem: \(1 - K\) is Fredholm whenever \(K\) is compact (finite kernel, closed range, finite-dimensional cokernel). The further classical fact that the index is \(0\) is not proved here. None of this is yet in Mathlib (only the weaker spectral dichotomy for compact operators is), so it is built here from scratch, as the analytic ingredient needed to eventually show the chiral Dirac operator \(D^{+}\) is Fredholm.
A compact operator \(K\) on a Hilbert space is approximable, in operator norm, by finite-rank operators: for every \(\varepsilon {\gt} 0\) there is a finite-rank \(F\) with \(\| K - F\| \leq \varepsilon \). The approximant is built by composing \(K\) with the orthogonal projection onto the span of a finite \(\varepsilon \)-net of the (relatively compact) image of the closed unit ball.
If a continuous linear map on an inner product space has finite-dimensional range, so does its adjoint.
If \(K\) is a compact operator on a Hilbert space, then its adjoint \(K^{\dagger }\) is also compact: the adjoints of finite-rank approximants of \(K\) (Theorem 16) are themselves finite-rank (Lemma 17), hence compact, and converge to \(K^{\dagger }\) in norm since the adjoint operation is norm-preserving.
The structural part of the classical Riesz–Schauder theorem: if \(K\) is compact on a Hilbert space, then \(1 - K\) is Fredholm. The kernel is finite-dimensional (it is the eigenspace of \(K\) at the eigenvalue \(1\)); the range is closed, via a bounded-below estimate on the orthogonal complement of the kernel established by a contradiction argument using compactness of \(K\); and the cokernel is finite-dimensional, via the adjoint identity \((1-K)^{\dagger } = 1 - K^{\dagger }\) (Theorem 18) together with \((\operatorname {ran}(1-K))^{\perp } = \ker ((1-K)^{\dagger })\). (The further classical fact that the index is \(0\) is not proved here.)
2.2 The graded-kernel index
For a (partially defined) linear operator \(D \colon \operatorname {dom}(D) \to \mathcal{H}\), the kernel \(\ker D \subseteq \mathcal{H}\) is the subspace of vectors \(\xi \in \operatorname {dom}(D)\) with \(D\xi = 0\).
If \((A, \mathcal{H}, \pi , D, \gamma )\) is an even spectral triple and \(\xi \in \ker D\), then \(\gamma \xi \in \ker D\). Consequently \(\ker D\) splits as \(\ker D = (\ker D)^{+} \oplus (\ker D)^{-}\) into the \((\pm 1)\)-eigenspaces of \(\gamma \) restricted to \(\ker D\).
The (super)index of an even Dirac datum \((D, \gamma )\) is the integer
This is the Fredholm index of the chiral operator \(D^{+}\) from Definition 24 in the special case \(p = 1\). The corresponding invariant of an even spectral triple is .
If \(D\) is self-adjoint with compact resolvent at \(i\), then \(\ker D\) is finite-dimensional. Consequently \(\operatorname {index}(D, \gamma )\) (Definition 22) is a difference of genuine finite dimensions: for \(\xi \in \ker D\), the resolvent \(R(i, D)\) satisfies \(R(i,D)(i\xi ) = \xi \), so \(\ker D\) embeds into the \(i^{-1}\)-eigenspace of the compact operator \(R(i, D)\), which is finite-dimensional by Riesz theory.
2.3 The general index pairing
This section is not yet formalized; it corresponds to Phase 2 of the project plan. It generalizes Section 2.2 from the unit projection \(p = 1\) to an arbitrary self-adjoint idempotent representing a class in \(K_0(A)\).
Let \((A, \mathcal{H}, \pi , D, \gamma )\) be an even spectral triple and let \(p \in M_n(A)\) be a self-adjoint idempotent (a projection representing a class in \(K_0(A)\)). The index pairing of \(p\) with \((A, \mathcal{H}, \pi , D, \gamma )\) is the Fredholm index
where \(D^{+}\) denotes the restriction of \(D\) to the \((+1)\)-eigenspace of \(\gamma \).