Matrix coefficients transfer along a ring hom fixing the base, and vanish together

Transfer of matrix coefficients along a ring homomorphism, and the equivalence it gives.

Let $K \subseteq \mathbb{C}$ be a subfield and let $\Phi : \mathbb{C} \to \mathbb{C}$ be a ring homomorphism fixing $K$ pointwise. Let $M$ be a complex matrix, indexed by arbitrary finite sets, and let $w$, $v$ be vectors with entries in $K$. Writing $\Phi(M)$ for $\Phi$ applied entrywise,

and consequently

Proof. Apply $\Phi$ to $\sum_{i,j} w_i M_{ij} v_j$: it preserves finite sums and products and fixes each $w_i$ and $v_j$. The equivalence follows because $\Phi$ is injective — its kernel is an ideal of the field $\mathbb{C}$ not containing $1$, hence zero.

What is new here relative to the existing node. Diaz.coeff_transfer already carries the forward identity, over an arbitrary subfield $K$, for index types $\mathrm{Fin}\,m$ and $\mathrm{Fin}\,n$. It does not carry the corollary's "consequently" clause. That clause is the half that uses injectivity, and it is the half the intended application needs: one wants to conclude that a coefficient fails to vanish downstream from its failing to vanish upstream, which the identity alone does not give. This node states the corollary in full, and takes the index types to be arbitrary finite types rather than $\mathrm{Fin}\,m$, $\mathrm{Fin}\,n$: $w^{\mathsf T} M v$ is a finite double sum, so finiteness of the index sets is what the expression means rather than an extra hypothesis, and there is no reason to force a caller through a numbering of the index set.

Hypotheses. None beyond the note's. $M$ is an arbitrary complex matrix; only the coefficient vectors are constrained to lie in $K$; $\Phi$ is only assumed to be a ring homomorphism fixing $K$ — not surjective, not continuous, not conjugation-equivariant.

Attribution. The statement is Carlo Perassi's, Corollary 7 (cor:transfer) of a note predating this mission. No novelty is claimed for the mathematics, which is elementary; the contribution is the formalisation.