Theorems · Definition · category theory

MonoidHom.toFunctor

{M : Type u} →
  {N : Type v} →
    [inst : Monoid M] →
      [inst_1 : Monoid N] → (M →* N) → CategoryTheory.Functor (CategoryTheory.SingleObj M) (CategoryTheory.SingleObj N)

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.

Defined in

Mathlib.CategoryTheory.SingleObj

Cited by

6 results in Mathlib

Foundations

Depth 19 from the axioms · uses Quot.sound

Assumes

MonoidMonoid