English
ProductMap equals the composition of lmul' with TensorProduct.map f g.
Русский
ProductMap равен композиции lmul' и TensorProduct.map f g.
LaTeX
$$productMap f g = (lmul' R).comp (TensorProduct.map f g)$$
Lean4
/-- The natural `A`-algebra homomorphism $A ⊗ (\text{End}_R M) → \text{End}_A (A ⊗ M)$,
where `M` is an `R`-module, and `A` an `R`-algebra. -/
@[simps!]
def tensorProductEnd : A ⊗[R] (End R M) →ₐ[A] End A (A ⊗[R] M) :=
Algebra.TensorProduct.algHomOfLinearMapTensorProduct (LinearMap.tensorProduct R A M M)
(fun a b f g ↦ by
apply LinearMap.ext
intro x
simp only [tensorProduct, mul_comm a b, Module.End.mul_eq_comp, TensorProduct.AlgebraTensorModule.lift_apply,
TensorProduct.lift.tmul, coe_restrictScalars, coe_mk, AddHom.coe_mk, mul_smul, smul_apply, baseChangeHom_apply,
baseChange_comp, comp_apply, Algebra.mul_smul_comm, Algebra.smul_mul_assoc])
(by
apply LinearMap.ext
intro x
simp only [tensorProduct, TensorProduct.AlgebraTensorModule.lift_apply, TensorProduct.lift.tmul,
coe_restrictScalars, coe_mk, AddHom.coe_mk, one_smul, baseChangeHom_apply, baseChange_eq_ltensor,
Module.End.one_eq_id, lTensor_id, LinearMap.id_apply])
