English
The map of compatible scalar multiplications is surjective onto the tensor product, giving a rich supply of elements.
Русский
Отображение совместимой скалярной умножения сюрьективно по тензорному произведению, обеспечивая богатый набор элементов.
LaTeX
$$$\\text{mapOfCompatibleSMul}_{R S A B} \\text{ is surjective}. $$$
Lean4
/-- If A and B are both R- and S-algebras and their actions on them commute,
and if the S-action on `A ⊗[R] B` can switch between the two factors, then there is a
canonical S-algebra homomorphism from `A ⊗[S] B` to `A ⊗[R] B`. -/
def mapOfCompatibleSMul : A ⊗[S] B →ₐ[S] A ⊗[R] B :=
.ofLinearMap (_root_.TensorProduct.mapOfCompatibleSMul R S A B) rfl fun x ↦
x.induction_on (by simp)
(fun _ _ y ↦ y.induction_on (by simp) (by simp) fun _ _ h h' ↦ by simp only [mul_add, map_add, h, h'])
fun _ _ h h' _ ↦ by simp only [add_mul, map_add, h, h']
