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

A continuous linear map between normed spaces is a Fredholm operator if its kernel is finite dimensional, its range is closed, and its cokernel is finite dimensional.

Closedness of the range is a genuine hypothesis: over an incomplete space a finite-dimensional cokernel need not force it. It is bundled here following the standard convention (McDuff--Salamon, Appendix A.1).

finiteDimensional_ker : FiniteDimensional 𝕜 ↥(↑T).ker
The kernel of a Fredholm operator is finite dimensional.
isClosed_range : IsClosed ↑(↑T).range
The range of a Fredholm operator is closed.
finiteDimensional_coker : FiniteDimensional 𝕜 (F ⧸ (↑T).range)
The cokernel of a Fredholm operator is finite dimensional.

Instances For

source

theorem TauCeti.IsFredholm.of_continuousLinearEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : E ≃L[𝕜] F) :

IsFredholm ↑e

A continuous linear equivalence is a Fredholm operator.

source

theorem TauCeti.isFredholm_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] :

IsFredholm (ContinuousLinearMap.id 𝕜 E)

The identity operator is Fredholm: its kernel is trivial and its range is everything.