English
If the algebra map R → T is surjective, then the flipped canonical map (TensorProduct.mk R S T).flip 1: T → S ⊗_R T is surjective; i.e., every element of S ⊗_R T can be expressed as t ⊗ 1 for some t ∈ T.
Русский
Если отображение алгебраного отображения R → T сюръективно, то перевёрнутое каноническое отображение (TensorProduct.mk R S T).flip 1: T → S ⊗_R T сюръективно; каждый элемент S ⊗_R T записывается как t ⊗ 1 для некоторого t ∈ T.
LaTeX
$$$\\big( \\operatorname{algebraMap}_R^T \\text{ surjective} \\big) \\Rightarrow \n\\operatorname{Surj}\\left( (\\mathrm{TensorProduct.mk}\\; R\\; S\\; T).\\text{flip } 1\\right).$$$
Lean4
theorem flip_mk_surjective (h : Function.Surjective (algebraMap R T)) :
Function.Surjective ((TensorProduct.mk R S T).flip 1) :=
by
rw [← LinearMap.range_eq_top, ← top_le_iff, ← span_tmul_eq_top, Submodule.span_le]
rintro _ ⟨s, t, rfl⟩
obtain ⟨r, rfl⟩ := h t
rw [Algebra.algebraMap_eq_smul_one, ← smul_tmul]
exact ⟨r • s, rfl⟩
