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)][altman2021term], 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^{\prime }\subseteq M$ generated by the $m_i$ satisfies the property that the induced map $M^{\prime }\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^{\prime }\otimes N\to M\otimes N$ is injective for every submodule $M^{\prime }\subseteq M$.

References

• [A. Altman and S. Kleiman, A term of commutative algebra (Lemma 8.16)][altman2021term]

TODO

• Prove the same theorems with $M$ and $N$ swapped.
• Prove the same theorems with universe polymorphism.

@[reducible, inline]

abbrev TensorProduct.VanishesTrivially (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] {ι : Type u} [Fintype ι] (m : ι → M) (n : ι → N) : Prop

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

• TensorProduct.VanishesTrivially R m n = ∃ (κ : Type ?u.78) (x : Fintype κ) (a : ι → κ → R) (y : κ → N), (∀ (i : ι), n i = ∑ j : κ, a i j • y j) ∧ ∀ (j : κ), ∑ i : ι, a i j • m i = 0

theorem TensorProduct.sum_tmul_eq_zero_of_vanishesTrivially (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] {ι : Type u} [Fintype ι] {m : ι → M} {n : ι → N} (hmn : TensorProduct.VanishesTrivially R m n) : ∑ i : ι, m i ⊗ₜ[R] n i = 0

Equational criterion for vanishing [A. Altman and S. Kleiman, A term of commutative algebra (Lemma 8.16)][altman2021term], 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$.

theorem TensorProduct.vanishesTrivially_of_sum_tmul_eq_zero (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] {ι : Type u} [Fintype ι] {m : ι → M} {n : ι → N} (hm : Submodule.span R (Set.range m) = ⊤) (hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0) : TensorProduct.VanishesTrivially R m n

Equational criterion for vanishing [A. Altman and S. Kleiman, A term of commutative algebra (Lemma 8.16)][altman2021term], forward direction.

Assume that the $m_i$ generate $M$. If the expression $\sum _i{m}_i\otimes n_i$ vanishes, then it vanishes trivially.

theorem TensorProduct.vanishesTrivially_iff_sum_tmul_eq_zero (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] {ι : Type u} [Fintype ι] {m : ι → M} {n : ι → N} (hm : Submodule.span R (Set.range m) = ⊤) : TensorProduct.VanishesTrivially R m n ↔ ∑ i : ι, m i ⊗ₜ[R] n i = 0

Equational criterion for vanishing [A. Altman and S. Kleiman, A term of commutative algebra (Lemma 8.16)][altman2021term].

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.

theorem TensorProduct.vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] {ι : Type u} [Fintype ι] {m : ι → M} {n : ι → N} (hm : Function.Injective ⇑(LinearMap.rTensor N (Submodule.span R (Set.range m)).subtype)) (hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0) : TensorProduct.VanishesTrivially R m n

Equational criterion for vanishing [A. Altman and S. Kleiman, A term of commutative algebra (Lemma 8.16)][altman2021term], forward direction, generalization.

Assume that the submodule $M^{\prime }\subseteq M$ generated by the $m_i$ satisfies the property that the map $M^{\prime }\otimes N\to M\otimes N$ is injective. If the expression $\sum _i{m}_i\otimes n_i$ vanishes, then it vanishes trivially.

theorem TensorProduct.vanishesTrivially_iff_sum_tmul_eq_zero_of_rTensor_injective (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] {ι : Type u} [Fintype ι] {m : ι → M} {n : ι → N} (hm : Function.Injective ⇑(LinearMap.rTensor N (Submodule.span R (Set.range m)).subtype)) : TensorProduct.VanishesTrivially R m n ↔ ∑ i : ι, m i ⊗ₜ[R] n i = 0

Equational criterion for vanishing [A. Altman and S. Kleiman, A term of commutative algebra (Lemma 8.16)][altman2021term], generalization.

Assume that the submodule $M^{\prime }\subseteq M$ generated by the $m_i$ satisfies the property that the map $M^{\prime }\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.

theorem TensorProduct.rTensor_injective_of_forall_vanishesTrivially (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] (hMN : ∀ {ι : Type u} [inst : Fintype ι] {m : ι → M} {n : ι → N}, ∑ i : ι, m i ⊗ₜ[R] n i = 0 → TensorProduct.VanishesTrivially R m n) (M' : Submodule R M) : Function.Injective ⇑(LinearMap.rTensor N M'.subtype)

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^{\prime }\subseteq M$, the map $M^{\prime }\otimes N\to M\otimes N$ is injective.

theorem TensorProduct.forall_vanishesTrivially_iff_forall_rTensor_injective (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] : (∀ {ι : Type u} [inst : Fintype ι] {m : ι → M} {n : ι → N}, ∑ i : ι, m i ⊗ₜ[R] n i = 0 → TensorProduct.VanishesTrivially R m n) ↔ ∀ (M' : Submodule R M), Function.Injective ⇑(LinearMap.rTensor N M'.subtype)

Every expression $\sum _i{m}_i\otimes n_i$ which vanishes also vanishes trivially if and only if for every submodule $M^{\prime }\subseteq M$, the map $M^{\prime }\otimes N\to M\otimes N$ is injective.

theorem TensorProduct.forall_vanishesTrivially_iff_forall_FG_rTensor_injective (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] : (∀ {ι : Type u} [inst : Fintype ι] {m : ι → M} {n : ι → N}, ∑ i : ι, m i ⊗ₜ[R] n i = 0 → TensorProduct.VanishesTrivially R m n) ↔ ∀ (M' : Submodule R M), M'.FG → Function.Injective ⇑(LinearMap.rTensor N M'.subtype)

Every expression $\sum _i{m}_i\otimes n_i$ which vanishes also vanishes trivially if and only if for every finitely generated submodule $M^{\prime }\subseteq M$, the map $M^{\prime }\otimes N\to M\otimes N$ is injective.

theorem TensorProduct.rTensor_injective_of_forall_FG_rTensor_injective (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] (hMN : ∀ (M' : Submodule R M), M'.FG → Function.Injective ⇑(LinearMap.rTensor N M'.subtype)) (M' : Submodule R M) : Function.Injective ⇑(LinearMap.rTensor N M'.subtype)

If the map $M^{\prime }\otimes N\to M\otimes N$ is injective for every finitely generated submodule $M^{\prime }\subseteq M$, then it is in fact injective for every submodule $M^{\prime }\subseteq M$.