Cyclicity of Fredholm determinants of row-compact operators

Let R be a complete ultrametric normed commutative ring with ‖1‖ = 1 and Tate scalars, and I, J discrete index types. For an endomorphism w of the model space C₀(I, R), the Fredholm determinant det (1 - T w) is the principal-minor series w.matrixCoeff.charPowerSeries of its matrix.

This file proves that for continuous linear maps u : C₀(J, R) →L[R] C₀(I, R) and v : C₀(I, R) →L[R] C₀(J, R), one of which is row compact, the determinants of the two composites agree:

det (1 - T (u ∘ v)) = det (1 - T (v ∘ u)) (ContinuousLinearMap.IsRowCompact.charPowerSeries_matrixCoeff_comp_comm).

Both composites are endomorphisms, of C₀(I, R) and of C₀(J, R) respectively, and both are row compact by the ideal property, so both series are entire (Matrix.isRestricted_charPowerSeries). Consequently the Fredholm determinant of a row-compact endomorphism is invariant under conjugation by any continuous linear equivalence of model spaces, possibly between different index types (ContinuousLinearMap.IsRowCompact.charPowerSeries_matrixCoeff_conj); no isometry is assumed.

The proof first treats an output truncation π_S ∘ u to a finite set S of coordinates. The determinant of π_S ∘ u ∘ v is the polynomial det (1 - X (u ∘ v)_S) of the finite block on S, while v ∘ π_S ∘ u factors through the finite free module R ^ S; its finite compressions are products of rectangular blocks, to which the finite identity det (1 - X A B) = det (1 - X B A) (Matrix.charpolyRev_mul_comm) applies. The general case follows by approximating u by its output truncations, since each Fredholm coefficient is continuous in operator norm on row-compact operators (ContinuousLinearMap.tendsto_charCoeff_matrixCoeff_of_tendsto).

Main results

• ContinuousLinearMap.tendsto_charCoeff_matrixCoeff_of_tendsto: the coefficients of the Fredholm determinant are continuous in operator norm on row-compact endomorphisms.
• ContinuousLinearMap.IsRowCompact.charPowerSeries_matrixCoeff_comp_comm: cyclicity det (1 - T (u ∘ v)) = det (1 - T (v ∘ u)) when u is row compact.
• ContinuousLinearMap.IsRowCompact.charPowerSeries_matrixCoeff_conj: invariance under conjugation by a continuous linear equivalence.

References

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

theorem ContinuousLinearMap.IsRowCompact.summable_principalMinor {I : Type u_1} {R : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [NormedCommRing R] [NormOneClass R] [IsUltrametricDist R] [CompleteSpace R] {w : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hw : w.IsRowCompact) (n : ℕ) : Summable fun (s : { s : Finset I // s.card = n }) => w.matrixCoeff.principalMinor ↑s

The principal minors of each size of a row-compact endomorphism of a model space form a summable family, so the coefficients of its Fredholm determinant are genuine sums.

theorem ContinuousLinearMap.tendsto_charCoeff_matrixCoeff_of_tendsto {I : Type u_1} {R : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [NormedCommRing R] [NormOneClass R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] {α : Type u_4} {l : Filter α} {w : α → ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} {w₀ : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hw : ∀ᶠ (a : α) in l, (w a).IsRowCompact) (hw₀ : w₀.IsRowCompact) (h : Filter.Tendsto (fun (a : α) => ‖w a - w₀‖) l (nhds 0)) (n : ℕ) : Filter.Tendsto (fun (a : α) => (w a).matrixCoeff.charCoeff n) l (nhds (w₀.matrixCoeff.charCoeff n))

Continuity of Fredholm coefficients in operator norm. If row-compact endomorphisms w a of a model space converge in operator norm to a row-compact endomorphism w₀, then each coefficient of the Fredholm determinant of w a converges to the corresponding coefficient for w₀.

theorem ContinuousLinearMap.IsRowCompact.charPowerSeries_matrixCoeff_comp_comm {I : Type u_1} {J : Type u_2} {R : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [NormOneClass R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] {u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R} (hu : u.IsRowCompact) (v : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap J R) : (u ∘SL v).matrixCoeff.charPowerSeries = (v ∘SL u).matrixCoeff.charPowerSeries

Cyclicity of Fredholm determinants. If u : C₀(J, R) →L[R] C₀(I, R) is row compact and v : C₀(I, R) →L[R] C₀(J, R) is any continuous linear map, the endomorphisms u ∘ v of C₀(I, R) and v ∘ u of C₀(J, R) have the same Fredholm determinant: det (1 - T (u ∘ v)) = det (1 - T (v ∘ u)). If instead v is row compact, apply this to v.

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

Cyclicity of Fredholm determinants for endomorphisms of one model space: det (1 - T (u * v)) = det (1 - T (v * u)) when u is row compact.

theorem ContinuousLinearMap.IsRowCompact.charPowerSeries_matrixCoeff_conj {I : Type u_1} {J : Type u_2} {R : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [NormOneClass R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hu : u.IsRowCompact) (e : ZeroAtInftyContinuousMap I R ≃L[R] ZeroAtInftyContinuousMap J R) : (↑e ∘SL u ∘SL ↑e.symm).matrixCoeff.charPowerSeries = u.matrixCoeff.charPowerSeries

Invariance under conjugation. The Fredholm determinant of a row-compact endomorphism u of C₀(I, R) is unchanged by conjugation e ∘ u ∘ e⁻¹ by a continuous linear equivalence e : C₀(I, R) ≃L[R] C₀(J, R), which need not be an isometry.