Coefficientwise base change of Fredholm series, resolvents and Riesz projectors

Let f : R →+* S be a bounded unital homomorphism of complete ultrametric normed commutative rings, with R Tate (TauCeti.NormedRing.IsTate R), and let u_S = u.mapCoeffs f hf be the coefficientwise extension of an endomorphism u of the model space C₀(I, R). The Fredholm series of u_S is the coefficientwise image of that of u, by continuity of f on the convergent principal-minor sums (ContinuousLinearMap.IsRowCompact.charPowerSeries_map).

For row-compact u the whole spectral calculus at a scalar a follows, at the scalar f a:

• the values of the Hasse derivatives of the Fredholm series, hence the Fredholm determinant and good zeros (ContinuousLinearMap.IsRowCompact.fredholmDet_mapCoeffs, ContinuousLinearMap.IsRowCompact.isGoodZero_charPowerSeries_mapCoeffs);
• the coefficients of the Fredholm resolvent (ContinuousLinearMap.IsRowCompact.resolventCoeff_mapCoeffs) and, when S is also Tate (TauCeti.NormedRing.IsTate S), the values of its Hasse derivatives (ContinuousLinearMap.IsRowCompact.resolventHasseDerivAt_mapCoeffs), since coefficient extension is a continuous ring homomorphism on endomorphisms;
• when S is Tate, Riesz projections, which need no compactness at all (ContinuousLinearMap.IsRieszProjection.mapCoeffs), and the explicit Riesz projector (ContinuousLinearMap.IsRowCompact.rieszProjection_mapCoeffs).

This comparison allows coefficient rings without a common ground field and does not require Noetherianity, flatness or a completed tensor product. Over rings with nilpotents it retains the coefficient information that evaluation at field-valued points would lose.

References

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

theorem ContinuousLinearMap.IsRowCompact.charPowerSeries_map {I : Type u_1} {R : Type u_3} {S : Type u_4} [TopologicalSpace I] [DiscreteTopology I] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] [DecidableEq I] [IsUltrametricDist R] [CompleteSpace R] {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hu : u.IsRowCompact) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) : (u.mapCoeffs f hf).matrixCoeff.charPowerSeries = (PowerSeries.map f) u.matrixCoeff.charPowerSeries

The Fredholm series commutes with bounded coefficient extension. This is an equality of power series over the coefficient ring, including when that ring has nilpotents.

theorem ContinuousLinearMap.IsRowCompact.evalAt_hasseDeriv_charPowerSeries_mapCoeffs {I : Type u_1} {R : Type u_3} {S : Type u_4} [TopologicalSpace I] [DiscreteTopology I] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] [DecidableEq I] [IsUltrametricDist R] [CompleteSpace R] {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hu : u.IsRowCompact) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) (k : ℕ) (a : R) : ((PowerSeries.hasseDeriv k) (u.mapCoeffs f hf).matrixCoeff.charPowerSeries).evalAt (f a) = f (((PowerSeries.hasseDeriv k) u.matrixCoeff.charPowerSeries).evalAt a)

The values at f a of the Hasse derivatives of the Fredholm series of the extension are the images of their values at a.

theorem ContinuousLinearMap.IsRowCompact.evalAt_charPowerSeries_mapCoeffs {I : Type u_1} {R : Type u_3} {S : Type u_4} [TopologicalSpace I] [DiscreteTopology I] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] [DecidableEq I] [IsUltrametricDist R] [CompleteSpace R] {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hu : u.IsRowCompact) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) (a : R) : (u.mapCoeffs f hf).matrixCoeff.charPowerSeries.evalAt (f a) = f (u.matrixCoeff.charPowerSeries.evalAt a)

The value H_u(a) of the Fredholm series at a scalar commutes with bounded coefficient extension.

theorem ContinuousLinearMap.IsRowCompact.fredholmDet_mapCoeffs {I : Type u_1} {R : Type u_3} {S : Type u_4} [TopologicalSpace I] [DiscreteTopology I] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] [DecidableEq I] [IsUltrametricDist R] [CompleteSpace R] {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hu : u.IsRowCompact) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) : (u.mapCoeffs f hf).fredholmDet = f u.fredholmDet

Bounded base change of the Fredholm determinant. For row-compact u, det (1 - u_S) = f (det (1 - u)).

theorem ContinuousLinearMap.IsRowCompact.isGoodZero_charPowerSeries_mapCoeffs {I : Type u_1} {R : Type u_3} {S : Type u_4} [TopologicalSpace I] [DiscreteTopology I] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] [DecidableEq I] [IsUltrametricDist R] [CompleteSpace R] {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hu : u.IsRowCompact) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) {a : R} {h : ℕ} (ha : u.matrixCoeff.charPowerSeries.IsGoodZero a h) : (u.mapCoeffs f hf).matrixCoeff.charPowerSeries.IsGoodZero (f a) h

A good zero a of order h of the Fredholm series of a row-compact u gives the good zero f a of the same order of the Fredholm series of its extension.

theorem ContinuousLinearMap.IsRowCompact.resolventCoeff_mapCoeffs {I : Type u_1} {R : Type u_3} {S : Type u_4} [TopologicalSpace I] [DiscreteTopology I] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] [DecidableEq I] [IsUltrametricDist R] [CompleteSpace R] {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hu : u.IsRowCompact) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) (m : ℕ) : (u.mapCoeffs f hf).resolventCoeff m = (u.resolventCoeff m).mapCoeffs f hf

The coefficients of the Fredholm resolvent commute with bounded coefficient extension.

theorem ContinuousLinearMap.IsRowCompact.resolventHasseDerivAt_mapCoeffs {I : Type u_1} {R : Type u_3} {S : Type u_4} [TopologicalSpace I] [DiscreteTopology I] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] [DecidableEq I] [IsUltrametricDist R] [CompleteSpace R] {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} [TauCeti.NormedRing.IsTate S] (hu : u.IsRowCompact) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) (k : ℕ) (a : R) : (u.mapCoeffs f hf).resolventHasseDerivAt k (f a) = (u.resolventHasseDerivAt k a).mapCoeffs f hf

Bounded base change of the Fredholm resolvent. For row-compact u, the value at f a of the k-th Hasse derivative of the Fredholm resolvent of the extension is the extension of its value at a.

theorem ContinuousLinearMap.IsRowCompact.resolventAt_mapCoeffs {I : Type u_1} {R : Type u_3} {S : Type u_4} [TopologicalSpace I] [DiscreteTopology I] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] [DecidableEq I] [IsUltrametricDist R] [CompleteSpace R] {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} [TauCeti.NormedRing.IsTate S] (hu : u.IsRowCompact) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) (a : R) : (u.mapCoeffs f hf).resolventAt (f a) = (u.resolventAt a).mapCoeffs f hf

The value V(a) of the Fredholm resolvent of a row-compact operator commutes with bounded coefficient extension.

theorem ContinuousLinearMap.IsRowCompact.rieszProjection_mapCoeffs {I : Type u_1} {R : Type u_3} {S : Type u_4} [TopologicalSpace I] [DiscreteTopology I] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] [DecidableEq I] [IsUltrametricDist R] [CompleteSpace R] {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} [TauCeti.NormedRing.IsTate S] (hu : u.IsRowCompact) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) {a : R} {h : ℕ} (hc : IsUnit (((PowerSeries.hasseDeriv h) u.matrixCoeff.charPowerSeries).evalAt a)) : (u.mapCoeffs f hf).rieszProjection (f a) h = (u.rieszProjection a h).mapCoeffs f hf

Bounded base change of the Riesz projector. If ΔʰH_u(a) is a unit, the Riesz projector of the extension of a row-compact u at f a is the extension of the Riesz projector of u at a.

theorem ContinuousLinearMap.IsRieszProjection.mapCoeffs {J : Type u_2} {R : Type u_3} {S : Type u_4} [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] [TauCeti.NormedRing.IsTate S] {u E : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap J R} {a : R} {h : ℕ} (hE : u.IsRieszProjection a h E) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) : (u.mapCoeffs f hf).IsRieszProjection (f a) h (E.mapCoeffs f hf)

Riesz projections under bounded base change. The coefficientwise extension of a Riesz projection of u at a of order h is a Riesz projection of the extension of u at f a of the same order. No compactness is needed.