Compact perturbations of Fredholm operators

A compact perturbation of a Fredholm operator between Banach spaces is Fredholm, with the same index. This is the last of the three classical stability statements for the Fredholm index -- after finite-rank perturbations (TauCeti.Analysis.Fredholm.FiniteRank) and small perturbations (TauCeti.Analysis.Fredholm.SmallPerturbation) -- and completes the linear half of Lane F0 of the analytic Heegaard Floer roadmap.

The starting point is the Riesz--Schauder theory of TauCeti.Analysis.Normed.Operator.Compact.RieszTheory: for a compact operator K the kernel of 1 - K is finite dimensional and its cokernel is finite dimensional, so 1 - K is Fredholm.

For a general Fredholm T and compact C, take a continuous quasi-inverse S of T, so that S ∘ T and T ∘ S differ from the identity by operators of finite rank. Then S ∘ (T + C) = (1 + S ∘ C) + (S ∘ T - 1) is a finite-rank perturbation of a compact perturbation of the identity, hence Fredholm, and likewise for (T + C) ∘ S. The kernel of T + C sits inside the kernel of S ∘ (T + C) and the range of T + C contains the range of (T + C) ∘ S, so both defect spaces of T + C are finite dimensional.

The index statement is then a connectedness argument rather than a new computation: the family c ↦ T + c • C is a continuous family of Fredholm operators over the preconnected parameter space 𝕜, so the local constancy of the index proved in TauCeti.Analysis.Fredholm.ContinuousFamily forces the values at c = 0 and c = 1 to agree.

Main declarations

• TauCeti.isFredholm_one_sub and TauCeti.isFredholm_one_add: 1 - K and 1 + K are Fredholm for K compact.
• ContinuousLinearMap.IsFredholm.add_of_isCompactOperator: a compact perturbation of a Fredholm operator is Fredholm.
• ContinuousLinearMap.index_add_of_isCompactOperator: a compact perturbation leaves the index unchanged.
• ContinuousLinearMap.index_one_sub_eq_zero and ContinuousLinearMap.index_one_add_eq_zero: 1 - K and 1 + K have index 0 for K compact.

The conventions follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Appendix A.1; the compact-perturbation statement is Atkinson's theorem together with the Riesz--Schauder theory, see Conway, A Course in Functional Analysis, Chapter XI.

theorem TauCeti.isFredholm_one_sub {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {K : E →L[𝕜] E} (hK : IsCompactOperator ⇑K) : (1 - K).IsFredholm

Riesz--Schauder: a compact perturbation of the identity is a Fredholm operator.

theorem TauCeti.isFredholm_one_add {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {K : E →L[𝕜] E} (hK : IsCompactOperator ⇑K) : (1 + K).IsFredholm

Riesz--Schauder, in the form in which compact perturbations of the identity arise below.

theorem ContinuousLinearMap.IsFredholm.add_of_isCompactOperator {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {T C : E →L[𝕜] F} (hT : T.IsFredholm) (hC : IsCompactOperator ⇑C) : (T + C).IsFredholm

A compact perturbation of a Fredholm operator between Banach spaces is Fredholm.

The proof is Atkinson's argument: a quasi-inverse S of T turns T + C into a compact perturbation of the identity on both sides, up to finite rank, and the two defect spaces of T + C are then squeezed between those of S ∘ (T + C) and (T + C) ∘ S.

theorem ContinuousLinearMap.index_add_of_isCompactOperator {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {T C : E →L[𝕜] F} (hT : T.IsFredholm) (hC : IsCompactOperator ⇑C) : (T + C).index = T.index

A compact perturbation leaves the Fredholm index unchanged.

The scalar family c ↦ T + c • C is a continuous family of Fredholm operators over the preconnected parameter space 𝕜, so its index is constant; comparing c = 0 with c = 1 gives the claim.

@[simp]

theorem ContinuousLinearMap.index_one_sub_eq_zero {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {K : E →L[𝕜] E} (hK : IsCompactOperator ⇑K) : (1 - K).index = 0

A compact perturbation of the identity has index 0.

@[simp]

theorem ContinuousLinearMap.index_one_add_eq_zero {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {K : E →L[𝕜] E} (hK : IsCompactOperator ⇑K) : (1 + K).index = 0

A compact perturbation of the identity has index 0, in additive form.