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.

Equations

• CategoryTheory.SingleObj = Quiver.SingleObj

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

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.

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

Monoid laws become category laws for the single object category.

Equations

• CategoryTheory.SingleObj.category M = CategoryTheory.Category.mk ⋯ ⋯ ⋯

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

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

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

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

Equations

• CategoryTheory.SingleObj.finCategoryOfFintype M = { fintypeObj := inferInstance, fintypeHom := inferInstance }

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

Groupoid structure on SingleObj M.

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

Equations

• CategoryTheory.SingleObj.groupoid G = CategoryTheory.Groupoid.mk (fun {X Y : CategoryTheory.SingleObj G} (x : X ⟶ Y) => x⁻¹) ⋯ ⋯

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

@[reducible, inline]

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

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

Equations

• CategoryTheory.SingleObj.star M = Quiver.SingleObj.star M

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

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

Equations

• CategoryTheory.SingleObj.toEnd M = let __src := Equiv.refl M; { toEquiv := __src, map_mul' := ⋯ }

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

def CategoryTheory.SingleObj.mapHom (M : Type u) [Monoid M] (N : Type v) [Monoid N] : (M →* N) ≃ CategoryTheory.Functor (CategoryTheory.SingleObj M) (CategoryTheory.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.

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.

theorem CategoryTheory.SingleObj.mapHom_id (M : Type u) [Monoid M] : (CategoryTheory.SingleObj.mapHom M M) (MonoidHom.id M) = CategoryTheory.Functor.id (CategoryTheory.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) : (CategoryTheory.SingleObj.mapHom M P) (g.comp f) = ((CategoryTheory.SingleObj.mapHom M N) f).comp ((CategoryTheory.SingleObj.mapHom N P) g)

@[simp]

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

@[simp]

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

def CategoryTheory.SingleObj.differenceFunctor {G : Type u} [Group G] {C : Type v} [CategoryTheory.Category.{w, v} C] (f : C → G) : CategoryTheory.Functor C (CategoryTheory.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)⁻¹.

Equations

• CategoryTheory.SingleObj.differenceFunctor f = { obj := fun (x : C) => (), map := fun {x y : C} (x_1 : x ⟶ y) => f y * (f x)⁻¹, map_id := ⋯, map_comp := ⋯ }

@[simp]

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

@[simp]

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

def CategoryTheory.SingleObj.functor {M : Type u} [Monoid M] {C : Type v} [CategoryTheory.Category.{w, v} C] {X : C} (f : M →* CategoryTheory.End X) : CategoryTheory.Functor (CategoryTheory.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.

Equations

• CategoryTheory.SingleObj.functor f = { obj := fun (x : CategoryTheory.SingleObj M) => X, map := fun {X_1 Y : CategoryTheory.SingleObj M} (a : X_1 ⟶ Y) => f a, map_id := ⋯, map_comp := ⋯ }

@[simp]

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

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

• CategoryTheory.SingleObj.natTrans u h = { app := fun (x : CategoryTheory.SingleObj M) => u, naturality := ⋯ }

@[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.

Equations

• f.toFunctor = (CategoryTheory.SingleObj.mapHom M N) f

@[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] : (MonoidHom.id M).toFunctor = CategoryTheory.Functor.id (CategoryTheory.SingleObj M)

@[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

@[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_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_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_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_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_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_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

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.

Equations

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

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.

Equations

• Units.toAut M = (Units.mapEquiv (CategoryTheory.SingleObj.toEnd M)).trans (CategoryTheory.Aut.unitsEndEquivAut (CategoryTheory.SingleObj.star M))

@[simp]

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

@[simp]

theorem Units.toAut_inv (M : Type u) [Monoid M] (x : Mˣ) : ((Units.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.

Equations

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

instance MonCat.toCat_full : MonCat.toCat.Full

Equations

• MonCat.toCat_full = ⋯

instance MonCat.toCat_faithful : MonCat.toCat.Faithful

Equations

• MonCat.toCat_faithful = ⋯