English
There is a canonical A-linear map from the A-tensor product to the R-tensor product under compatible smul conditions.
Русский
Существует каноническое A-линейное отображение из A-тензорного произведения в R-тензорное произведение при несовпадении діях и совместимости смул.
LaTeX
$$$mapOfCompatibleSMul : M \\otimes_A N \\to_A M \\otimes_R N$$$
Lean4
/-- If M and N are both R- and A-modules and their actions on them commute,
and if the A-action on `M ⊗[R] N` can switch between the two factors, then there is a
canonical A-linear map from `M ⊗[A] N` to `M ⊗[R] N`. -/
def mapOfCompatibleSMul : M ⊗[A] N →ₗ[A] M ⊗[R] N :=
lift
{ toFun := fun m ↦
{ __ := mk R M N m
map_smul' := fun _ _ ↦ (smul_tmul _ _ _).symm }
map_add' := fun _ _ ↦ LinearMap.ext <| by simp
map_smul' := fun _ _ ↦ rfl }
