Origin and use of an identity of formal power series: $\det(1 - \psi T) = \exp \left(-\sum_{s=1}^{\infty} \text{Tr}(\psi^{s})T^{s}/s\right)$

The following is a historical question, but first some background:

Let $\psi$ be a linear operator from a vector space to itself. The following two expressions, viewed as formal power series, can be shown to be equal (even for an infinite dimensional vector space):

$$ \det(1 - \psi T) = \exp \left(-\sum_{s=1}^{\infty} \text{Tr}(\psi^{s})T^{s}/s\right) $$

Here is a simple example using the associated matrix in the finite dimensional case:

For more on this topic (and how to ensure the definitions make sense for infinite dimensional vector spaces) see: N. Koblitz, p-adic Numbers, p-adic Analysis, and Zeta-Functions, Springer-Verlag, New York, 1984.

In particular, see Koblitz's book for how ($p$-adic versions of) this identity can be used in Bernard Dwork's proof of the rationality of the zeta function (resolving the first of the Weil Conjectures).

I would welcome any insight as to how one thinks up, observes, or conjectures such an identity in the first place, but my question is: what is the origin of this identity and where else has it appeared (perhaps in a somewhat modified form)?

Using $\det\exp=\exp\mathrm{tr}$, we have $$ \det(I-tA) = \det \exp\log(I-tA) = \exp\mathrm{tr}\log(I-tA) $$ and as $$ \log(I-tA) = -\sum_{k\ge1} \frac1k t^k A^k, $$ we have $$ \exp\mathrm{tr}\log(I-tA) = \exp\left( -\sum_{k\ge1} \frac1k t^k \mathrm{tr}(A^k)\right) $$ This shows that your identity is a form of the $\det\exp$ identity.

The question about the origins is interesting and I do not have much to say (which was why I restricted myself to a comment in the first place). For complex matrices it is very easy to prove that $\det\exp(A)=\exp\mathrm{tr}(A)$, which might explain why I have never seen a name attached to it.

I have seen it used in connection with Lie groups (to prove that sl is the Lie algebra of SL), and (in forms like what you stated) in work on enumeration.

The development of this operator identity can be traced back till the very beginning of the 20th century.

I think the paper On the numerical evaluation of Fredholm determinants from Folkmar Bornemann (2008) could be useful for you. Bornemann presents in Section 3: Definition and Properties of Fredholm and Operator Determinants of this paper four different representations of your stated operator identity. He writes:

For a trace class operator $A \in \mathcal{J}_1(\mathcal{H})$ there are several equivalent constructions that all define one and the same entire function \begin{align*} d(z)=\text{det}(I+zA)\qquad(z\in\mathbb{R}) \end{align*} in fact, each construction has been chosen at least once, in different places of the literature, as the basic definition of the operator determinant:

$1.)$ Gohberg and Krein ($1969$, p. $157$) define the determinant by the locally uniformly convergent (infinite) product \begin{align*} \text{det}(I+zA)=\prod_{n=1}^{N(A)}(1+z\lambda_n(A)) \end{align*} which possesses zeros exactly at $z_n=-1/\lambda_n(A)$, counting multiplicity.

$2.)$ Gohberg et al. ($1990$, p. $115$) define the determinant as follows. Given any sequence of finite rank operators $A_n$ with $A_n\rightarrow A$ converging in trace class norm, the sequence of finite dimensional determinants \begin{align*} \text{det}\left(I+zA_n\upharpoonright_{\text{ran}(A_n)}\right) \end{align*} (which are polynomials in z) converges locally uniform to $\text{det}(I+zA)$, independently of the choice of the sequence $A_n$. The existence of at least one such sequence follows from the singular value representation at $(2.1)$.

$3.)$ Dunford and Schwartz ($1963$, p. $1029$) define the determinant by what is often called Plemelj’s formula \begin{align*} \text{det}(I+zA)=\exp(\text{tr}\ \text{log}(I+zA))=\exp\left(-\sum_{n=1}^{\infty}\frac{(-z)^n}{n}\text{tr}A^n\right) \end{align*} which converges for $|z|<1/|\lambda_1(A)|$ and can analytically be continued as an entire function to all $z\in\mathbb{C}$.

$4.)$ Grothendieck ($1956$, p. $347$) and Simon ($1977$, p. $254$) define the determinant most elegantly with a little exterior algebra (Greub $1967$). With $\bigwedge^n(A)\in\mathcal(J)_1\left(\bigwedge^n(\mathcal{H})\right)$ being the $n^\text{th}$ exterior product of $A$, the power series \begin{align*} \text{det}(I+zA)=\sum_{n=0}^{\infty}z^n\text{tr}\bigwedge^n(A) \end{align*} converges for all $z\in\mathbb{C}$. Note that $\text{tr}\bigwedge^{n}(A)=\sum_{i_1<\cdots<i_n}\lambda_{i_1}(A)\cdots\lambda_{i_n}(A)$ is just the $n^\text{th}$ symmetric function of the eigenvalues of $A$.

Proofs of the equivalence can be found in (Gohberg et al. $2000$, Chap. $2$) and (Simon $2005$, Chap. $3$).

In a footnote for $3.)$ above, Bornemann provides additional information to the Plemelj Formula, namely:

Plemelj ($1904$, Eq. $(62)$) had given a corresponding form of the Fredholm determinant for integral operators. However, it can already be found in Fredholm ($1903$, p. $384$).

So, the formula seems to go back till Fredholm $1903$. I suppose according to some references I've found, it's the following paper: I. Fredholm, Sur une classe d`équation fonctionelle, Acta Math. $27, 365-390 (1903)$.