English
Let R be a commutative semiring and A be an R-algebra. There is a natural R-linear map from the tensor product A ⊗R R[X] to the polynomial ring AX, obtained by lifting the bilinear map (a, p) ↦ a · p interpreted coefficientwise via the algebra structure. This map is denoted toFunLinear and is defined as the linear extension of the bilinear map toFunBilinear.
Русский
Пусть R — коммутативное полускольное кольцо, A — R-алгебра. Существует естественный R-линейный отображение от тензорного произведения A ⊗R R[X] к AX, получаемое как линейное продолжение биЛинейной карты (a, p) ↦ a · p, трактованной по всем коэффициентам через структуру алгебры. Это отображение обозначается as toFunLinear и является линейной редукцией bilinear map toFunBilinear.
LaTeX
$$$toFunLinear_R A = \\mathrm{TensorProduct}.lift( toFunBilinear_R A )$$$
Lean4
/-- (Implementation detail).
The function underlying `A ⊗[R] R[X] →ₐ[R] A[X]`,
as a linear map.
-/
def toFunLinear : A ⊗[R] R[X] →ₗ[R] A[X] :=
TensorProduct.lift (toFunBilinear R A)
