English
There is a canonical algebra homomorphism from End_A M ⊗ End_R N to End_A (M ⊗_R N) built from the homTensorHomMap construction; this is an instance of a general tensor-algebra construction.
Русский
Существуют канонические алгебраические отображения из End_A M ⊗ End_R N в End_A (M ⊗_R N), получаемые из конструкций homTensorHomMap.
LaTeX
$$endTensorEndAlgHom : End_A M ⊗_R End_R N →ₐ[S] End_A (M ⊗_R N)$$
Lean4
/-- The natural linear map $A ⊗ \text{Hom}_R(M, N) → \text{Hom}_A (M_A, N_A)$,
where $M_A$ and $N_A$ are the respective modules over $A$ obtained by extension of scalars.
See `LinearMap.tensorProductEnd` for this map specialized to endomorphisms,
and bundled as `A`-algebra homomorphism. -/
@[simps!]
def tensorProduct : A ⊗[R] (M →ₗ[R] N) →ₗ[A] (A ⊗[R] M) →ₗ[A] (A ⊗[R] N) :=
TensorProduct.AlgebraTensorModule.lift <|
{ toFun := fun a ↦ a • baseChangeHom R A M N
map_add' := by simp only [add_smul, forall_true_iff]
map_smul' := by simp only [smul_assoc, RingHom.id_apply, forall_true_iff] }
