English
For any r in the scalar algebra S, the map algebraMap S (A ⊗_R B) sends r to (algebraMap S A r) ⊗ 1.
Русский
Для любого элемента r из S отображение algebraMap S (A ⊗_R B) отправляет r в (algebraMap S A r) ⊗ 1.
LaTeX
$$$ algebraMap S (A \otimes_R B) r = (algebraMap S A) r \otimes_\text{tmul} 1 $$$
Lean4
instance leftAlgebra [SMulCommClass R S A] : Algebra S (A ⊗[R] B) :=
{ commutes' := fun r x =>
by
dsimp only [RingHom.toFun_eq_coe, RingHom.comp_apply, includeLeftRingHom_apply]
rw [algebraMap_eq_smul_one, ← smul_tmul', ← one_def, mul_smul_comm, smul_mul_assoc, mul_one, one_mul]
smul_def' := fun r x =>
by
dsimp only [RingHom.toFun_eq_coe, RingHom.comp_apply, includeLeftRingHom_apply]
rw [algebraMap_eq_smul_one, ← smul_tmul', smul_mul_assoc, ← one_def, one_mul]
algebraMap := TensorProduct.includeLeftRingHom.comp (algebraMap S A) }
