# Documentation

Mathlib.CategoryTheory.SingleObj

# 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 on End (SingleObj.star α) is flip (*), not (*). This way multiplication on End agrees with the multiplication on α.

• By default, Lean puts instances into CategoryTheory namespace instead of CategoryTheory.SingleObj, so we give all names explicitly.

@[inline, reducible]

Abbreviation that allows writing CategoryTheory.SingleObj rather than Quiver.SingleObj.

Instances For
instance CategoryTheory.SingleObj.categoryStruct (α : Type u) [One α] [Mul α] :

One and flip (*) become id and comp for morphisms of the single object category.

Monoid laws become category laws for the single object category.

theorem CategoryTheory.SingleObj.id_as_one (α : Type u) [] (x : ) :
theorem CategoryTheory.SingleObj.comp_as_mul (α : Type u) [] {x : } {y : } {z : } (f : x y) (g : y z) :

Groupoid structure on SingleObj α.

theorem CategoryTheory.SingleObj.inv_as_inv (α : Type u) [] {x : } {y : } (f : x y) :
@[inline, reducible]

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
theorem CategoryTheory.SingleObj.toEnd_def (α : Type u) [] (x : α) :
= x
def CategoryTheory.SingleObj.mapHom (α : Type u) (β : Type v) [] [] :

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
theorem CategoryTheory.SingleObj.mapHom_comp {α : Type u} {β : Type v} [] [] (f : α →* β) {γ : Type w} [] (g : β →* γ) :
↑() () = CategoryTheory.Functor.comp (↑() f) (↑() g)
@[simp]
theorem CategoryTheory.SingleObj.differenceFunctor_obj {C : Type u_1} {G : Type u_2} [] [] (f : CG) :
∀ (x : C),
@[simp]
theorem CategoryTheory.SingleObj.differenceFunctor_map {C : Type u_1} {G : Type u_2} [] [] (f : CG) {x : C} {y : C} :
∀ (x : x y), = f y * (f x)⁻¹
def CategoryTheory.SingleObj.differenceFunctor {C : Type u_1} {G : Type u_2} [] [] (f : CG) :

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
@[reducible]
def MonoidHom.toFunctor {α : Type u} {β : Type v} [] [] (f : α →* β) :

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
@[simp]
theorem MonoidHom.id_toFunctor (α : Type u) [] :
@[simp]
theorem MonoidHom.comp_toFunctor {α : Type u} {β : Type v} [] [] (f : α →* β) {γ : Type w} [] (g : β →* γ) :
def Units.toAut (α : Type u) [] :

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
@[simp]
theorem Units.toAut_hom (α : Type u) [] (x : αˣ) :
(↑() x).hom =
@[simp]
theorem Units.toAut_inv (α : Type u) [] (x : αˣ) :
(↑() x).inv =

The fully faithful functor from MonCat to Cat.

Instances For