Tensor product of linearly independent families

Stream: mathlib4

[Andrew Yang]

When is the tensor product of linearly independent families linearly independent?
This is not always true, and essentially you are asking $P \otimes M \to N \otimes M$ to be injective if $P \to N$ is injective and $P$ is free.

Let’s call such $M$ good modules (if $P \otimes M \hookrightarrow N \otimes M$ for all $N$ and all free $P \subseteq N$). Is there a better characterization of them? Here are some facts I know about them:

1. Flat modules are good.
2. Submodules of good modules are good.
3. (Potentially infinite) direct product of good modules are good. (Because $P \otimes \prod_i M_i \hookrightarrow \prod_i P \otimes M_i$)
4. Good modules are torsion free. (By looking at $(a) \subseteq R$ for $a \in R^0$)

5. Over integral domains, torsion free modules are good (Because $M \hookrightarrow k \otimes_R M$ with $k = \mathrm{Frac}(R)$ and $k \otimes_R M$ is $k$-flat).

6. There are torsion free modules that are not good. Take $k$ a field, $R = k[x, y]/(x^2, xy, y^2)$ and $M = k^5$ with $x$ acting on it via $\left(\begin{smallmatrix}0&0&0&0&0\\0&0&0&0&0\\0&0&0&0&0\\0&1&0&0&0\\0&0&1&0&0\end{smallmatrix}\right)$ and $y$ via $\left(\begin{smallmatrix}0&0&0&0&0\\0&0&0&0&0\\0&0&0&0&0\\1&0&0&0&0\\0&1&0&0&0\end{smallmatrix}\right)$. Then $M$ is torsion free, $R \xrightarrow{\cdot e_2} M$ is injective, but $M \xrightarrow{\cdot \otimes e_2} M \otimes M$ is not injective because $e_4 \otimes e_2 = ye_1 \otimes e_2 = e_1 \otimes ye_2 = e_1 \otimes xe_3 = xe_1 \otimes e_3 = 0$. (Example taken from here)

[Paul Lezeau]

I have a proof that torsionless modules work for taking tensor products of linearly independent families #24219