# mathlibdocumentation

category_theory.single_obj

# Single-object category

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.

## Main definitions

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.

## Implementation notes

• 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.

@[nolint]
def category_theory.single_obj  :
Type u → Type

Type tag on unit used to define single-object categories and groupoids.

Equations
@[instance]

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

Equations
@[instance]
def category_theory.single_obj.category (α : Type u) [monoid α] :

Monoid laws become category laws for the single object category.

Equations
@[instance]
def category_theory.single_obj.groupoid (α : Type u) [group α] :

Groupoid structure on single_obj α.

See https://stacks.math.columbia.edu/tag/0019.

Equations
def category_theory.single_obj.star (α : Type u) :

The single object in single_obj α.

Equations
def category_theory.single_obj.to_End (α : Type u) [monoid α] :

The endomorphisms monoid of the only object in single_obj α is equivalent to the original monoid α.

Equations
theorem category_theory.single_obj.to_End_def (α : Type u) [monoid α] (x : α) :

def category_theory.single_obj.map_hom (α : Type u) (β : Type v) [monoid α] [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.

See https://stacks.math.columbia.edu/tag/001F -- although we do not characterize when the functor is full or faithful.

Equations
theorem category_theory.single_obj.map_hom_id (α : Type u) [monoid α] :

theorem category_theory.single_obj.map_hom_comp {α : Type u} {β : Type v} [monoid α] [monoid β] (f : α →* β) {γ : Type w} [monoid γ] (g : β →* γ) :
(g.comp f) =

def monoid_hom.to_functor {α : Type u} {β : Type v} [monoid α] [monoid β] :

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.

Equations
@[simp]
theorem monoid_hom.id_to_functor (α : Type u) [monoid α] :

@[simp]
theorem monoid_hom.comp_to_functor {α : Type u} {β : Type v} [monoid α] [monoid β] (f : α →* β) {γ : Type w} [monoid γ] (g : β →* γ) :

def units.to_Aut (α : Type u) [monoid α] :

The units in a monoid are (multiplicatively) equivalent to the automorphisms of star when we think of the monoid as a single-object category.

Equations
@[simp]
theorem units.to_Aut_hom (α : Type u) [monoid α] (x : units α) :

@[simp]
theorem units.to_Aut_inv (α : Type u) [monoid α] (x : units α) :

The fully faithful functor from Mon to Cat.

Equations
@[instance]

Equations
@[instance]