Single-object category #
Single object category with a given monoid of endomorphisms. It is defined to facilitate transferring some definitions and lemmas (e.g., conjugacy etc.) from category theory to monoids and groups.
Main definitions #
Given a type α
with a monoid structure, SingleObj α
is Unit
type with Category
structure
such that End (SingleObj α).star
is the monoid α
. This can be extended to a functor
MonCat ⥤ Cat
.
If α
is a group, then SingleObj α
is a groupoid.
An element x : α
can be reinterpreted as an element of End (SingleObj.star α)
using
SingleObj.toEnd
.
Implementation notes #
-
categoryStruct.comp
onEnd (SingleObj.star α)
isflip (*)
, not(*)
. This way multiplication onEnd
agrees with the multiplication onα
. -
By default, Lean puts instances into
CategoryTheory
namespace instead ofCategoryTheory.SingleObj
, so we give all names explicitly.
Abbreviation that allows writing CategoryTheory.SingleObj
rather than Quiver.SingleObj
.
Instances For
Monoid laws become category laws for the single object category.
Groupoid structure on SingleObj α
.
Abbreviation that allows writing CategoryTheory.SingleObj.star
rather than
Quiver.SingleObj.star
.
Instances For
The endomorphisms monoid of the only object in SingleObj α
is equivalent to the original
monoid α.
Instances For
There is a 1-1 correspondence between monoid homomorphisms α → β
and functors between the
corresponding single-object categories. It means that SingleObj
is a fully faithful
functor.
See https://stacks.math.columbia.edu/tag/001F -- although we do not characterize when the functor is full or faithful.
Instances For
Given a function f : C → G
from a category to a group, we get a functor
C ⥤ G
sending any morphism x ⟶ y
to f y * (f x)⁻¹
.
Instances For
Reinterpret a monoid homomorphism f : α → β
as a functor (single_obj α) ⥤ (single_obj β)
.
See also CategoryTheory.SingleObj.mapHom
for an equivalence between these types.
Instances For
The units in a monoid are (multiplicatively) equivalent to
the automorphisms of star
when we think of the monoid as a single-object category.
Instances For
The fully faithful functor from MonCat
to Cat
.