Invertibility and the nonzero spectrum of a row-compact operator

Let R be a complete ultrametric normed commutative ring with Tate scalars, I a discrete index type, and u a row-compact endomorphism of the model space C₀(I, R) with Fredholm series H_u(T) = det (1 - T u), the principal-minor series u.matrixCoeff.charPowerSeries. The Fredholm series detects exactly which operators 1 - a • u are invertible in the algebra of continuous endomorphisms:

IsUnit (1 - a • u) ↔ IsUnit (H_u(a)) (ContinuousLinearMap.IsRowCompact.isUnit_one_sub_smul_iff).

The resolvent V(a) supplies the inverse when H_u(a) is a unit, and multiplicativity of the Fredholm determinant gives the converse. In terms of the spectrum of u over R, the inverse r⁻¹ of a unit r lies in the spectrum exactly when H_u(r) is not a unit (ContinuousLinearMap.IsRowCompact.inv_mem_spectrum_iff). Over coefficient rings with nilpotents this is a condition on units, not on vanishing.

Over a complete nontrivially normed ultrametric field K it becomes Serre's description of the nonzero spectrum: for μ ≠ 0,

μ ∈ spectrum K u ↔ H_u(μ⁻¹) = 0 (ContinuousLinearMap.IsRowCompact.mem_spectrum_iff_evalAt_inv_eq_zero).

Since H_u(0) = 1, every zero a of H_u is nonzero, and the zeros of H_u are exactly the inverses of the nonzero spectral values (ContinuousLinearMap.IsRowCompact.evalAt_charPowerSeries_eq_zero_iff). Nothing is asserted about 0 ∈ spectrum K u, which the Fredholm series does not see.

Strassmann's theorem then bounds the spectrum away from zero. If H_u is distinguished of degree s at the radius ε⁻¹, that is, s is the largest index at which ‖cₙ‖ ε⁻ⁿ attains its maximum, then at most s spectral values have norm at least ε (ContinuousLinearMap.IsRowCompact.encard_setOf_mem_spectrum_le). Such an s exists for every ε > 0, since H_u is entire and nonzero, so only finitely many spectral values have norm bounded below by a positive number, and every nonzero spectral value is isolated in the spectrum. Zero may be an accumulation point of the spectrum. The same bound, finiteness and isolation hold for the extension of u to C₀(I, L) along any complete normed field extension L of K, such as a complete field over which H_u splits: the spectrum of the extension is controlled by the zeros of H_u in L.

Main results

• ContinuousLinearMap.IsRowCompact.isUnit_one_sub_smul_iff: 1 - a • u is invertible if and only if H_u(a) is a unit.
• ContinuousLinearMap.IsRowCompact.isUnit_one_sub_iff: 1 - u is invertible if and only if the Fredholm determinant det (1 - u) is a unit.
• ContinuousLinearMap.IsRowCompact.mem_spectrum_iff_evalAt_inv_eq_zero: over a field, a nonzero μ lies in the spectrum of u if and only if H_u(μ⁻¹) = 0.
• ContinuousLinearMap.IsRowCompact.encard_setOf_mem_spectrum_mapCoeffs_le and ContinuousLinearMap.IsRowCompact.finite_setOf_mem_spectrum_mapCoeffs: after extension to a complete normed field L, at most s spectral values, and in any case finitely many, have norm at least ε, where H_u is distinguished of degree s at ε⁻¹.
• ContinuousLinearMap.IsRowCompact.encard_setOf_mem_spectrum_le and ContinuousLinearMap.IsRowCompact.finite_setOf_mem_spectrum: the same over K itself.
• ContinuousLinearMap.IsRowCompact.eventually_notMem_spectrum_mapCoeffs and ContinuousLinearMap.IsRowCompact.eventually_notMem_spectrum: every nonzero spectral value is isolated in the spectrum, after extension to L and over K itself.

References

• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §§5–7.
• R. Coleman, p-adic Banach spaces and families of modular forms, Invent. Math. 127 (1997), 417–479, Appendix A.

theorem ContinuousLinearMap.IsRowCompact.isUnit_one_sub_smul_iff {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hu : u.IsRowCompact) {a : R} : IsUnit (1 - a • u) ↔ IsUnit (u.matrixCoeff.charPowerSeries.evalAt a)

Invertibility and the Fredholm series. For a row-compact endomorphism u of C₀(I, R), the operator 1 - a • u is invertible if and only if the value H_u(a) of the Fredholm series det (1 - T u) is a unit of R.

theorem ContinuousLinearMap.IsRowCompact.isUnit_one_sub_iff {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hu : u.IsRowCompact) : IsUnit (1 - u) ↔ IsUnit u.fredholmDet

Invertibility and the Fredholm determinant. For a row-compact endomorphism u of C₀(I, R), the operator 1 - u is invertible if and only if the Fredholm determinant det (1 - u) is a unit of R.

theorem ContinuousLinearMap.IsRowCompact.inv_mem_spectrum_iff {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hu : u.IsRowCompact) {r : Rˣ} : ↑r⁻¹ ∈ spectrum R u ↔ ¬IsUnit (u.matrixCoeff.charPowerSeries.evalAt ↑r)

Unit spectral values. For a row-compact endomorphism u of C₀(I, R) and a unit r of R, the inverse r⁻¹ lies in the spectrum of u if and only if the value H_u(r) of the Fredholm series is not a unit of R.

theorem ContinuousLinearMap.IsRowCompact.mem_spectrum_iff_evalAt_inv_eq_zero {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {K : Type u_2} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {u : ZeroAtInftyContinuousMap I K →L[K] ZeroAtInftyContinuousMap I K} (hu : u.IsRowCompact) {μ : K} (hμ : μ ≠ 0) : μ ∈ spectrum K u ↔ u.matrixCoeff.charPowerSeries.evalAt μ⁻¹ = 0

The nonzero spectrum of a row-compact operator. For a row-compact endomorphism u of C₀(I, K) over a complete ultrametric field and μ ≠ 0, μ lies in the spectrum of u if and only if μ⁻¹ is a zero of the Fredholm series det (1 - T u).

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

The zeros of the Fredholm series. For a row-compact endomorphism u of C₀(I, K), the zeros of the Fredholm series det (1 - T u) are exactly the inverses of the nonzero elements of the spectrum of u. Since det (1 - 0 u) = 1, no zero is 0.

theorem ContinuousLinearMap.IsRowCompact.encard_setOf_mem_spectrum_mapCoeffs_le {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {K : Type u_2} {L : Type u_3} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] [NontriviallyNormedField L] [NormedAlgebra K L] [IsUltrametricDist L] [CompleteSpace L] {u : ZeroAtInftyContinuousMap I K →L[K] ZeroAtInftyContinuousMap I K} (hu : u.IsRowCompact) {ε : ℝ} (hε : 0 < ε) {s : ℕ} (hs : TauCeti.PowerSeries.IsDistinguished ε⁻¹ s u.matrixCoeff.charPowerSeries) : {μ : L | μ ∈ spectrum L (u.mapCoeffs (algebraMap K L) ⋯) ∧ ε ≤ ‖μ‖}.encard ≤ ↑s

Strassmann's bound for the spectrum. Let u be a row-compact endomorphism of C₀(I, K), and let its Fredholm series H_u be distinguished of degree s at the radius ε⁻¹. Then the extension of u to C₀(I, L), for a complete normed field extension L of K, has at most s spectral values of norm at least ε.

theorem ContinuousLinearMap.IsRowCompact.finite_setOf_mem_spectrum_mapCoeffs {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {K : Type u_2} {L : Type u_3} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] [NontriviallyNormedField L] [NormedAlgebra K L] [IsUltrametricDist L] [CompleteSpace L] {u : ZeroAtInftyContinuousMap I K →L[K] ZeroAtInftyContinuousMap I K} (hu : u.IsRowCompact) {ε : ℝ} (hε : 0 < ε) : {μ : L | μ ∈ spectrum L (u.mapCoeffs (algebraMap K L) ⋯) ∧ ε ≤ ‖μ‖}.Finite

After extension to a complete normed field L, a row-compact endomorphism of C₀(I, K) has only finitely many spectral values of norm at least ε, for every ε > 0.

theorem ContinuousLinearMap.IsRowCompact.encard_setOf_mem_spectrum_le {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {K : Type u_2} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {u : ZeroAtInftyContinuousMap I K →L[K] ZeroAtInftyContinuousMap I K} (hu : u.IsRowCompact) {ε : ℝ} (hε : 0 < ε) {s : ℕ} (hs : TauCeti.PowerSeries.IsDistinguished ε⁻¹ s u.matrixCoeff.charPowerSeries) : {μ : K | μ ∈ spectrum K u ∧ ε ≤ ‖μ‖}.encard ≤ ↑s

Strassmann's bound for the spectrum over the coefficient field: if the Fredholm series of a row-compact endomorphism u of C₀(I, K) is distinguished of degree s at the radius ε⁻¹, then u has at most s spectral values of norm at least ε.

theorem ContinuousLinearMap.IsRowCompact.finite_setOf_mem_spectrum {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {K : Type u_2} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {u : ZeroAtInftyContinuousMap I K →L[K] ZeroAtInftyContinuousMap I K} (hu : u.IsRowCompact) {ε : ℝ} (hε : 0 < ε) : {μ : K | μ ∈ spectrum K u ∧ ε ≤ ‖μ‖}.Finite

A row-compact endomorphism of C₀(I, K) has only finitely many spectral values of norm at least ε, for every ε > 0.

theorem ContinuousLinearMap.IsRowCompact.eventually_notMem_spectrum_mapCoeffs {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {K : Type u_2} {L : Type u_3} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] [NontriviallyNormedField L] [NormedAlgebra K L] [IsUltrametricDist L] [CompleteSpace L] {u : ZeroAtInftyContinuousMap I K →L[K] ZeroAtInftyContinuousMap I K} (hu : u.IsRowCompact) {μ : L} (hμ : μ ≠ 0) : ∀ᶠ (ν : L) in nhdsWithin μ {μ}ᶜ, ν ∉ spectrum L (u.mapCoeffs (algebraMap K L) ⋯)

Nonzero spectral values are isolated. For a row-compact endomorphism u of C₀(I, K), a complete normed field extension L of K and μ : L with μ ≠ 0, no point of a punctured neighbourhood of μ lies in the spectrum of the extension of u to C₀(I, L).

theorem ContinuousLinearMap.IsRowCompact.eventually_notMem_spectrum {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {K : Type u_2} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {u : ZeroAtInftyContinuousMap I K →L[K] ZeroAtInftyContinuousMap I K} (hu : u.IsRowCompact) {μ : K} (hμ : μ ≠ 0) : ∀ᶠ (ν : K) in nhdsWithin μ {μ}ᶜ, ν ∉ spectrum K u

Nonzero spectral values are isolated over the coefficient field: for a row-compact endomorphism u of C₀(I, K) and μ ≠ 0, no point of a punctured neighbourhood of μ lies in the spectrum of u.