English
The tmul in directLimitLeft evaluated at the image of g under the i-th inclusion matches the corresponding directLimit element for g ⊗ m.
Русский
Значение tmul в directLimitLeft, взятое на образе g под включением i-й компоненты, совпадает с элементом directLimit для g ⊗ m.
LaTeX
$$$\mathrm{directLimitLeft}\; f\; M\ (\mathrm{in}_i(g) \otimes m) = \mathrm{in}_i(f_i g) \otimes m$$$
Lean4
/-- For any element `x` of `M ⊗[R] N`, there exists a finite subset `{ (m_i, n_i) }`
of `M × N` such that each `m_i` is distinct (we represent it as an element of `M →₀ N`),
such that `x` is equal to the sum of `m_i ⊗ₜ[R] n_i`. -/
theorem exists_finsupp_left (x : M ⊗[R] N) : ∃ S : M →₀ N, x = S.sum fun m n ↦ m ⊗ₜ[R] n := by
induction x with
| zero => exact ⟨0, by simp⟩
| tmul x y => exact ⟨Finsupp.single x y, by simp⟩
| add x y hx hy =>
obtain ⟨Sx, hx⟩ := hx
obtain ⟨Sy, hy⟩ := hy
use Sx + Sy
rw [hx, hy]
exact (Finsupp.sum_add_index' (by simp) TensorProduct.tmul_add).symm
