English
If a monoid M acts faithfully on a semiring R, then the associated action map x ↦ (r ↦ x • r) from M to End(R) is injective; i.e., different elements of M induce different endomorphisms of R.
Русский
Если действие моноида M на полугольнике R сохраняет различие (оно верно ~faithful), то отображение x ↦ (r ↦ x • r) от M в End(R) инъективно; различные элементы M порождают различные концевые отображения.
LaTeX
$$$\\text{If }\\text{FaithfulSMul}(M,R),\\; \\text{then }\\operatorname{toRingHom}_M^R: M \\to^* \\operatorname{End}(R)\\text{ is injective}$$$
Lean4
theorem toRingHom_injective [MulSemiringAction M R] [FaithfulSMul M R] :
Function.Injective (MulSemiringAction.toRingHom M R) := fun _ _ h =>
eq_of_smul_eq_smul fun r => RingHom.ext_iff.1 h r
