Documentation

Mathlib.CategoryTheory.SingleObj

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] :

CategoryStruct.{u, 0} (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] :

Category.{u, 0} (SingleObj M)

Monoid laws become category laws for the single object category.

Equations

CategoryTheory.SingleObj.category M = { toCategoryStruct := CategoryTheory.SingleObj.categoryStruct M, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

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

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.

Equations

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

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

Groupoid (SingleObj G)

Groupoid structure on SingleObj M.

Stacks Tag 0019

Equations

CategoryTheory.SingleObj.groupoid G = { toCategory := CategoryTheory.SingleObj.category G, inv := fun {X Y : CategoryTheory.SingleObj G} (x : X ⟶ Y) => x⁻¹, inv_comp := ⋯, comp_inv := ⋯ }

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

@[reducible, inline]

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

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 ≃* End (star M)

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

Equations

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

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.

Stacks Tag 001F (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] :

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

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

@[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✝ = ()

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.

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

Equations

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

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

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] :

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

Equations

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

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

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ˣ) :

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

Equations

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

instance MonCat.toCat_full :

instance MonCat.toCat_faithful :