Composition of Fredholm operators

This file proves that the index of a composite of Fredholm operators between normed spaces is the sum of their indices, over an arbitrary nontrivially normed scalar field. It also records the corresponding statements for powers of a Fredholm endomorphism, which do assume a complete scalar field, since they go through Mathlib's ContinuousLinearMap.IsFredholm.comp.

That a composite is Fredholm is Mathlib's ContinuousLinearMap.IsFredholm.comp. Index additivity reuses Mathlib's LinearMap.index_comp, whose proof is the six-term exact sequence

0 → ker T → ker (S ∘ T) → ker S → coker T → coker (S ∘ T) → coker S → 0.

These results supply the compositional calculus for the Fredholm operators and index theory in Lane F0 of the analytic Heegaard Floer roadmap.

Main declarations

• ContinuousLinearMap.index_comp: the index of a composite is the sum of the indices.
• ContinuousLinearMap.IsFredholm.pow: every power of a Fredholm endomorphism is Fredholm.
• ContinuousLinearMap.index_pow: the index of the nth power is n times the index.

The conventions and the composition theorem follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Appendix A.1.

@[simp]

theorem ContinuousLinearMap.index_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (S : F →L[𝕜] G) (T : E →L[𝕜] F) (hS : S.IsFredholm) (hT : T.IsFredholm) : (S ∘SL T).index = S.index + T.index

The Fredholm index is additive under composition.

theorem ContinuousLinearMap.IsFredholm.pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {X : Type u_5} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {A : X →L[𝕜] X} (hA : A.IsFredholm) (n : ℕ) : (A ^ n).IsFredholm

Over a complete nontrivially normed scalar field, every natural-number power of a Fredholm endomorphism is Fredholm.

@[simp]

theorem ContinuousLinearMap.index_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {X : Type u_5} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (A : X →L[𝕜] X) (hA : A.IsFredholm) (n : ℕ) : (A ^ n).index = ↑n * A.index

The index of the nth power of a Fredholm endomorphism is n times its index.