English
Let hm be the injectivity condition on rTensor. Then VanishesTrivially R m n holds if and only if ∑ i m_i ⊗ n_i = 0.
Русский
Пусть hm задаёт инъективность rTensor. Тогда VanishesTrivially R m n выполняется тогда и только тогда, когда ∑ i m_i ⊗ n_i = 0.
LaTeX
$$$ \\text{Injective}(rTensor\\; N\\; (\\operatorname{span} R (\\{m_i\\})).subtype) \\;\n\\Longrightarrow\\; (\\text{VanishesTrivially}_R(m, n) \\iff \\sum_i m_i \\otimes n_i = 0)$$$
Lean4
/-- **Equational criterion for vanishing**
[A. Altman and S. Kleiman, *A term of commutative algebra* (Lemma 8.16)][altman2021term],
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. -/
theorem vanishesTrivially_iff_sum_tmul_eq_zero_of_rTensor_injective
(hm : Injective (rTensor N (span R (Set.range m)).subtype)) :
VanishesTrivially R m n ↔ ∑ i, m i ⊗ₜ n i = (0 : M ⊗[R] N) :=
⟨sum_tmul_eq_zero_of_vanishesTrivially R, vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective R hm⟩
