English
Equivalence: vanishes trivially for all finite-generated submodules M' of M iff for all FG submodules M' the map rTensor N M'.subtype is injective.
Русский
Эквивалентность: исчезновение тривиально для всех порождаемых FG подмодулей M' тогда и только тогда, когда для всех FG-подмодулей M' отображение rTensor N M'.subtype инъективно.
LaTeX
$$$(\\forall M' : Submodule R M, M'.FG) \\;\\Rightarrow\\; Injective(rTensor N M'.subtype) \\;\\Leftrightarrow\\; (\\text{VanishesTrivially}_R(m, n) \\iff \\sum_i m_i ⊗ n_i = 0)$$$
Lean4
/-- 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. -/
theorem forall_vanishesTrivially_iff_forall_fg_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) (_ : M'.FG), Injective (rTensor N M'.subtype) :=
by
constructor
· intro h M' _
exact rTensor_injective_of_forall_vanishesTrivially R h M'
· intro h k m n hmn
exact vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective R (h _ (fg_span (Set.finite_range _))) hmn
