lTensorAlgHom — Mathlib

English

The map sending f to 1 ⊗ f is a morphism of algebras from End_R(M) to End_R(N ⊗_R M).

Русский

Отображение, отправляющее f в 1 ⊗ f, является морфизмом полуалгебр от End_R(M) в End_R(N ⊗_R M).

LaTeX

$$$\\mathrm{lTensorAlgHom}: \\mathrm{Module.End}_R(M) \\to_{\\,\\}^{\\,\\} \\mathrm{Module.End}_R(N \\otimes_R M)$$$

Lean4

/-- The map `LinearMap.lTensorHom` which sends `f ↦ 1 ⊗ f` as a morphism of algebras. -/
@[simps!]
def lTensorAlgHom : Module.End R M →ₐ[R] Module.End R (N ⊗[R] M) :=
  .ofLinearMap (lTensorHom (M := N)) (lTensor_id N M) (lTensor_mul N)

Похожие утверждения