English
If S is commutative and f: A →ₐ[R] S, g: B →ₐ[R] S are algebra homomorphisms, then there is a canonical algebra homomorphism productMap f g: A ⊗_R B →ₐ[R] S defined by a ⊗ b ↦ f(a) g(b).
Русский
Если S коммутативна и заданы алгебра-гомоморфизмы f и g, существует канонический алгебра-гомоморфизм productMap f g: A ⊗_R B →ₐ[R] S, заданный на чистом тензоре a ⊗ b как f(a) g(b).
LaTeX
$$$ productMap f g : A \otimes_R B \to S,\qquad (a \otimes b) \mapsto f(a)\, g(b) $$$
Lean4
/-- If `S` is commutative, for a pair of morphisms `f : A →ₐ[R] S`, `g : B →ₐ[R] S`,
We obtain a map `A ⊗[R] B →ₐ[R] S` that commutes with `f`, `g` via `a ⊗ b ↦ f(a) * g(b)`.
This is a special case of `Algebra.TensorProduct.productLeftAlgHom` for when the two base rings are
the same.
-/
def productMap : A ⊗[R] B →ₐ[R] S :=
productLeftAlgHom f g
