English
There is a 1‑1 correspondence between monoid homomorphisms M →* N and functors from the single-object category of M to the single-object category of N; i.e., SingleObj is fully faithful with respect to MonoidHom.
Русский
Существует биекция между гомоморфизмами моноидов M →* N и функторными отображениями между одиночными объектами категорий; то есть Functor(SingleObj M, SingleObj N) эквивалентен MonoidHom(M,N).
LaTeX
$$$(M\\to^* N) \\simeq \\mathrm{Functor}(\\mathrm{SingleObj} M, \\mathrm{SingleObj} N)$$$
Lean4
/-- There is a 1-1 correspondence between monoid homomorphisms `M → N` and functors between the
corresponding single-object categories. It means that `SingleObj` is a fully faithful functor. -/
@[stacks 001F "We do not characterize when the functor is full or faithful."]
def mapHom : (M →* N) ≃ SingleObj M ⥤ SingleObj N
where
toFun
f :=
{ obj := id
map := ⇑f
map_id := fun _ => f.map_one
map_comp := fun x y => f.map_mul y x }
invFun
f :=
{ toFun := fun x => f.map ((toEnd M) x)
map_one' := f.map_id _
map_mul' := fun x y => f.map_comp y x }
left_inv := by cat_disch
right_inv := by cat_disch
