Continuous families of Fredholm operators

The Fredholm index is locally constant in a continuous family of Fredholm operators. Consequently, it is constant when the parameter space is preconnected, and in particular at the endpoints of a path of Fredholm operators.

This is the continuous-family form of stability under small perturbations. It is a basic input to the spectral-flow and Riemann--Roch-with-boundary developments in Lanes F0 and F1.3 of the analytic Heegaard Floer roadmap: a family can change index only by leaving the Fredholm locus.

The proofs use the operator-norm neighborhood on which ContinuousLinearMap.IsFredholm.eventually_isFredholm_and_index_eq makes the index constant, together with Mathlib's general API for locally constant functions on preconnected spaces.

Main declarations

• Continuous.isLocallyConstant_index: the index of a continuous Fredholm family is locally constant.
• ContinuousOn.index_eq_of_isPreconnected: two parameters in the same preconnected set give operators of equal index.
• Continuous.index_eq_of_preconnectedSpace: a continuous Fredholm family over a preconnected space has constant index.
• Path.index_eq: the endpoints of a continuous Fredholm path have equal index.
• index_eq_of_segment: two operators joined by a Fredholm affine segment have equal index.

The index convention and its perturbation stability follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Appendix A.1.

theorem Continuous.isLocallyConstant_index {K : Type u_1} {E : Type u_2} {F : Type u_3} {X : Type u_4} [NontriviallyNormedField K] [CompleteSpace K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [TopologicalSpace X] {A : X → E →L[K] F} (hA : Continuous A) (hFredholm : ∀ (x : X), (A x).IsFredholm) : IsLocallyConstant fun (x : X) => (A x).index

The Fredholm index of a continuous family of Fredholm operators is locally constant on the parameter space.

theorem ContinuousOn.index_eq_of_isPreconnected {K : Type u_1} {E : Type u_2} {F : Type u_3} {X : Type u_4} [NontriviallyNormedField K] [CompleteSpace K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [TopologicalSpace X] {A : X → E →L[K] F} {s : Set X} (hA : ContinuousOn A s) (hFredholm : ∀ x ∈ s, (A x).IsFredholm) (hs : IsPreconnected s) {x y : X} (hx : x ∈ s) (hy : y ∈ s) : (A x).index = (A y).index

Along a continuous family of Fredholm operators, parameters in the same preconnected set give operators with equal index.

theorem Continuous.index_eq_of_preconnectedSpace {K : Type u_1} {E : Type u_2} {F : Type u_3} {X : Type u_4} [NontriviallyNormedField K] [CompleteSpace K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [TopologicalSpace X] [PreconnectedSpace X] {A : X → E →L[K] F} (hA : Continuous A) (hFredholm : ∀ (x : X), (A x).IsFredholm) (x y : X) : (A x).index = (A y).index

A continuous family of Fredholm operators over a preconnected parameter space has constant index.

theorem Path.index_eq {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [CompleteSpace K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] {T S : E →L[K] F} (A : Path T S) (hFredholm : ∀ (t : ↑unitInterval), (A t).IsFredholm) : T.index = S.index

The endpoints of a continuous path of Fredholm operators have the same index.

theorem TauCeti.index_eq_of_segment {K' : Type u_5} {E' : Type u_6} {F' : Type u_7} [NontriviallyNormedField K'] [IsRCLikeNormedField K'] [CompleteSpace K'] [NormedAddCommGroup E'] [NormedSpace K' E'] [CompleteSpace E'] [NormedAddCommGroup F'] [NormedSpace K' F'] [NormedSpace ℝ (E' →L[K'] F')] (T S : E' →L[K'] F') : (∀ (t : ↑unitInterval), ((1 - ↑t) • T + ↑t • S).IsFredholm) → T.index = S.index

Two operators over an IsRCLikeNormedField have equal index if every operator on the affine segment between them is Fredholm.