English
If the submodule generated by m_i spans M, and the sum ∑ i m_i ⊗ n_i equals zero, then the pair (m, n) vanishes trivially: VanishesTrivially R m n.
Русский
Если подмодуль, порождённый m_i, покрывает M, и сумма ∑ i m_i ⊗ n_i равна нулю, то пара (m, n) исчезает тривиально: VanishesTrivially R m n.
LaTeX
$$$ (\\operatorname{span}_R \\{ m_i \\}) = M \\quad\\text{and}\\quad \\sum_i m_i \\otimes n_i = 0 \\quad\\Rightarrow\\quad \\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.
Assume that the $m_i$ generate $M$. If the expression $\sum_i m_i \otimes n_i$
vanishes, then it vanishes trivially. -/
theorem vanishesTrivially_of_sum_tmul_eq_zero (hm : Submodule.span R (Set.range m) = ⊤)
(hmn : ∑ i, m i ⊗ₜ n i = (0 : M ⊗[R] N)) : VanishesTrivially R m n := by
-- Define a map $G \colon R^\iota \to M$ whose matrix entries are the $m_i$. It is surjective.
set G : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R m with hG
have G_basis_eq (i : ι) : G (Finsupp.single i 1) = m i := by simp [hG]
have G_surjective : Surjective G := by
apply LinearMap.range_eq_top.mp
apply top_le_iff.mp
rw [← hm]
apply Submodule.span_le.mpr
rintro _ ⟨i, rfl⟩
use Finsupp.single i 1, G_basis_eq i
set en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ n i with hen
have en_mem_ker : en ∈ ker (rTensor N G) := by
simp [hen, G_basis_eq, hmn]
-- We have an exact sequence $\ker G \to R^\iota \to M \to 0$.
have exact_ker_subtype : Exact (ker G).subtype G := G.exact_subtype_ker_map
have exact_rTensor_ker_subtype : Exact (rTensor N (ker G).subtype) (rTensor N G) :=
rTensor_exact (M := ↥(ker G)) N exact_ker_subtype G_surjective
have en_mem_range : en ∈ range (rTensor N (ker G).subtype) := exact_rTensor_ker_subtype.linearMap_ker_eq ▸ en_mem_ker
obtain ⟨kn, hkn⟩ := en_mem_range
obtain ⟨ma, rfl : kn = ∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2⟩ := exists_finset kn
refine .of_fintype (κ := ma) (fun i ⟨⟨kj, _⟩, _⟩ ↦ (kj : ι →₀ R) i) (fun ⟨⟨_, yj⟩, _⟩ ↦ yj) ?_ ?_
· intro i
classical
apply_fun finsuppScalarLeft R N ι at hkn
apply_fun (· i) at hkn
symm at hkn
simp only [map_sum, finsuppScalarLeft_apply_tmul, zero_smul, Finsupp.single_zero, Finsupp.sum_single_index,
one_smul, Finsupp.finset_sum_apply, Finsupp.single_apply, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte,
rTensor_tmul, coe_subtype, Finsupp.sum_apply, Finsupp.sum_ite_eq', Finsupp.mem_support_iff, ne_eq, ite_not,
en] at hkn
simp only [Finset.univ_eq_attach, Finset.sum_attach ma (fun x ↦ (x.1 : ι →₀ R) i • x.2)]
convert hkn using 2 with x _
split
· next h'x => rw [h'x, zero_smul]
· rfl
· rintro ⟨⟨⟨k, hk⟩, _⟩, _⟩
simpa only [hG, linearCombination_apply, zero_smul, implies_true, Finsupp.sum_fintype] using mem_ker.mp hk
