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]

abbrev CategoryTheory.SingleObj : Type u_1 → Type

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

@[implicit_reducible]

instance CategoryTheory.SingleObj.categoryStruct (M : Type u) [One M] [Mul M] : CategoryStruct.{u, 0} (SingleObj M)

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

@[implicit_reducible]

instance CategoryTheory.SingleObj.category (M : Type u) [Monoid M] : Category.{u, 0} (SingleObj M)

Monoid laws become category laws for the single object category.

theorem CategoryTheory.SingleObj.id_as_one (M : Type u) [Monoid M] (x : SingleObj M) : CategoryStruct.id x = 1

theorem CategoryTheory.SingleObj.comp_as_mul (M : Type u) [Monoid M] {x y z : SingleObj M} (f : x ⟶ y) (g : y ⟶ z) : CategoryStruct.comp f g = g * f

@[implicit_reducible]

instance CategoryTheory.SingleObj.finCategoryOfFintype (M : Type) [Fintype M] [Monoid M] : FinCategory (SingleObj M)

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

@[implicit_reducible]

instance CategoryTheory.SingleObj.groupoid (G : Type u) [Group G] : Groupoid (SingleObj G)

Groupoid structure on SingleObj M.

theorem CategoryTheory.SingleObj.inv_as_inv (G : Type u) [Group G] {x y : SingleObj G} (f : x ⟶ y) : inv f = f⁻¹

@[reducible, inline]

abbrev CategoryTheory.SingleObj.star (M : Type u) : SingleObj M

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

def CategoryTheory.SingleObj.toEnd (M : Type u) [Monoid M] : M ≃* End (star M)

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

theorem CategoryTheory.SingleObj.toEnd_def (M : Type u) [Monoid M] (x : M) : (toEnd M) x = x

def CategoryTheory.SingleObj.mapHom (M : Type u) [Monoid M] (N : Type v) [Monoid N] : (M →* N) ≃ Functor (SingleObj M) (SingleObj N)

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.

theorem CategoryTheory.SingleObj.mapHom_id (M : Type u) [Monoid M] : (mapHom M M) (MonoidHom.id M) = Functor.id (SingleObj M)

theorem CategoryTheory.SingleObj.mapHom_comp {M : Type u} [Monoid M] {N : Type v} [Monoid N] (f : M →* N) {P : Type w} [Monoid P] (g : N →* P) : (mapHom M P) (g.comp f) = ((mapHom M N) f).comp ((mapHom N P) g)

def CategoryTheory.SingleObj.differenceFunctor {G : Type u} [Group G] {C : Type v} [Category.{w, v} C] (f : C → G) : Functor C (SingleObj G)

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)⁻¹.

@[simp]

theorem CategoryTheory.SingleObj.differenceFunctor_obj {G : Type u} [Group G] {C : Type v} [Category.{w, v} C] (f : C → G) (x✝ : C) : (differenceFunctor f).obj x✝ = ()

@[simp]

theorem CategoryTheory.SingleObj.differenceFunctor_map {G : Type u} [Group G] {C : Type v} [Category.{w, v} C] (f : C → G) {x y : C} (x✝ : x ⟶ y) : (differenceFunctor f).map x✝ = f y * (f x)⁻¹

def CategoryTheory.SingleObj.functor {M : Type u} [Monoid M] {C : Type v} [Category.{w, v} C] {X : C} (f : M →* End X) : Functor (SingleObj M) C

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

@[simp]

theorem CategoryTheory.SingleObj.functor_obj {M : Type u} [Monoid M] {C : Type v} [Category.{w, v} C] {X : C} (f : M →* End X) (x✝ : SingleObj M) : (functor f).obj x✝ = X

@[simp]

theorem CategoryTheory.SingleObj.functor_map {M : Type u} [Monoid M] {C : Type v} [Category.{w, v} C] {X : C} (f : M →* End X) {X✝ Y✝ : SingleObj M} (a : X✝ ⟶ Y✝) : (functor f).map a = f a

def CategoryTheory.SingleObj.natTrans {M : Type u} [Monoid M] {C : Type v} [Category.{w, v} C] {F G : Functor (SingleObj M) C} (u : F.obj (star M) ⟶ G.obj (star M)) (h : ∀ (a : M), CategoryStruct.comp (F.map a) u = 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.

@[simp]

theorem CategoryTheory.SingleObj.natTrans_app {M : Type u} [Monoid M] {C : Type v} [Category.{w, v} C] {F G : Functor (SingleObj M) C} (u : F.obj (star M) ⟶ G.obj (star M)) (h : ∀ (a : M), CategoryStruct.comp (F.map a) u = CategoryStruct.comp u (G.map a)) (x✝ : SingleObj M) : (natTrans u h).app x✝ = u

@[reducible, inline]

abbrev MonoidHom.toFunctor {M : Type u} {N : Type v} [Monoid M] [Monoid N] (f : M →* N) : CategoryTheory.Functor (CategoryTheory.SingleObj M) (CategoryTheory.SingleObj 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.

@[simp]

theorem MonoidHom.comp_toFunctor {M : Type u} {N : Type v} [Monoid M] [Monoid N] (f : M →* N) {P : Type w} [Monoid P] (g : N →* P) : (g.comp f).toFunctor = f.toFunctor.comp g.toFunctor

@[simp]

theorem MonoidHom.id_toFunctor (M : Type u) [Monoid M] : (id M).toFunctor = CategoryTheory.Functor.id (CategoryTheory.SingleObj M)

def MulEquiv.toSingleObjEquiv {M : Type u} {N : Type v} [Monoid M] [Monoid N] (e : M ≃* N) : CategoryTheory.SingleObj M ≌ CategoryTheory.SingleObj N

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

@[simp]

theorem MulEquiv.toSingleObjEquiv_functor_map {M : Type u} {N : Type v} [Monoid M] [Monoid N] (e : M ≃* N) {X✝ Y✝ : CategoryTheory.SingleObj M} (a : M) : e.toSingleObjEquiv.functor.map a = e a

@[simp]

theorem MulEquiv.toSingleObjEquiv_unitIso_hom {M : Type u} {N : Type v} [Monoid M] [Monoid N] (e : M ≃* N) : e.toSingleObjEquiv.unitIso.hom = CategoryTheory.eqToHom ⋯

@[simp]

theorem MulEquiv.toSingleObjEquiv_inverse_map {M : Type u} {N : Type v} [Monoid M] [Monoid N] (e : M ≃* N) {X✝ Y✝ : CategoryTheory.SingleObj N} (a : N) : e.toSingleObjEquiv.inverse.map a = e.symm a

@[simp]

theorem MulEquiv.toSingleObjEquiv_unitIso_inv {M : Type u} {N : Type v} [Monoid M] [Monoid N] (e : M ≃* N) : e.toSingleObjEquiv.unitIso.inv = CategoryTheory.eqToHom ⋯

@[simp]

theorem MulEquiv.toSingleObjEquiv_inverse_obj {M : Type u} {N : Type v} [Monoid M] [Monoid N] (e : M ≃* N) (a : CategoryTheory.SingleObj N) : e.toSingleObjEquiv.inverse.obj a = a

@[simp]

theorem MulEquiv.toSingleObjEquiv_counitIso_hom {M : Type u} {N : Type v} [Monoid M] [Monoid N] (e : M ≃* N) : e.toSingleObjEquiv.counitIso.hom = CategoryTheory.eqToHom ⋯

@[simp]

theorem MulEquiv.toSingleObjEquiv_counitIso_inv {M : Type u} {N : Type v} [Monoid M] [Monoid N] (e : M ≃* N) : e.toSingleObjEquiv.counitIso.inv = CategoryTheory.eqToHom ⋯

@[simp]

theorem MulEquiv.toSingleObjEquiv_functor_obj {M : Type u} {N : Type v} [Monoid M] [Monoid N] (e : M ≃* N) (a : CategoryTheory.SingleObj M) : e.toSingleObjEquiv.functor.obj a = a

def Units.toAut (M : Type u) [Monoid M] : Mˣ ≃* CategoryTheory.Aut (CategoryTheory.SingleObj.star M)

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

@[simp]

theorem Units.toAut_hom (M : Type u) [Monoid M] (x : Mˣ) : ((toAut M) x).hom = (CategoryTheory.SingleObj.toEnd M) ↑x

@[simp]

theorem Units.toAut_inv (M : Type u) [Monoid M] (x : Mˣ) : ((toAut M) x).inv = (CategoryTheory.SingleObj.toEnd M) ↑x⁻¹

def MonCat.toCat : CategoryTheory.Functor MonCat CategoryTheory.Cat

The fully faithful functor from MonCat to Cat.

instance MonCat.toCat_full : toCat.Full

instance MonCat.toCat_faithful : toCat.Faithful