The zero Fredholm operator

This file characterizes when the zero continuous linear map is Fredholm. Its kernel is the whole domain and its cokernel is the whole codomain, so it is Fredholm exactly when both spaces are finite dimensional. Its index formula is supplied by TauCeti.Topology.Algebra.Module.ContinuousLinearMap.Index.

The result isolates the finite-dimensional block in a Fredholm decomposition: after an invertible block is split off, a remaining zero block records precisely the kernel and cokernel. The characterization needs only topologies on the domain and codomain, with the codomain T1; neither a norm nor continuity of addition or scalar multiplication is required.

Main declarations

• TauCeti.isFredholm_zero_iff: the zero operator is Fredholm exactly when its domain and codomain are finite dimensional.

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

@[simp]

theorem TauCeti.isFredholm_zero_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [T1Space F] : ContinuousLinearMap.IsFredholm 0 ↔ FiniteDimensional 𝕜 E ∧ FiniteDimensional 𝕜 F

The zero continuous linear map is Fredholm exactly when its domain and codomain are both finite dimensional.