Injective and surjective criteria for Fredholm operators

This file gives streamlined Fredholm criteria when an operator is already known to be injective or surjective. Between Banach spaces over an IsRCLikeNormedField, a surjective continuous linear map is Fredholm exactly when its kernel is finite dimensional. Between Banach spaces over any nontrivially normed field, an injective continuous linear map with closed range is Fredholm exactly when its cokernel is finite dimensional. Specialising both sides gives the bijective corollary: a bijective continuous linear map between Banach spaces is Fredholm.

These criteria are the elementary endpoints of the finite-dimensional reductions used throughout Fredholm theory. As an application of the injective closed-range criterion, the inclusion of the kernel of an operator of finite rank is Fredholm.

Main declarations

• TauCeti.isFredholm_iff_finite_ker_of_surjective: the surjective criterion.
• TauCeti.isFredholm_iff_finite_coker_of_injective: the injective closed-range criterion.
• TauCeti.isFredholm_ker_subtypeL: the inclusion of the kernel of an operator of finite rank is Fredholm.
• ContinuousLinearMap.IsFredholm.of_bijective: a bijective continuous linear map between Banach spaces is Fredholm.

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

theorem ContinuousLinearMap.IsFredholm.of_surjective {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [IsRCLikeNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {T : E →L[K] F} (hT : Function.Surjective ⇑T) [FiniteDimensional K ↥(↑T).ker] : T.IsFredholm

A surjective continuous linear map between Banach spaces over an IsRCLikeNormedField with finite-dimensional kernel is Fredholm.

theorem TauCeti.isFredholm_iff_finite_ker_of_surjective {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [IsRCLikeNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {T : E →L[K] F} (hT : Function.Surjective ⇑T) : T.IsFredholm ↔ FiniteDimensional K ↥(↑T).ker

For a surjective continuous linear map between Banach spaces over an IsRCLikeNormedField, Fredholmness is equivalent to finite-dimensionality of the kernel.

theorem ContinuousLinearMap.IsFredholm.of_injective {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {T : E →L[K] F} (hT : Function.Injective ⇑T) (hclosed : IsClosed ↑(↑T).range) [FiniteDimensional K (F ⧸ (↑T).range)] : T.IsFredholm

An injective continuous linear map between Banach spaces with closed range and finite-dimensional cokernel is Fredholm.

theorem TauCeti.isFredholm_iff_finite_coker_of_injective {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {T : E →L[K] F} (hT : Function.Injective ⇑T) (hclosed : IsClosed ↑(↑T).range) : T.IsFredholm ↔ FiniteDimensional K (F ⧸ (↑T).range)

For an injective continuous linear map between Banach spaces with closed range, Fredholmness is equivalent to finite-dimensionality of the cokernel.

theorem TauCeti.isFredholm_ker_subtypeL {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] {T : E →L[K] F} (hT : (↑T).HasFiniteRange) : (↑T).ker.subtypeL.IsFredholm

The inclusion of the kernel of an operator of finite rank is Fredholm: the kernel is closed and, by the first isomorphism theorem, of finite codimension.

theorem ContinuousLinearMap.IsFredholm.of_bijective {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {T : E →L[K] F} (hT : Function.Bijective ⇑T) : T.IsFredholm

A bijective continuous linear map between Banach spaces is Fredholm. This formulation does not require bundling its inverse as a continuous linear equivalence. Codomain completeness is used by Mathlib's bounded-inverse construction ContinuousLinearEquiv.ofBijective.