Fredholm operators

This file connects Mathlib's analytic notion of a Fredholm operator to the nonlinear-analysis substrate of the analytic Heegaard Floer roadmap (Lane F0, "Fredholm operators and index theory"). All Fredholm hypotheses use ContinuousLinearMap.IsFredholm directly. That predicate asks for a strict map with closed range, finite-dimensional kernel and cokernel, and a topologically complemented kernel. Between Banach spaces over an IsRCLikeNormedField the strictness, closed-range and complemented-kernel conditions are automatic, so the predicate is equivalent there to finite dimensionality of the kernel and cokernel alone; that equivalence is proved and exposed as TauCeti.isFredholm_iff_finite_ker_coker in TauCeti.Analysis.Fredholm.ClosedRange. Outside that setting ContinuousLinearMap.IsFredholm is genuinely stronger, and it is the notion intended throughout.

Main declarations

• TauCeti.isFredholm_of_finiteDimensional: every operator between finite-dimensional spaces is Fredholm.
• ContinuousLinearMap.IsFredholm.neg, ContinuousLinearMap.IsFredholm.smul: Fredholmness is preserved by negation and by nonzero scalar multiples.
• ContinuousLinearMap.IsFredholm.comp_equiv and ContinuousLinearMap.IsFredholm.equiv_comp: composing with a continuous linear equivalence on either side preserves Fredholmness. Mathlib provides stronger ↔ versions over complete scalar fields; these implications hold over any NontriviallyNormedField.

The Fredholm index and its elementary API live in TauCeti.Topology.Algebra.Module.ContinuousLinearMap.Index.

theorem TauCeti.isFredholm_of_finiteDimensional {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (T : E →L[𝕜] F) : T.IsFredholm

Every continuous linear map between finite-dimensional spaces is Fredholm.

theorem ContinuousLinearMap.IsFredholm.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (hT : T.IsFredholm) {c : 𝕜} (hc : c ≠ 0) : (c • T).IsFredholm

A nonzero scalar multiple of a Fredholm operator is Fredholm.

theorem ContinuousLinearMap.IsFredholm.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (hT : T.IsFredholm) : (-T).IsFredholm

The negation of a Fredholm operator is Fredholm.

theorem ContinuousLinearMap.IsFredholm.equiv_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] {T : E →L[𝕜] F} (hT : T.IsFredholm) (e : F ≃L[𝕜] G) : (↑e ∘SL T).IsFredholm

Postcomposing a Fredholm operator with a continuous linear equivalence yields a Fredholm operator.

This is the mpr direction of Mathlib's ContinuousLinearMap.isFredholm_equiv_comp, which states the ↔ and so is stronger, but assumes a complete scalar field. Transporting the structure fields directly proves this implication over any NontriviallyNormedField.

theorem ContinuousLinearMap.IsFredholm.comp_equiv {𝕜 : 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] {T : E →L[𝕜] F} (hT : T.IsFredholm) (e : G ≃L[𝕜] E) : (T ∘SL ↑e).IsFredholm

Precomposing a Fredholm operator with a continuous linear equivalence yields a Fredholm operator.

This is the mpr direction of Mathlib's ContinuousLinearMap.isFredholm_comp_equiv, which states the ↔ and so is stronger, but assumes a complete scalar field. Transporting the structure fields directly proves this implication over any NontriviallyNormedField.