Fredholm operators from finite-codimension restrictions

Let T : E →L[𝕜] F carry a closed finite-codimensional subspace E₁ into a closed finite-codimensional subspace F₁. Mathlib's ContinuousLinearMap.IsFredholm.of_restrict shows that T is Fredholm when the induced operator E₁ →L[𝕜] F₁ is. This file records the accompanying index formula: the index of T is the index of the restriction plus codim E₁ - codim F₁. It is a basic reduction for the Fredholm-operator substrate in Lane F0 of the analytic Heegaard Floer roadmap, in particular when an operator is first controlled after discarding finitely many modes.

Main declarations

• ContinuousLinearMap.index_restrict: the index formula for the restriction of a continuous linear map to closed finite-codimensional subspaces.

The finite-codimension reduction and index convention follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Appendix A.1. The proof factors T through the inclusions of the subspaces and applies Mathlib's composition formula for the index.

@[simp]

theorem ContinuousLinearMap.index_restrict {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [CompleteSpace K] [NormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] {T : E →L[K] F} {E₁ : Submodule K E} {F₁ : Submodule K F} (hE₁ : IsClosed ↑E₁) [E₁.CoFG] (hF₁ : IsClosed ↑F₁) [F₁.CoFG] (hT : Set.MapsTo ⇑T ↑E₁ ↑F₁) (hT₁ : (T.restrict hT).IsFredholm) : (T.restrict hT).index = T.index - ↑(Module.finrank K (E ⧸ E₁)) + ↑(Module.finrank K (F ⧸ F₁))

The index of the restriction of a continuous linear map from E to F to closed finite-codimensional subspaces E₁ and F₁ is the index of the full operator minus codim E₁ plus codim F₁.