English
The action of moduleAux on a simple tensor a ⊗ b and an element m equals a · b · m.
Русский
Действие moduleAux на простой тензор a ⊗ b и элемент m равно a · b · m.
LaTeX
$$moduleAux (a ⊗ b) m = a · b · m$$
Lean4
/-- The algebra homomorphism from `End M ⊗ End N` to `End (M ⊗ N)` sending `f ⊗ₜ g` to
the `TensorProduct.map f g`, the tensor product of the two maps.
This is an `AlgHom` version of `TensorProduct.AlgebraTensorModule.homTensorHomMap`. Like that
definition, this is generalized across many different rings; namely a tower of algebras `A/S/R`. -/
def endTensorEndAlgHom : End A M ⊗[R] End R N →ₐ[S] End A (M ⊗[R] N) :=
Algebra.TensorProduct.algHomOfLinearMapTensorProduct (AlgebraTensorModule.homTensorHomMap R A S M N M N)
(fun _f₁ _f₂ _g₁ _g₂ => AlgebraTensorModule.ext fun _m _n => rfl) (AlgebraTensorModule.ext fun _m _n => rfl)
