English
A monoid homomorphism f: M →* End X into the endomorphisms of an object X induces a functor SingleObj M ⥤ C sending the single object to X and a ∈ M to the endomorphism f(a).
Русский
Гомоморфизм моноидов f: M →* End X порождает функтор SingleObj M ⥤ C, отправляющий единственный объект в X и элемент a ∈ M в эндоморфизм f(a).
LaTeX
$$$\\text{If } f: M \\to^* \\mathrm{End}(X), \\text{ then } F:\\mathrm{SingleObj} M \\to C \\text{ with } F(*)=X,\\ F(a)=f(a).$$$
Lean4
/-- A monoid homomorphism `f: M → End X` into the endomorphisms of an object `X` of a category `C`
induces a functor `SingleObj M ⥤ C`. -/
@[simps]
def functor {X : C} (f : M →* End X) : SingleObj M ⥤ C
where
obj _ := X
map a := f a
map_id _ := MonoidHom.map_one f
map_comp a b := MonoidHom.map_mul f b a
