Fredholm invertibility on modules with property (Pr)

The Fredholm series of a row-compact endomorphism of a module with property (Pr) detects invertibility: 1 - a u is a unit exactly when H_u(a) is a unit. This transports the model-space criterion along an arbitrary continuous linear retract, without assuming a finite free complement. The rectangular Jacobson identity compares 1 - a u with 1 - a i u r.

Over a complete ultrametric field, the nonzero spectrum is therefore the set of inverses of Fredholm zeros. Over coefficient rings, the criterion is about units, not vanishing; it applies also to nonreduced rings and finite projective modules of nonconstant rank. No assertion about the spectral value zero is made.

References

• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §§5–7.
• C. Johansson and J. Newton, Extended eigenvarieties for overconvergent cohomology, arXiv:1604.07739, §§2.1–2.2.

theorem ContinuousLinearMap.IsPrCompact.isUnit_one_sub_smul_iff {R : Type u_1} {M : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [Module R M] [ContinuousConstSMul R M] {u : M →L[R] M} (hu : u.IsPrCompact) {a : R} : IsUnit (1 - a • u) ↔ IsUnit (u.charPowerSeries.evalAt a)

For a row-compact endomorphism of a module with property (Pr), 1 - a u is invertible exactly when its Fredholm series evaluated at a is a unit.

theorem ContinuousLinearMap.IsPrCompact.inv_mem_spectrum_iff {R : Type u_1} {M : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] [SeminormedAddCommGroup M] [Module R M] [ContinuousConstSMul R M] {u : M →L[R] M} (hu : u.IsPrCompact) {a : Rˣ} : ↑a⁻¹ ∈ spectrum R u ↔ ¬IsUnit (u.charPowerSeries.evalAt ↑a)

For a unit a in the coefficient ring, a⁻¹ is in the spectrum of a row-compact endomorphism of a (Pr) module exactly when H_u(a) is not a unit.

theorem ContinuousLinearMap.IsPrCompact.mem_spectrum_iff_evalAt_inv_eq_zero {K : Type u_1} {M : Type u_2} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] [SeminormedAddCommGroup M] [Module K M] [ContinuousConstSMul K M] {u : M →L[K] M} (hu : u.IsPrCompact) {μ : K} (hμ : μ ≠ 0) : μ ∈ spectrum K u ↔ u.charPowerSeries.evalAt μ⁻¹ = 0

The nonzero spectrum of a row-compact endomorphism of a (Pr) module over a complete ultrametric field is detected by the zeros of its Fredholm series.

theorem ContinuousLinearMap.IsPrCompact.evalAt_charPowerSeries_eq_zero_iff {K : Type u_1} {M : Type u_2} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] [SeminormedAddCommGroup M] [Module K M] [ContinuousConstSMul K M] {u : M →L[K] M} (hu : u.IsPrCompact) {a : K} : u.charPowerSeries.evalAt a = 0 ↔ a ≠ 0 ∧ a⁻¹ ∈ spectrum K u

Fredholm zeros on a (Pr) module are exactly the inverses of its nonzero spectral values. In particular zero is never a Fredholm zero.