The Fredholm determinant of a row-compact operator

Let R be a complete ultrametric normed commutative ring with ‖1‖ = 1, and I a discrete index type. For an endomorphism u of the model space C₀(I, R), the Fredholm series H_u(T) = det (1 - T u) is the principal-minor series u.matrixCoeff.charPowerSeries of its matrix, and the Fredholm determinant det (1 - u) is its value H_u(1) at T = 1 (ContinuousLinearMap.fredholmDet). For row-compact u the series is entire, so this value is a genuine convergent sum, and the value of H_u at any scalar a is the Fredholm determinant of a • u (ContinuousLinearMap.IsRowCompact.fredholmDet_smul).

The main result is the multiplicativity of the Fredholm determinant over ultrametric Tate scalars: for row-compact u and v, which need not commute,

det (1 - (u + v - u v)) = det (1 - u) det (1 - v) (ContinuousLinearMap.IsRowCompact.fredholmDet_add_sub_mul),

since 1 - (u + v - u v) = (1 - u) (1 - v). The proof truncates u and v to a finite set S of output coordinates. The truncated identity is the finite determinant identity det ((1 - A) (1 - B)) = det (1 - A) det (1 - B) for the blocks of u and v on S (ContinuousLinearMap.fredholmDet_indicatorCLM_comp). The truncations converge in operator norm and share a null row majorant, so their Fredholm determinants converge (ContinuousLinearMap.tendsto_fredholmDet_of_tendsto).

Consequently, if 1 - a • u is invertible in the algebra of continuous endomorphisms then H_u(a) is a unit of R (ContinuousLinearMap.IsRowCompact.isUnit_evalAt_charPowerSeries_of_isUnit_one_sub_smul): the inverse is 1 - w for a row-compact w, and det (1 - a u) det (1 - w) = det 1 = 1. Over coefficient rings with nilpotents this is a statement about units, not only about nonvanishing.

Main definitions

• ContinuousLinearMap.fredholmDet: the Fredholm determinant det (1 - u) = H_u(1).

Main results

• ContinuousLinearMap.fredholmDet_eq_det: on a finite index type, det (1 - u) is the determinant of 1 minus the matrix of u.
• ContinuousLinearMap.tendsto_fredholmDet_of_tendsto: continuity of the Fredholm determinant in operator norm along families with a common null row majorant.
• ContinuousLinearMap.IsRowCompact.fredholmDet_add_sub_mul: multiplicativity.
• ContinuousLinearMap.IsRowCompact.isUnit_fredholmDet_of_isUnit_one_sub and ContinuousLinearMap.IsRowCompact.isUnit_evalAt_charPowerSeries_of_isUnit_one_sub_smul: an invertible 1 - a • u has a unit Fredholm determinant.

References

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

noncomputable def ContinuousLinearMap.fredholmDet {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [NormedCommRing R] (u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R) : R

The Fredholm determinant det (1 - u) of an endomorphism u of the model space C₀(I, R): the value at T = 1 of its Fredholm series det (1 - T u), the principal-minor series of its matrix. When u is row compact over a complete ultrametric ring with ‖1‖ = 1 the series is entire (Matrix.isRestricted_charPowerSeries), so this value is a convergent sum.

theorem ContinuousLinearMap.fredholmDet_def {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [NormedCommRing R] (u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R) : u.fredholmDet = u.matrixCoeff.charPowerSeries.evalAt 1

@[simp]

theorem ContinuousLinearMap.fredholmDet_zero {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [NormedCommRing R] : fredholmDet 0 = 1

The Fredholm determinant of the zero operator is det 1 = 1.

theorem ContinuousLinearMap.fredholmDet_eq_det {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [NormedCommRing R] [Fintype I] (u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R) : u.fredholmDet = (1 - u.matrixCoeff).det

Finite matrix comparison. On a finite index type, the Fredholm determinant is the determinant of 1 minus the matrix.

theorem ContinuousLinearMap.fredholmDet_indicatorCLM_comp {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [NormedCommRing R] (S : Finset I) (u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R) : (ZeroAtInftyContinuousMap.indicatorCLM R ↑S ∘SL u).fredholmDet = (1 - u.matrixCoeff.submatrix Subtype.val Subtype.val).det

The Fredholm determinant of the output truncation π_S ∘ u to a finite set S is det (1 - A) for the finite block A of the matrix of u on S.

theorem ContinuousLinearMap.IsRowCompact.fredholmDet_smul {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] [NormOneClass R] {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hu : u.IsRowCompact) (a : R) : (a • u).fredholmDet = u.matrixCoeff.charPowerSeries.evalAt a

The Fredholm series at a scalar. For row-compact u and any a : R, the value H_u(a) of the Fredholm series of u is the Fredholm determinant of a • u.

theorem ContinuousLinearMap.tendsto_fredholmDet_of_tendsto {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] {α : Type u_3} {l : Filter α} {w : α → ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} {w₀ : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} {r : I → ℝ} (hr : Filter.Tendsto r Filter.cofinite (nhds 0)) (hw : ∀ (a : α) (i j : I), ‖(w a).matrixCoeff i j‖ ≤ r i) (h : Filter.Tendsto (fun (a : α) => ‖w a - w₀‖) l (nhds 0)) : Filter.Tendsto (fun (a : α) => (w a).fredholmDet) l (nhds w₀.fredholmDet)

Continuity of the Fredholm determinant. If endomorphisms w a of C₀(I, R) converge in operator norm to w₀, and all of them have entries bounded by a common null row majorant r, then their Fredholm determinants converge to that of w₀.

theorem ContinuousLinearMap.IsRowCompact.fredholmDet_add_sub_mul {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] {u v : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hu : u.IsRowCompact) (hv : v.IsRowCompact) : (u + v - u * v).fredholmDet = u.fredholmDet * v.fredholmDet

Multiplicativity of the Fredholm determinant. For row-compact endomorphisms u and v of C₀(I, R), which need not commute, det (1 - (u + v - u v)) = det (1 - u) det (1 - v), reflecting 1 - (u + v - u v) = (1 - u) (1 - v).

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

If 1 - u is invertible in the algebra of continuous endomorphisms of C₀(I, R) for a row-compact u, the Fredholm determinant det (1 - u) is a unit of R.

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

Invertibility forces a unit determinant. If u is row compact and 1 - a • u is invertible in the algebra of continuous endomorphisms of C₀(I, R), then the value H_u(a) of the Fredholm series of u is a unit of R.