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

@[inline, reducible]

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
• = CategoryTheory.Category.mk
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
• = CategoryTheory.FinCategory.mk

Groupoid structure on SingleObj M.

See .

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

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' := (_ : ∀ (x x_1 : M), ().toFun (x * x_1) = ().toFun (x * x_1)) }
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 -- 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) :
() =
@[simp]
theorem CategoryTheory.SingleObj.differenceFunctor_obj {G : Type u} [] {C : Type v} (f : CG) :
∀ (x : C), .toPrefunctor.obj x = ()
@[simp]
theorem CategoryTheory.SingleObj.differenceFunctor_map {G : Type u} [] {C : Type v} (f : CG) {x : C} {y : C} :
∀ (x_1 : x y), .toPrefunctor.map 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
Instances For
@[simp]
theorem CategoryTheory.SingleObj.functor_obj {M : Type u} [] {C : Type v} {X : C} (f : ) :
∀ (x : ), .toPrefunctor.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), .toPrefunctor.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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.SingleObj.natTrans_app {M : Type u} [] {C : Type v} {F : } {G : } (u : F.toPrefunctor.obj G.toPrefunctor.obj ) (h : ∀ (a : M), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map a) u = CategoryTheory.CategoryStruct.comp u (G.toPrefunctor.map a)) :
∀ (x : ), .app x = u
def CategoryTheory.SingleObj.natTrans {M : Type u} [] {C : Type v} {F : } {G : } (u : F.toPrefunctor.obj G.toPrefunctor.obj ) (h : ∀ (a : M), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map a) u = CategoryTheory.CategoryStruct.comp u (G.toPrefunctor.map a)) :
F G

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

Equations
Instances For
@[reducible]
def 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
Instances For
@[simp]
theorem MonoidHom.comp_toFunctor {M : Type u} {N : Type v} [] [] (f : M →* N) {P : Type w} [] (g : N →* P) :
@[simp]
theorem MonoidHom.id_toFunctor (M : Type u) [] :
@[simp]
theorem MulEquiv.toSingleObjEquiv_functor_obj {M : Type u} {N : Type v} [] [] (e : M ≃* N) (a : ) :
.functor.toPrefunctor.obj a = a
@[simp]
theorem MulEquiv.toSingleObjEquiv_counitIso_hom {M : Type u} {N : Type v} [] [] (e : M ≃* N) :
.counitIso.hom = CategoryTheory.eqToHom (_ : )
@[simp]
theorem MulEquiv.toSingleObjEquiv_unitIso_hom {M : Type u} {N : Type v} [] [] (e : M ≃* N) :
.unitIso.hom = CategoryTheory.eqToHom (_ : )
@[simp]
theorem MulEquiv.toSingleObjEquiv_unitIso_inv {M : Type u} {N : Type v} [] [] (e : M ≃* N) :
.unitIso.inv = CategoryTheory.eqToHom (_ : )
@[simp]
theorem MulEquiv.toSingleObjEquiv_functor_map {M : Type u} {N : Type v} [] [] (e : M ≃* N) :
∀ {X Y : } (a : M), .functor.toPrefunctor.map a = e a
@[simp]
theorem MulEquiv.toSingleObjEquiv_inverse_obj {M : Type u} {N : Type v} [] [] (e : M ≃* N) (a : ) :
.inverse.toPrefunctor.obj a = a
@[simp]
theorem MulEquiv.toSingleObjEquiv_counitIso_inv {M : Type u} {N : Type v} [] [] (e : M ≃* N) :
.counitIso.inv = CategoryTheory.eqToHom (_ : )
@[simp]
theorem MulEquiv.toSingleObjEquiv_inverse_map {M : Type u} {N : Type v} [] [] (e : M ≃* N) :
∀ {X Y : } (a : N), .inverse.toPrefunctor.map a = () 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