English
Equivalence: vanishes trivially for all sums iff for every submodule M', the map rTensor N M'.subtype is injective.
Русский
Эквивалентность: исчезновение тривиально для всех сумм эквивалентно тому, что для каждого подмодуля M' отображение rTensor N M'.subtype является инъективным.
LaTeX
$$$(\\forall l, m, n,\n \\sum_i m_i \\otimes n_i = 0 \\Rightarrow \\text{VanishesTrivially}_R(m, n)) \\iff \\forall M', Injective(rTensor N M'.subtype)$$$
Lean4
/-- 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. -/
theorem forall_vanishesTrivially_iff_forall_rTensor_injective :
(∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ n i = (0 : M ⊗[R] N) → VanishesTrivially R m n) ↔
∀ M' : Submodule R M, Injective (rTensor N M'.subtype) :=
by
constructor
· intro h
exact rTensor_injective_of_forall_vanishesTrivially R h
· intro h k m n hmn
exact vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective R (h _) hmn
