Fredholm series of row-compact operators on modules with property (Pr)

Let R be a complete ultrametric normed commutative ring with ‖1‖ = 1 and Tate scalars, and M a module with property (Pr) (TauCeti.HasPr R M): a continuous linear retract M →ⁱ C₀(J, R) →ʳ M, r ∘ i = id, of a model space. The Fredholm series H_u(T) = det (1 - T u) of an endomorphism u of M (ContinuousLinearMap.charPowerSeries) is the principal-minor series of the extension i ∘ u ∘ r of u to C₀(J, R), for a retract presentation of M fixed by choice.

For a row-compact u (ContinuousLinearMap.IsPrCompact) the series does not depend on the presentation: for every retract r ∘ i = id of M through a model space, in any universe,

H_u = det (1 - T (i ∘ u ∘ r)) (ContinuousLinearMap.IsPrCompact.charPowerSeries_eq).

Given two presentations (i, r) and (i', r'), the extensions factor as i ∘ u ∘ r = (i ∘ r') ∘ (i' ∘ u ∘ r) and i' ∘ u ∘ r' = (i' ∘ u ∘ r) ∘ (i ∘ r'), and the cyclicity of Fredholm determinants of model-space operators (ContinuousLinearMap.IsRowCompact.charPowerSeries_matrixCoeff_comp_comm) applies to the row-compact factor i' ∘ u ∘ r. No finite-dimensional complement of the range of i is presumed.

Consequently H_u is entire, satisfies H_{u ∘ v} = H_{v ∘ u} for maps between two (Pr) modules when u is row compact, is invariant under conjugation by continuous linear equivalences, and rescales as H_{c u}(T) = H_u(c T). On a model space it is the principal-minor series of the matrix of u. On a finitely generated module with (Pr), which is projective, it is the reversed characteristic polynomial det (1 - X u) of finite projective modules (ContinuousLinearMap.charPowerSeries_eq_projectiveCharpolyRev). This polynomial need not have degree equal to a rank of M, and its leading coefficient need not be a unit: the rank of a finite projective module may vary over Spec R.

Main definitions

• ContinuousLinearMap.charPowerSeries: the Fredholm series det (1 - T u) of an endomorphism of a module with property (Pr).

Main results

• ContinuousLinearMap.IsPrCompact.charPowerSeries_eq: independence of the presentation.
• ContinuousLinearMap.IsRowCompact.charPowerSeries_eq_charPowerSeries_matrixCoeff: on a model space it is the principal-minor series of the matrix.
• ContinuousLinearMap.IsPrCompact.charPowerSeries_comp_comm: cyclicity det (1 - T (u ∘ v)) = det (1 - T (v ∘ u)).
• ContinuousLinearMap.IsPrCompact.charPowerSeries_conj: invariance under conjugation.
• ContinuousLinearMap.IsPrCompact.isEntire_charPowerSeries: the series is entire.
• ContinuousLinearMap.charPowerSeries_eq_projectiveCharpolyRev: comparison with the finite projective determinant.

References

• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §5.
• K. Buzzard, Eigenvarieties, in L-functions and Galois Representations, LMS Lecture Note Series 320 (2007), §2.
• C. Johansson and J. Newton, Extended eigenvarieties for overconvergent cohomology, arXiv:1604.07739, §2.1.

noncomputable def ContinuousLinearMap.charPowerSeries {R : Type w} [SeminormedCommRing R] {M : Type u} [SeminormedAddCommGroup M] [Module R M] (u : M →L[R] M) : PowerSeries R

The Fredholm series det (1 - T u) of an endomorphism u of a module M with property (Pr): the principal-minor series of the extension i ∘ u ∘ r of u through a retract presentation r ∘ i = id of M by a model space C₀(J, R), fixed by choice. If u is row compact, it does not depend on the presentation (ContinuousLinearMap.IsPrCompact.charPowerSeries_eq). If M does not have property (Pr) the series is 1.

@[simp]

theorem ContinuousLinearMap.constantCoeff_charPowerSeries {R : Type w} [SeminormedCommRing R] {M : Type u} [SeminormedAddCommGroup M] [Module R M] (u : M →L[R] M) : PowerSeries.constantCoeff u.charPowerSeries = 1

The constant coefficient of the Fredholm series is 1.

theorem ContinuousLinearMap.charPowerSeries_ne_zero {R : Type w} [SeminormedCommRing R] {M : Type u} [SeminormedAddCommGroup M] [Module R M] [Nontrivial R] (u : M →L[R] M) : u.charPowerSeries ≠ 0

Over a nontrivial ring the Fredholm series is nonzero, since its constant coefficient is 1.

@[simp]

theorem ContinuousLinearMap.charPowerSeries_zero {R : Type w} [SeminormedCommRing R] {M : Type u} [SeminormedAddCommGroup M] [Module R M] : charPowerSeries 0 = 1

The Fredholm series of the zero endomorphism is 1.

theorem ContinuousLinearMap.IsPrCompact.charPowerSeries_eq {R : Type w} [NormedCommRing R] [NormOneClass R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] {M : Type u} [SeminormedAddCommGroup M] [Module R M] {u : M →L[R] M} (hu : u.IsPrCompact) {J : Type u_1} [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] {i : M →L[R] ZeroAtInftyContinuousMap J R} {r : ZeroAtInftyContinuousMap J R →L[R] M} (hri : r ∘SL i = ContinuousLinearMap.id R M) : u.charPowerSeries = (i ∘SL u ∘SL r).matrixCoeff.charPowerSeries

Independence of the presentation. The Fredholm series of a row-compact endomorphism u of a module with property (Pr) is the principal-minor series of its extension i ∘ u ∘ r through any retract presentation r ∘ i = id of the module by a model space.

theorem ContinuousLinearMap.IsRowCompact.charPowerSeries_eq_charPowerSeries_matrixCoeff {R : Type w} [NormedCommRing R] [NormOneClass R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hu : u.IsRowCompact) : u.charPowerSeries = u.matrixCoeff.charPowerSeries

On a model space, the Fredholm series of a row-compact endomorphism is the principal-minor series of its matrix.

theorem ContinuousLinearMap.IsPrCompact.isEntire_charPowerSeries {R : Type w} [NormedCommRing R] [NormOneClass R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] {M : Type u} [SeminormedAddCommGroup M] [Module R M] {u : M →L[R] M} (hu : u.IsPrCompact) : u.charPowerSeries.IsEntire

The Fredholm series of a row-compact endomorphism of a module with property (Pr) is entire.

theorem ContinuousLinearMap.IsPrCompact.charPowerSeries_comp_comm {R : Type w} [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {u : M →L[R] N} (hu : u.IsPrCompact) (v : N →L[R] M) : (u ∘SL v).charPowerSeries = (v ∘SL u).charPowerSeries

Cyclicity of Fredholm series on (Pr) modules. If u : M →L[R] N is row compact and v : N →L[R] M is any continuous linear map, the endomorphisms u ∘ v of N and v ∘ u of M have the same Fredholm series: det (1 - T (u ∘ v)) = det (1 - T (v ∘ u)).

theorem ContinuousLinearMap.IsPrCompact.charPowerSeries_conj {R : Type w} [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] {M : Type u} [SeminormedAddCommGroup M] [Module R M] {N : Type u} [SeminormedAddCommGroup N] [Module R N] {u : M →L[R] M} (hu : u.IsPrCompact) (e : M ≃L[R] N) : (↑e ∘SL u ∘SL ↑e.symm).charPowerSeries = u.charPowerSeries

Invariance under conjugation. The Fredholm series of a row-compact endomorphism u of a module with property (Pr) is unchanged by conjugation e ∘ u ∘ e⁻¹ by a continuous linear equivalence e, which need not be an isometry.

theorem ContinuousLinearMap.IsPrCompact.charPowerSeries_smul {R : Type w} [NormedCommRing R] [NormOneClass R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] {M : Type u} [SeminormedAddCommGroup M] [Module R M] [ContinuousConstSMul R M] {u : M →L[R] M} (hu : u.IsPrCompact) (c : R) : (c • u).charPowerSeries = (PowerSeries.rescale c) u.charPowerSeries

Scaling. For a row-compact endomorphism u of a module with property (Pr), the Fredholm series of c • u is that of u with the variable rescaled by c: H_{c u}(T) = H_u(c T).

theorem ContinuousLinearMap.charPowerSeries_eq_projectiveCharpolyRev {R : Type w} [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] {M : Type u} [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [Module.Finite R M] (hM : TauCeti.HasPr R M) (u : M →L[R] M) : u.charPowerSeries = ↑(↑u).projectiveCharpolyRev

Comparison with the finite projective determinant. On a finitely generated module with property (Pr), which is projective (TauCeti.HasPr.projective), the Fredholm series of every endomorphism u is the reversed characteristic polynomial det (1 - X u) of u as an endomorphism of a finite projective module.