Vanishing of elements in a tensor product of two modules #
Let $M$ and $N$ be modules over a commutative ring $R$. Recall that every element of $M \otimes N$
can be written as a finite sum $\sum_{i} m_i \otimes n_i$ of pure tensors
(TensorProduct.exists_finset). We would like to determine under what circumstances such an
expression vanishes.
Let us say that an expression $\sum_{i \in \iota} m_i \otimes n_i$ in $M \otimes N$
vanishes trivially (TensorProduct.VanishesTrivially) if there exist a finite index type
$\kappa$, elements $(y_j)_{j \in \kappa}$ of $N$, and elements
$(a_{ij})_{i \in \iota, j \in \kappa}$ of $R$ such that for all $i$,
$$n_i = \sum_j a_{ij} y_j$$
and for all $j$,
$$\sum_{i} a_{ij} m_i = 0.$$
(The terminology "trivial" comes from Stacks 00HK.)
It is not difficult to show (TensorProduct.sum_tmul_eq_zero_of_vanishesTrivially) that if
$\sum_i m_i \otimes n_i$ vanishes trivially, then it vanishes; that is,
$\sum_i m_i \otimes n_i = 0$.
The equational criterion for vanishing (TensorProduct.vanishesTrivially_iff_sum_tmul_eq_zero),
which appears as
A. Altman and S. Kleiman, A term of commutative algebra (Lemma 8.16),
states that if the elements $m_i$ generate the module $M$, then $\sum_i m_i \otimes n_i = 0$ if and
only if the expression $\sum_i m_i \otimes n_i$ vanishes trivially.
We also prove the following generalization
(TensorProduct.vanishesTrivially_iff_sum_tmul_eq_zero_of_rTensor_injective). If the submodule
$M' \subseteq M$ generated by the $m_i$ satisfies the property that the induced map
$M' \otimes N \to M \otimes N$ is injective, then $\sum_i m_i \otimes n_i = 0$ if and only if the
expression $\sum_i m_i \otimes n_i$ vanishes trivially. (In the case that $M = R$, this yields the
equational criterion for flatness Module.Flat.iff_forall_isTrivialRelation.)
Conversely (TensorProduct.rTensor_injective_of_forall_vanishesTrivially),
suppose that for every equation $\sum_i m_i \otimes n_i = 0$, the expression
$\sum_i m_i \otimes n_i$ vanishes trivially. Then the induced map $M' \otimes N \to M \otimes N$
is injective for every submodule $M' \subseteq M$.
References #
TODO #
- Prove the same theorems with $M$ and $N$ swapped.
- Prove the same theorems with universe polymorphism.
An expression $\sum_i m_i \otimes n_i$ in $M \otimes N$ vanishes trivially if there exist a finite index type $\kappa$, elements $(y_j)_{j \in \kappa}$ of $N$, and elements $(a_{ij})_{i \in \iota, j \in \kappa}$ of $R$ such that for all $i$, $$n_i = \sum_j a_{ij} y_j$$ and for all $j$, $$\sum_{i} a_{ij} m_i = 0.$$ Note that this condition is not symmetric in $M$ and $N$. (The terminology "trivial" comes from Stacks 00HK.)
Equations
Instances For
Equational criterion for vanishing A. Altman and S. Kleiman, A term of commutative algebra (Lemma 8.16), backward direction.
If the expression $\sum_i m_i \otimes n_i$ vanishes trivially, then it vanishes. That is, $\sum_i m_i \otimes n_i = 0$.
Equational criterion for vanishing A. Altman and S. Kleiman, A term of commutative algebra (Lemma 8.16), forward direction.
Assume that the $m_i$ generate $M$. If the expression $\sum_i m_i \otimes n_i$ vanishes, then it vanishes trivially.
Equational criterion for vanishing A. Altman and S. Kleiman, A term of commutative algebra (Lemma 8.16).
Assume that the $m_i$ generate $M$. Then the expression $\sum_i m_i \otimes n_i$ vanishes trivially if and only if it vanishes.
Equational criterion for vanishing A. Altman and S. Kleiman, A term of commutative algebra (Lemma 8.16), forward direction, generalization.
Assume that the submodule $M' \subseteq M$ generated by the $m_i$ satisfies the property that the map $M' \otimes N \to M \otimes N$ is injective. If the expression $\sum_i m_i \otimes n_i$ vanishes, then it vanishes trivially.
Equational criterion for vanishing A. Altman and S. Kleiman, A term of commutative algebra (Lemma 8.16), generalization.
Assume that the submodule $M' \subseteq M$ generated by the $m_i$ satisfies the property that the map $M' \otimes N \to M \otimes N$ is injective. Then the expression $\sum_i m_i \otimes n_i$ vanishes trivially if and only if it vanishes.
Converse of TensorProduct.vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective.
Assume that every expression $\sum_i m_i \otimes n_i$ which vanishes also vanishes trivially. Then, for every submodule $M' \subseteq M$, the map $M' \otimes N \to M \otimes N$ is injective.
Every expression $\sum_i m_i \otimes n_i$ which vanishes also vanishes trivially if and only if for every submodule $M' \subseteq M$, the map $M' \otimes N \to M \otimes N$ is injective.
Every expression $\sum_i m_i \otimes n_i$ which vanishes also vanishes trivially if and only if for every finitely generated submodule $M' \subseteq M$, the map $M' \otimes N \to M \otimes N$ is injective.
If the map $M' \otimes N \to M \otimes N$ is injective for every finitely generated submodule $M' \subseteq M$, then it is in fact injective for every submodule $M' \subseteq M$.