Single object category with a given monoid of endomorphisms. It is defined to facilitate transfering some definitions and lemmas (e.g., conjugacy etc.) from category theory to monoids and groups.
Given a type α with a monoid structure, single_obj α is unit type with category structure such that End (single_obj α).star is the monoid α. This can be extended to a functor Mon ⥤ Cat.
If α is a group, then single_obj α is a groupoid.
An element x : α can be reinterpreted as an element of End (single_obj.star α) using single_obj.to_End.
category_struct.comp on End (single_obj.star α) is flip (*), not (*). This way multiplication on End agrees with the multiplication on α.
By default, Lean puts instances into category_theory namespace instead of category_theory.single_obj, so we give all names explicitly.
Type tag on unit used to define single-object categories and groupoids.
One and flip (*) become id and comp for morphisms of the single object category.
Monoid laws become category laws for the single object category.
Groupoid structure on single_obj α
The endomorphisms monoid of the only object in single_obj α is equivalent to the original monoid α.
There is a 1-1 correspondence between monoid homomorphisms α → β and functors between the corresponding single-object categories. It means that single_obj is a fully faithful functor.
Reinterpret a monoid homomorphism f : α → β as a functor (single_obj α) ⥤ (single_obj β). See also category_theory.single_obj.map_hom for an equivalence between these types.
The fully faithful functor from Mon to Cat.