The Fredholm alternative for completely continuous operators

On a Banach space over a complete nontrivially normed field, 1 - u is Fredholm of index zero whenever u is a norm limit of operators of finite rank. In particular, injectivity, surjectivity and invertibility of 1 - u are equivalent, and every nonzero spectral value of u is an eigenvalue. These statements apply over nonarchimedean fields without local compactness or spherical completeness. Only the Fredholm and index statements need the scalar field to be complete; the equivalences of injectivity, surjectivity and invertibility, and the eigenvalue statement, follow from the algebraic fact that 1 + F is injective if and only if it is surjective for F of finite rank, and hold over any nontrivially normed field.

The native ContinuousLinearMap.IsFredholm conclusion includes strictness, closed range, finite-dimensional kernel and cokernel, and a continuous complement to the kernel.

References

• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §§2–3, 7.

theorem ContinuousLinearMap.IsCompletelyContinuous.isFredholm_one_sub {K : Type u_1} {E : Type u_2} [NontriviallyNormedField K] [CompleteSpace K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] {u : E →L[K] E} (hu : u.IsCompletelyContinuous) : (1 - u).IsFredholm

A completely continuous perturbation of the identity is a Fredholm operator, over any complete nontrivially normed field.

@[simp]

theorem ContinuousLinearMap.IsCompletelyContinuous.index_one_sub_eq_zero {K : Type u_1} {E : Type u_2} [NontriviallyNormedField K] [CompleteSpace K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] {u : E →L[K] E} (hu : u.IsCompletelyContinuous) : (1 - u).index = 0

A completely continuous perturbation of the identity has Fredholm index zero.

theorem ContinuousLinearMap.IsCompletelyContinuous.injective_one_sub_iff_surjective {K : Type u_1} {E : Type u_2} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] {u : E →L[K] E} (hu : u.IsCompletelyContinuous) : Function.Injective ⇑(1 - u) ↔ Function.Surjective ⇑(1 - u)

For a completely continuous u, 1 - u is injective if and only if it is surjective.

theorem ContinuousLinearMap.IsCompletelyContinuous.isUnit_one_sub_iff_injective {K : Type u_1} {E : Type u_2} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] {u : E →L[K] E} (hu : u.IsCompletelyContinuous) : IsUnit (1 - u) ↔ Function.Injective ⇑(1 - u)

For a completely continuous u, injectivity of 1 - u is equivalent to invertibility.

theorem ContinuousLinearMap.IsCompletelyContinuous.isUnit_one_sub_iff_surjective {K : Type u_1} {E : Type u_2} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] {u : E →L[K] E} (hu : u.IsCompletelyContinuous) : IsUnit (1 - u) ↔ Function.Surjective ⇑(1 - u)

For a completely continuous u, surjectivity of 1 - u is equivalent to invertibility.

theorem ContinuousLinearMap.IsCompletelyContinuous.hasEigenvalue_iff_mem_spectrum {K : Type u_1} {E : Type u_2} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] {u : E →L[K] E} (hu : u.IsCompletelyContinuous) {μ : K} (hμ : μ ≠ 0) : Module.End.HasEigenvalue (↑u) μ ↔ μ ∈ spectrum K u

Every nonzero spectral value of a completely continuous operator is an eigenvalue. The spectrum is the spectrum in the algebra of continuous endomorphisms.