English
Assume the R-algebra map r ↦ ϕ(r) ∈ S is surjective. Then the canonical map M → S ⊗_R M given by m ↦ 1 ⊗ m is surjective; equivalently, every element of S ⊗_R M can be written as 1 ⊗ m for some m ∈ M.
Русский
Пусть отображение алгебра-маркировки R → S является сюръективным. Тогда каноническое отображение M → S ⊗_R M, заданное m ↦ 1 ⊗ m, сюръективно; то есть каждый элемент S ⊗_R M имеет вид 1 ⊗ m для некоторого m ∈ M.
LaTeX
$$$\\text{Suppose } \\operatorname{algebraMap}_R^S:\\ R\\to S \\text{ is surjective. Then the map }\\varphi:M\\to S\\otimes_R M,\\; \\varphi(m)=1\\otimes m,\\; \\text{is surjective.}$$$$
Lean4
theorem mk_surjective (h : Function.Surjective (algebraMap R S)) : Function.Surjective (TensorProduct.mk R S M 1) :=
by
rw [← LinearMap.range_eq_top, ← top_le_iff, ← span_tmul_eq_top, Submodule.span_le]
rintro _ ⟨x, y, rfl⟩
obtain ⟨x, rfl⟩ := h x
rw [Algebra.algebraMap_eq_smul_one, smul_tmul]
exact ⟨x • y, rfl⟩
