# 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 M with a monoid structure, SingleObj M is Unit type with Category structure such that End (SingleObj M).star is the monoid M. This can be extended to a functor MonCat ⥤ Cat.

If M is a group, then SingleObj M is a groupoid.

An element x : M can be reinterpreted as an element of End (SingleObj.star M) using SingleObj.toEnd.

## Implementation notes #

• categoryStruct.comp on End (SingleObj.star M) is flip (*), not (*). This way multiplication on End agrees with the multiplication on M.

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

@[reducible, inline]

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

Equations
Instances For

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

Equations
• One or more equations did not get rendered due to their size.

Monoid laws become category laws for the single object category.

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

If M is finite and in universe zero, then SingleObj M is a FinCategory.

Equations
• = { fintypeObj := inferInstance, fintypeHom := inferInstance }

Groupoid structure on SingleObj M.

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

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

Equations
Instances For

The endomorphisms monoid of the only object in SingleObj M is equivalent to the original monoid M.

Equations
• = let __src := ; { toEquiv := __src, map_mul' := }
Instances For
theorem CategoryTheory.SingleObj.toEnd_def (M : Type u) [] (x : M) :
def CategoryTheory.SingleObj.mapHom (M : Type u) [] (N : Type v) [] :

There is a 1-1 correspondence between monoid homomorphisms M → N 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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.SingleObj.mapHom_comp {M : Type u} [] {N : Type v} [] (f : M →* N) {P : Type w} [] (g : N →* P) :
(g.comp f) = ().comp ()
@[simp]
theorem CategoryTheory.SingleObj.differenceFunctor_obj {G : Type u} [] {C : Type v} (f : CG) :
∀ (x : C),
@[simp]
theorem CategoryTheory.SingleObj.differenceFunctor_map {G : Type u} [] {C : Type v} (f : CG) {x : C} {y : C} :
∀ (x_1 : x y), x_1 = f y * (f x)⁻¹
def CategoryTheory.SingleObj.differenceFunctor {G : Type u} [] {C : Type v} (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)⁻¹.

Equations
• = { obj := fun (x : C) => (), map := fun {x y : C} (x_1 : x y) => f y * (f x)⁻¹, map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.SingleObj.functor_obj {M : Type u} [] {C : Type v} {X : C} (f : ) :
∀ (x : ), .obj x = X
@[simp]
theorem CategoryTheory.SingleObj.functor_map {M : Type u} [] {C : Type v} {X : C} (f : ) :
∀ {X_1 Y : } (a : X_1 Y), .map a = f a
def CategoryTheory.SingleObj.functor {M : Type u} [] {C : Type v} {X : C} (f : ) :

A monoid homomorphism f: M → End X into the endomorphisms of an object X of a category C induces a functor SingleObj M ⥤ C.

Equations
• = { obj := fun (x : ) => X, map := fun {X_1 Y : } (a : X_1 Y) => f a, map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.SingleObj.natTrans_app {M : Type u} [] {C : Type v} {F : } {G : } (u : F.obj G.obj ) (h : ∀ (a : M), CategoryTheory.CategoryStruct.comp (F.map a) u = CategoryTheory.CategoryStruct.comp u (G.map a)) :
∀ (x : ), .app x = u
def CategoryTheory.SingleObj.natTrans {M : Type u} [] {C : Type v} {F : } {G : } (u : F.obj G.obj ) (h : ∀ (a : M), CategoryTheory.CategoryStruct.comp (F.map a) u = CategoryTheory.CategoryStruct.comp u (G.map a)) :
F G

Construct a natural transformation between functors SingleObj M ⥤ C by giving a compatible morphism SingleObj.star M.

Equations
• = { app := fun (x : ) => u, naturality := }
Instances For
@[reducible, inline]
abbrev MonoidHom.toFunctor {M : Type u} {N : Type v} [] [] (f : M →* 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.

Equations
• f.toFunctor =
Instances For
@[simp]
theorem MonoidHom.comp_toFunctor {M : Type u} {N : Type v} [] [] (f : M →* N) {P : Type w} [] (g : N →* P) :
(g.comp f).toFunctor = f.toFunctor.comp g.toFunctor
@[simp]
theorem MonoidHom.id_toFunctor (M : Type u) [] :
().toFunctor =
@[simp]
theorem MulEquiv.toSingleObjEquiv_functor_obj {M : Type u} {N : Type v} [] [] (e : M ≃* N) (a : ) :
e.toSingleObjEquiv.functor.obj a = a
@[simp]
theorem MulEquiv.toSingleObjEquiv_unitIso_hom {M : Type u} {N : Type v} [] [] (e : M ≃* N) :
e.toSingleObjEquiv.unitIso.hom =
@[simp]
theorem MulEquiv.toSingleObjEquiv_unitIso_inv {M : Type u} {N : Type v} [] [] (e : M ≃* N) :
e.toSingleObjEquiv.unitIso.inv =
@[simp]
theorem MulEquiv.toSingleObjEquiv_counitIso_hom {M : Type u} {N : Type v} [] [] (e : M ≃* N) :
e.toSingleObjEquiv.counitIso.hom =
@[simp]
theorem MulEquiv.toSingleObjEquiv_inverse_map {M : Type u} {N : Type v} [] [] (e : M ≃* N) :
∀ {X Y : } (a : N), e.toSingleObjEquiv.inverse.map a = e.symm a
@[simp]
theorem MulEquiv.toSingleObjEquiv_counitIso_inv {M : Type u} {N : Type v} [] [] (e : M ≃* N) :
e.toSingleObjEquiv.counitIso.inv =
@[simp]
theorem MulEquiv.toSingleObjEquiv_inverse_obj {M : Type u} {N : Type v} [] [] (e : M ≃* N) (a : ) :
e.toSingleObjEquiv.inverse.obj a = a
@[simp]
theorem MulEquiv.toSingleObjEquiv_functor_map {M : Type u} {N : Type v} [] [] (e : M ≃* N) :
∀ {X Y : } (a : M), e.toSingleObjEquiv.functor.map a = e a
def MulEquiv.toSingleObjEquiv {M : Type u} {N : Type v} [] [] (e : M ≃* N) :

Reinterpret a monoid isomorphism f : M ≃* N as an equivalence SingleObj M ≌ SingleObj N.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Units.toAut (M : 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.

Equations
Instances For
@[simp]
theorem Units.toAut_hom (M : Type u) [] (x : Mˣ) :
(() x).hom =
@[simp]
theorem Units.toAut_inv (M : Type u) [] (x : Mˣ) :
(() x).inv =

The fully faithful functor from MonCat to Cat.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Equations