Closed range from a finite-dimensional cokernel

For the nonlinear-analysis substrate of the analytic Heegaard Floer roadmap (Lane F0, "Fredholm operators and index theory"), this file proves that the closed-range hypothesis in the definition of a Fredholm operator is automatic between Banach spaces once the cokernel is finite dimensional.

Concretely, a continuous linear map T : E →L[𝕜] F between complete normed spaces whose cokernel F ⧸ range T is finite dimensional already has closed range. The proof is a clean application of the Banach open mapping theorem: choosing a finite-dimensional algebraic complement N of range T, the auxiliary map Φ(x, n) = T x + n from E × N is a continuous linear surjection between Banach spaces, hence a quotient map. Its preimage Φ ⁻¹' range T = E × {0} is closed, and a quotient map carries the closed-set characterization that a set is closed exactly when its preimage is, so range T is closed.

This upgrades the Fredholm predicate of TauCeti.Analysis.Fredholm.Basic: over Banach spaces over an IsRCLikeNormedField (in particular, real or complex Banach spaces), a Fredholm operator is exactly a continuous linear map with finite-dimensional kernel and cokernel, the closed-range condition following for free. Downstream this lets Sard–Smale and transversality arguments certify Fredholmness of a linearization from the two defect spaces alone, without a separate closed-range check.

Main declarations

• ContinuousLinearMap.isClosed_range_of_finite_coker: a continuous linear map between Banach spaces with finite-dimensional cokernel has closed range.
• ContinuousLinearMap.IsFredholm.of_finite_ker_coker: over Banach spaces over an IsRCLikeNormedField, finite-dimensional kernel and cokernel suffice for Fredholmness.
• TauCeti.isFredholm_iff_finite_ker_coker: over Banach spaces over an IsRCLikeNormedField, the Fredholm predicate is equivalent to finite dimensionality of the kernel and cokernel.

The conventions follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Appendix A.1, where a Fredholm operator has finite-dimensional kernel and cokernel; the closed-range condition is noted there to be automatic between Banach spaces.

theorem ContinuousLinearMap.isClosed_range_of_finite_coker {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) [FiniteDimensional 𝕜 (F ⧸ (↑T).range)] : IsClosed ↑(↑T).range

A continuous linear map between Banach spaces whose cokernel F ⧸ range T is finite dimensional has closed range.

Closedness of the range is therefore not an independent hypothesis in the Banach setting: it is forced by finite dimensionality of the cokernel. The proof runs the Banach open mapping theorem on the surjection Φ(x, n) = T x + n from E × N, where N is a finite-dimensional algebraic complement of range T.

theorem ContinuousLinearMap.IsFredholm.of_finite_ker_coker {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) (hker : FiniteDimensional 𝕜 ↥(↑T).ker) (hcoker : FiniteDimensional 𝕜 (F ⧸ (↑T).range)) : T.IsFredholm

Over Banach spaces over an IsRCLikeNormedField, a continuous linear map with finite-dimensional kernel and cokernel is Fredholm: the closed-range condition is automatic.

This is the Banach-space form of the Fredholm criterion, complementing the direct constructor of ContinuousLinearMap.IsFredholm by removing the closed-range obligation.

theorem TauCeti.isFredholm_iff_finite_ker_coker {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : T.IsFredholm ↔ FiniteDimensional 𝕜 ↥(↑T).ker ∧ FiniteDimensional 𝕜 (F ⧸ (↑T).range)

Over Banach spaces over an IsRCLikeNormedField, the Fredholm predicate is equivalent to finite dimensionality of the kernel and cokernel; closedness of the range is not an independent condition.