English
If every sum ∑ i m_i ⊗ n_i that vanishes also vanishes trivially, then for any submodule M' of M, the map M' ⊗ N → M ⊗ N is injective.
Русский
Если каждое исчезновение сумма ∑ i m_i ⊗ n_i, которое равно нулю, исчезает тривиально, то для любого подмодуля M' модуля M отображение M' ⊗ N → M ⊗ N инъективно.
LaTeX
$$$ (\\forall l, m, n,\n \\sum_i m_i \\otimes n_i = 0 \\Rightarrow \\text{VanishesTrivially}_R(m, n)) \;\Rightarrow\; \\forall M' \\subseteq M,\; Injective(rTensor\\; N\\; M'.subtype) $$$
Lean4
/-- 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. -/
theorem rTensor_injective_of_forall_vanishesTrivially
(hMN : ∀ {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
apply (injective_iff_map_eq_zero _).mpr
rintro x hx
obtain ⟨s, rfl⟩ := exists_finset x
rw [← Finset.sum_attach]
apply sum_tmul_eq_zero_of_vanishesTrivially
simp only [map_sum, rTensor_tmul, coe_subtype] at hx
have e := (Fintype.equivFin s).symm
rw [← Finset.sum_coe_sort, ← e.sum_comp] at hx
have := hMN hx
rw [← e.vanishesTrivially_comp]
unfold VanishesTrivially at this ⊢
convert this
symm
convert (injective_iff_map_eq_zero' _).mp (injective_subtype M') _
simp
