English
For a finite subset of a tensor product, there exist finite submodules M' ⊆ M and N' ⊆ N such that the subset lies in the image of M' ⊗ N' in M ⊗ N.
Русский
Для конечного подзадача тензорного произведения существуют конечные подмодули M' ⊆ M и N' ⊆ N, так что множество содержится в образе M' ⊗ N' в M ⊗ N.
LaTeX
$$$\exists M'\le M, N'\le N,\ Module.Finite\ M',\ Module.Finite\ N',\ s \subseteq LinearMap.range (TensorProduct.map (inclusion\ M' ) (inclusion \ N'))$$$
Lean4
/-- For any element `x` of `M ⊗[R] N`, there exists a finite subset `{ (m_i, n_i) }`
of `M × N` such that each `n_i` is distinct (we represent it as an element of `N →₀ M`),
such that `x` is equal to the sum of `m_i ⊗ₜ[R] n_i`. -/
theorem exists_finsupp_right (x : M ⊗[R] N) : ∃ S : N →₀ M, x = S.sum fun n m ↦ m ⊗ₜ[R] n :=
by
obtain ⟨S, h⟩ := exists_finsupp_left (TensorProduct.comm R M N x)
refine ⟨S, (TensorProduct.comm R M N).injective ?_⟩
simp_rw [h, Finsupp.sum, map_sum, comm_tmul]
