English
Let A and B be subalgebras of a commutative R-algebra S. There exists a canonical R-algebra homomorphism from the tensor product A ⊗_R B to S given by multiplication in S; on simple tensors it sends a ⊗ b to ab.
Русский
Пусть A и B - подалгебры над R внутри коммутативной R-алгебры S. Существует канонический R-алгебрный гомоморфизм A ⊗_R B → S, задаваемый умножением в S; на простых тензорах a ⊗ b отображается в ab.
LaTeX
$$$\exists \varphi: A \otimes_R B \to_R S,\; \varphi(a \otimes b) = ab \quad(a \in A, b \in B)$$$
Lean4
/-- If `A` and `B` are subalgebras in a commutative algebra `S` over `R`,
there is the natural `R`-algebra homomorphism
`A ⊗[R] B →ₐ[R] S` induced by multiplication in `S`. -/
def mulMap : A ⊗[R] B →ₐ[R] S :=
Algebra.TensorProduct.productMap A.val B.val
