English
If the map M' ⊗ N → M ⊗ N is injective for the submodule M' generated by m_i, then vanishing of ∑ i m_i ⊗ n_i implies vanishing trivially: VanishesTrivially R m n.
Русский
Если отображение M' ⊗ N → M ⊗ N инъективно для подмодуля M' порождаемого m_i, то исчезновение ∑ i m_i ⊗ n_i приводит к исчезновению тривиальному: VanishesTrivially R m n.
LaTeX
$$$ \\text{Injective}(\\, rTensor\\; N\\; M'.subtype\\,) \\Rightarrow (\\sum_i m_i \\otimes n_i = 0 \\Rightarrow \\text{VanishesTrivially}_R(m, n))$$$
Lean4
/-- **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' \subseteq M$ generated by the $m_i$
satisfies the property that the map $M' \otimes N \to M \otimes N$ is injective. If the expression
$\sum_i m_i \otimes n_i$ vanishes, then it vanishes trivially. -/
theorem vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective
(hm : Injective (rTensor N (span R (Set.range m)).subtype)) (hmn : ∑ i, m i ⊗ₜ n i = (0 : M ⊗[R] N)) :
VanishesTrivially R m n := by
-- Restrict `m` on the codomain to $M'$, then apply `vanishesTrivially_of_sum_tmul_eq_zero`.
have mem_M' i : m i ∈ span R (Set.range m) := subset_span ⟨i, rfl⟩
set m' : ι → span R (Set.range m) := Subtype.coind m mem_M' with m'_eq
have hm' : span R (Set.range m') = ⊤ :=
by
apply map_injective_of_injective (injective_subtype (span R (Set.range m)))
rw [Submodule.map_span, Submodule.map_top, range_subtype, coe_subtype, ← Set.range_comp]
rfl
have hm'n : ∑ i, m' i ⊗ₜ n i = (0 : span R (Set.range m) ⊗[R] N) :=
by
apply hm
simp only [m'_eq, map_sum, rTensor_tmul, coe_subtype, Subtype.coind_coe, map_zero, hmn]
have : VanishesTrivially R m' n := vanishesTrivially_of_sum_tmul_eq_zero R hm' hm'n
unfold VanishesTrivially at this ⊢
convert this with κ _ a y j
convert (injective_iff_map_eq_zero' _).mp (injective_subtype (span R (Set.range m))) _
simp [m'_eq]
