toAlgHom — Mathlib

English

Each element m of M defines an R-algebra homomorphism A →ₐ[R] A given by a ↦ m • a; this is the canonical action by the monoid.

Русский

Каждый элемент m из M задаёт гомоморфизм A →ₐ[R] A над R, действуя через a ↦ m • a; это каноническое действие моноида.

LaTeX

$$$ toAlgHom (m) : A \\toₐ[R] A $ with defined action $toAlgHom(m)(a) = m \\cdot a$$$

Lean4

/-- Each element of the monoid defines an algebra homomorphism.

This is a stronger version of `MulSemiringAction.toRingHom` and
`DistribMulAction.toLinearMap`. -/
@[simps]
def toAlgHom (m : M) : A →ₐ[R] A :=
  { MulSemiringAction.toRingHom _ _ m with
    toFun := fun a => m • a
    commutes' := smul_algebraMap _ }

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