English
The scalar multiplication on an object of ModuleCat R induces a ring hom from R into the endomorphisms of the forgetful abelian group.
Русский
Векторное умножение на объекте ModuleCat R индуцирует однородное гомоморфное отображение кольца R в концевые преобразования забытого абелевой группы.
LaTeX
$$$\mathrm{smul}: R \to^+* \mathrm{End}(\bigl(\mathrm{forget\_to\_AddCommGrp}(\mathrm{ModuleCat}(R))\bigr))$$$
Lean4
/-- The scalar multiplication on an object of `ModuleCat R` considered as
a morphism of rings from `R` to the endomorphisms of the underlying abelian group. -/
def smul : R →+* End ((forget₂ (ModuleCat R) AddCommGrpCat).obj M)
where
toFun
r :=
AddCommGrpCat.ofHom
{ toFun := fun (m : M) => r • m
map_zero' := by rw [smul_zero]
map_add' := fun x y => by rw [smul_add] }
map_one' := AddCommGrpCat.ext (fun x => by simp)
map_zero' := AddCommGrpCat.ext (fun x => by simp)
map_mul' r s := AddCommGrpCat.ext (fun (x : M) => (smul_smul r s x).symm)
map_add' r s := AddCommGrpCat.ext (fun (x : M) => add_smul r s x)
