The Fredholm alternative and eigenvalues of row-compact operators

Let u be row compact on C₀(I, K) over a complete nontrivially normed ultrametric field. Every operator 1 - a • u is Fredholm in Mathlib's sense and has index zero. Thus its range is closed, its kernel and cokernel are finite dimensional, and its kernel has a continuous complement. The field need not be locally compact, discretely valued or spherically complete.

The general Fredholm alternative for completely continuous operators supplies these results. Combining it with the Fredholm-series description of the spectrum shows that every zero a of H_u gives the eigenvalue a⁻¹. The condition a ≠ 0 is automatic because H_u(0) = 1. This identifies actual eigenvalues, without asserting an algebraic multiplicity or a dimension formula for a generalised eigenspace. Nonzero eigenvalues in the original field are preserved and reflected by bounded field extension.

References

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

theorem ContinuousLinearMap.IsRowCompact.isFredholm_one_sub_smul {K : Type u_1} {I : Type u_2} [NontriviallyNormedField K] [CompleteSpace K] [IsUltrametricDist K] [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {u : ZeroAtInftyContinuousMap I K →L[K] ZeroAtInftyContinuousMap I K} (hu : u.IsRowCompact) (a : K) : (1 - a • u).IsFredholm

Every scalar multiple of a row-compact operator is a Fredholm perturbation of the identity, including at zeros of its Fredholm series.

@[simp]

theorem ContinuousLinearMap.IsRowCompact.index_one_sub_smul_eq_zero {K : Type u_1} {I : Type u_2} [NontriviallyNormedField K] [CompleteSpace K] [IsUltrametricDist K] [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {u : ZeroAtInftyContinuousMap I K →L[K] ZeroAtInftyContinuousMap I K} (hu : u.IsRowCompact) (a : K) : (1 - a • u).index = 0

The Fredholm operator 1 - a • u has index zero for every scalar a.

theorem ContinuousLinearMap.IsRowCompact.evalAt_charPowerSeries_eq_zero_iff_hasEigenvalue {K : Type u_1} {I : Type u_2} [NontriviallyNormedField K] [CompleteSpace K] [IsUltrametricDist K] [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {u : ZeroAtInftyContinuousMap I K →L[K] ZeroAtInftyContinuousMap I K} (hu : u.IsRowCompact) {a : K} : u.matrixCoeff.charPowerSeries.evalAt a = 0 ↔ a ≠ 0 ∧ Module.End.HasEigenvalue (↑u) a⁻¹

The zeros of the Fredholm series of a row-compact operator are exactly the inverses of its nonzero eigenvalues. This conclusion concerns eigenvalues in the given coefficient field.

@[simp]

theorem ContinuousLinearMap.IsRowCompact.hasEigenvalue_mapCoeffs_iff {K : Type u_1} {I : Type u_2} [NontriviallyNormedField K] [CompleteSpace K] [IsUltrametricDist K] [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {u : ZeroAtInftyContinuousMap I K →L[K] ZeroAtInftyContinuousMap I K} {L : Type u_3} [NontriviallyNormedField L] [CompleteSpace L] [IsUltrametricDist L] (hu : u.IsRowCompact) (f : K →+* L) (hf : ∃ (C : NNReal), ∀ (x : K), ‖f x‖ ≤ ↑C * ‖x‖) {μ : K} (hμ : μ ≠ 0) : Module.End.HasEigenvalue (↑(u.mapCoeffs f hf)) (f μ) ↔ Module.End.HasEigenvalue (↑u) μ

A nonzero scalar of the original field is an eigenvalue after bounded field extension exactly when it was an eigenvalue before extension. This does not address the eigenvalue zero.