The Stacks project

There is a stronger if and only if version in MatCRT, p.177.

If $t : M \to M$ is injective then flatness of $M/tM$ over $A$ implies that $t : M \to M$ is $A$-universally flat by Lemma 10.39.12 so the other direction is true without any hypotheses on the ring map $A \to B$ and the module $M$ (in the sense that $t : M \otimes_A A' \to M \otimes_A A'$ is injective for absolutely any $A$-algebra $A'$ including residue fields).

The result of MatCRT you are referring too is probably Theorem 22.5. This is the same as Lemma 10.99.1 modulo the fact that it only states and proves the difficult direction (again the other direction follows immediately from Lemma 10.39.12).

If you have a ring map $A \to B$, an element $t \in B$ and a $B$-module $M$, then to show that $t : M \to M$ is injective and $M/tM$ flat over $A$, it suffices to do this after localization at all maximal ideals of $B$. Thus the problem always immediately reduces to the local case (this is just what Matsumura says in the proof of Theorem 22.6 on page 177).

The statement in the local case has a number of variants in the Stacks project: for example, we have 10.99.1, 10.99.2, 10.128.4, 10.128.5, 37.18.1, 41.9.2, 38.7.2, 38.7.5, and finally all of More on Flatness, Section 38.25 is about variants of this lemma and contains the strongest possible version one could ever imagine (I think).

In many of these lemmas (not all) we could make the statement an equivalence. Hmm... Do others agree this is a good idea?