English
The linear map underlying rTensorAlgHom coincides with the canonical rTensor linear map; they are the same when viewed as linear maps.
Русский
Линейное отображение, лежащее в основе rTensorAlgHom, совпадает с каноническим линейным отображением rTensor; как линейные отображения они тождественны.
LaTeX
$$$\\text{(rTensorAlgHom)}\\; \\text{as linear map} = rTensor$$$
Lean4
/-- The algebra morphism from a tensor product of a polynomial algebra
by an algebra to a polynomial algebra -/
noncomputable def rTensorAlgHom : (MvPolynomial σ S) ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N) :=
Algebra.TensorProduct.lift (mapAlgHom Algebra.TensorProduct.includeLeft)
((IsScalarTower.toAlgHom R (S ⊗[R] N) _).comp Algebra.TensorProduct.includeRight)
(fun p n => by simp [commute_iff_eq, algebraMap_eq, mul_comm])
