Characteristic polynomials of matrix polynomials and exterior powers Suppose we know that the generic matrix $(x_{ij})$ is diagonalizable over a commutative ring containing $\mathbb Z[x_{11},\dots ,x_{nn}]$.
How can one deduce the following facts?

*

*Suppose $A,B\in \mathrm M_n(R)$ have the same characteristic polynomial. Then for any $f\in R[x]$, so do $f(A),f(B)$.

*Suppose the characteristic polynomial of $A\in \mathrm M_n(R)$ splits over an extension $R_1\supset R$ as $\chi_A=\prod_{i=1}^n(x-\lambda _i)$. Then for any $f\in R[x]$ we have $\chi_{f(A)}=\prod_{i=1}^n(x-f(\lambda _i))$.

5.4, 5.5 in the constructive commutative algebra book by Lombardi & Quitte outline an argument, but I am not able to follow it.
 A: Consider the generic degree $n$ polynomial $\omega = \sum_{i=0}^n t_ix^i\in \mathbb Z[t_0,\dots ,t_n,x]$. The expression on the right below is symmetric in $x_1,\dots ,x_n$, whence there is a unique $\Omega \in \mathbb Z[t_0,\dots ,t_n,x_1,\dots ,x_n]$ satisfying $$\Omega(t_0,\dots,t_n,s_1(x_{1..n}),\dots,s_n(x_{1..n}))=\prod_{i=1}^n\omega(x_i).$$
Theorem. Let $\chi_A=x^n+\sum_{i=0}^{n-1}c_ix^i\in \mathbb Z[x_{11},\dots,x_{nn}][x]$ be the characteristic polynomial of the generic matrix. We have the following equality in $\mathbb Z[t_0,\dots ,t_n,x_{11},\dots,x_{nn}]$.
$$\det\omega(A)=\det(A^n+\sum_{i=0}^{n-1}t_iA^i)=\Omega(t_0,\dots ,t_n,-c_{n-1},\dots,(-1)^nc_0).$$
Proof. Pass to an extension over which $\chi_A$ is split separable with roots $\lambda_1,\dots ,\lambda_n$ and $A$ is diagonalizable. By calculation in this extension $\det \omega(A)=\prod_{i=1}^n\omega(\lambda_i)$. Specializing $x_1,\dots ,x_n$ to $\lambda_1,\dots ,\lambda_n$ gives the same result for the RHS. Hence the equation holds in the extension, whence it holds in the asserted ring.
Corollary. Let $A\in \mathrm M_n(R)$. Suppose $\chi_A=\prod_{i=1}^n(x-\lambda_i)$ in an extension $R\subset R_1$. For every $f\in R[x]$ we have $\det f(A)=\prod_{i=1}^nf(\lambda_i)$.
Algebraic spectral mapping theorem. Invoke the corollary for $R[x]$ and the polynomial $x-f(y)\in R[x,y]$.
