English
Let A be an algebra over a commutative semiring R. Then there is a natural algebra homomorphism from A to the endomorphism ring End_R(A) given by left multiplication: to each a ∈ A, assign the endomorphism x ↦ a x of the R-module A. This map preserves addition and multiplication and sends 1 to the identity.
Русский
Пусть A — алгебра над коммутативным полупринцом R. Существует естественный алгебраический гомоморфизм из A в кольцо концевых отображений End_R(A), задаваемый левым умножением: a ↦ (x ↦ a x). Этот отображение сохраняет сложение и умножение и отображает 1 в тождественный эндоморфизм.
LaTeX
$$$\exists \ell: A \to_{R} \mathrm{End}_{R}(A),\forall a,x\in A:\ \ell(a)(x)=a\,x.$$$
Lean4
/-- The multiplication in an algebra is an algebra homomorphism into the endomorphisms on
the algebra.
A weaker version of this for non-unital algebras exists as `NonUnitalAlgHom.lmul`. -/
def _root_.Algebra.lmul : A →ₐ[R] End R A
where
__ := NonUnitalAlgHom.lmul R A
map_one' := mulLeft_one _ _
commutes' r := ext fun a => (Algebra.smul_def r a).symm
