Finitely generated modules over Noetherian local ring that become isomorphic after faithfully flat base change Let $(R,\mathfrak m)$ be a Noetherian local ring. Let $S$ be a Noetherian ring which is a faithfully flat $R$-algebra. If $M,N$ are finitely generated $R$-modules such that $M\otimes_R S \cong N \otimes_R S$ (isomorphic as $S$-modules), then is it true that $M\cong N$?
I know this is true when $S=\widehat R$ is the $\mathfrak m$-adic completion of $R$, and in that case it follows from a result of Guralnick which says that if $M/\mathfrak m^n M \cong N/\mathfrak m^n N$ for all $n\gg 0$, then $M\cong N$.
Is the claim indeed true for any Noetherian faithfully flat $R$-algebra?  If this is known, what is a good reference?
 A: For finitely presented modules $M$, $N$ over a ring $R$ the formation of $\text{Hom}_R(M, N)$ commutes with flat base change: for a flat ring map $R \to S$ we have $\text{Hom}_R(M, N) \otimes_R S \to \text{Hom}_S(M \otimes_R S, N \otimes_R S)$ is an isomorphism. See Tag 087R. Of course since $R$ is Noetherian your modules are finitely presented.
Let $R \to S$, $M$, $N$ be as in the question. Consider the map
$$
\text{Hom}_R(M, N) \longrightarrow \text{Hom}_R(M/\mathfrak m M, N/ \mathfrak m N)
$$
We claim it suffices to show image $E$ of this map contains an element which defines an isomorphism between the finite dimensional vector spaces $M/\mathfrak m M$ and $N/\mathfrak m N$. Namely, then by Nakayama we have a surjection $M \to N$. By symmetry there is a surjection $N \to M$. Then a standard trick Tag 05G8 shows that the composition $M \to N \to M$ is an isomorphism and we conclude.
The fact that formation of these modules and the maps between them commutes with base change to $S$, the fact that over $S$ we have an isomorphism between these modules, the fact that $S$ contains a prime lying over $\mathfrak m$ by faithful flatness, shows that, in case the residue field $k = R/\mathfrak m$ is infinite, it suffices to prove the following lemma.
Lemma: Let $K/k$ be an extension of infinite fields. Let $E \subset \text{Hom}_k(V, W)$ be a $k$-subvector space for some finite dimensional $k$-vector spaces $V$ and $W$. If $E \otimes_k K$ contains an isomorphism $V \otimes_k K \to W \otimes_k K$, then $E$ contains an isomorphism $V \to W$.
Proof hint: look at the determinant function.
Remark. If $k$ is finite, then we can still conclude: by the comment of Anonymous we may replace $R$ by a finite flat extension of $R$ to make the residue field large enough and then the argument grosso modo still works.
