instMulDistribMulActionAlgHomUnits

English

Each element m of a monoid M defines an R-algebra endomorphism of A by the action a ↦ m • a; this is a bona fide AlgHom.

Русский

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

LaTeX

$$$ toAlgHom (m) : A \\to_{{R}} A \\text{ with } (toAlgHom(m)).toFun(a) = m \\cdot a $$$

Lean4

instance : MulDistribMulAction (A →ₐ[R] A) Aˣ where
  smul f := Units.map f
  one_smul _ := by ext; rfl
  mul_smul _ _ _ := by ext; rfl
  smul_mul _ _ _ := by ext; exact map_mul _ _ _
  smul_one _ := by ext; exact map_one _

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