English
A further refinement with left-submodule inclusion in the map from M to M', giving a finite left-submodule and a suitable image containment.
Русский
Доработанный вариант с включением левого подмодуля в отображение из M в M', обеспечивающий конечность и включение образа.
LaTeX
$$$\exists M', N', M' \le M, N' \le N,\ s \subseteq \mathrm{range}( (inclusion M').rTensor N) $$$
Lean4
/-- For a finite subset `s` of `M ⊗[R] N`, there exists a finitely generated
submodule `M'` of `M`, such that `s` is contained in the image
of `M' ⊗[R] N` in `M ⊗[R] N`. -/
theorem exists_finite_submodule_left_of_setFinite (s : Set (M ⊗[R] N)) (hs : s.Finite) :
∃ M' : Submodule R M, Module.Finite R M' ∧ s ⊆ LinearMap.range (M'.subtype.rTensor N) :=
by
obtain ⟨M', _, hfin, _, h⟩ := exists_finite_submodule_of_setFinite s hs
refine ⟨M', hfin, ?_⟩
rw [mapIncl, ← LinearMap.rTensor_comp_lTensor] at h
exact h.trans (LinearMap.range_comp_le_range _ _)
