toFunctor — Mathlib

English

Every monoid homomorphism f: M →* N corresponds to a functor SingleObj M ⥤ SingleObj N.

Русский

Каждый гомоморфизм моноидов f: M →* N соответствует функтору SingleObj M ⥤ SingleObj N.

LaTeX

$$$\\mathrm{toFunctor} : (M \\to^* N) \\to \\mathrm{Functor}(\\mathrm{SingleObj} M, \\mathrm{SingleObj} N)$$$

Lean4

/-- Reinterpret a monoid homomorphism `f : M → N` as a functor `(single_obj M) ⥤ (single_obj N)`.
See also `CategoryTheory.SingleObj.mapHom` for an equivalence between these types. -/
abbrev toFunctor (f : M →* N) : SingleObj M ⥤ SingleObj N :=
  SingleObj.mapHom M N f

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