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

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

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

Implementation notes

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

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

@[inline, reducible]

abbrev CategoryTheory.SingleObj : Type u_1 → Type

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

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

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

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

Monoid laws become category laws for the single object category.

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

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

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

Groupoid structure on SingleObj α.

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

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

@[inline, reducible]

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

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

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

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

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

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

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

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

theorem CategoryTheory.SingleObj.mapHom_comp {α : Type u} {β : Type v} [Monoid α] [Monoid β] (f : α →* β) {γ : Type w} [Monoid γ] (g : β →* γ) : ↑(CategoryTheory.SingleObj.mapHom α γ) (MonoidHom.comp g f) = CategoryTheory.Functor.comp (↑(CategoryTheory.SingleObj.mapHom α β) f) (↑(CategoryTheory.SingleObj.mapHom β γ) g)

@[simp]

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

@[simp]

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

def CategoryTheory.SingleObj.differenceFunctor {C : Type u_1} {G : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [Group G] (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)⁻¹.

@[reducible]

def MonoidHom.toFunctor {α : Type u} {β : Type v} [Monoid α] [Monoid β] (f : α →* β) : CategoryTheory.Functor (CategoryTheory.SingleObj α) (CategoryTheory.SingleObj β)

Reinterpret a monoid homomorphism f : α → β as a functor (single_obj α) ⥤ (single_obj β). See also CategoryTheory.SingleObj.mapHom for an equivalence between these types.

@[simp]

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

@[simp]

theorem MonoidHom.comp_toFunctor {α : Type u} {β : Type v} [Monoid α] [Monoid β] (f : α →* β) {γ : Type w} [Monoid γ] (g : β →* γ) : MonoidHom.toFunctor (MonoidHom.comp g f) = CategoryTheory.Functor.comp (MonoidHom.toFunctor f) (MonoidHom.toFunctor g)

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

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 (α : Type u) [Monoid α] (x : αˣ) : (↑(Units.toAut α) x).hom = ↑(CategoryTheory.SingleObj.toEnd α) ↑x

@[simp]

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

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

The fully faithful functor from MonCat to Cat.

instance MonCat.toCatFull : CategoryTheory.Full MonCat.toCat

instance MonCat.toCat_faithful : CategoryTheory.Faithful MonCat.toCat