mathlib3 documentation

category_theory.single_obj

Single-object category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Single object category with a given monoid of endomorphisms. It is defined to facilitate transfering some definitions and lemmas (e.g., conjugacy etc.) from category theory to monoids and groups.

Main definitions #

Given a type α with a monoid structure, single_obj α is unit type with category structure such that End (single_obj α).star is the monoid α. This can be extended to a functor Mon ⥤ Cat.

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

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

Implementation notes #

source
@[reducible]
def category_theory.single_obj (α : Type u_1) :
Type

Abbreviation that allows writing category_theory.single_obj rather than quiver.single_obj.

source
@[protected, instance]
def category_theory.single_obj.category_struct (α : Type u) [has_one α] [has_mul α] :
category_theory.category_struct (category_theory.single_obj α)

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

Equations
source
@[protected, instance]
def category_theory.single_obj.category (α : Type u) [monoid α] :
category_theory.category (category_theory.single_obj α)

Monoid laws become category laws for the single object category.

Equations
source
theorem category_theory.single_obj.id_as_one (α : Type u) [monoid α] (x : category_theory.single_obj α) :
𝟙 x = 1
source
theorem category_theory.single_obj.comp_as_mul (α : Type u) [monoid α] {x y z : category_theory.single_obj α} (f : x ⟶ y) (g : y ⟶ z) :
f ≫ g = g * f
source
@[protected, instance]
def category_theory.single_obj.groupoid (α : Type u) [group α] :
category_theory.groupoid (category_theory.single_obj α)

Groupoid structure on single_obj α.

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

Equations
source
theorem category_theory.single_obj.inv_as_inv (α : Type u) [group α] {x y : category_theory.single_obj α} (f : x ⟶ y) :
category_theory.inv f = f⁻¹
source
@[reducible]
def category_theory.single_obj.star (α : Type u) :
category_theory.single_obj α

Abbreviation that allows writing category_theory.single_obj.star rather than quiver.single_obj.star.

source
def category_theory.single_obj.to_End (α : Type u) [monoid α] :
α ≃* category_theory.End (category_theory.single_obj.star α)

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

Equations
source
theorem category_theory.single_obj.to_End_def (α : Type u) [monoid α] (x : α) :
⇑(category_theory.single_obj.to_End α) x = x
source
def category_theory.single_obj.map_hom (α : Type u) (β : Type v) [monoid α] [monoid β] :
(α →* β) ≃ category_theory.single_obj α ⥤ category_theory.single_obj β

There is a 1-1 correspondence between monoid homomorphisms α → β and functors between the corresponding single-object categories. It means that single_obj 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
source
theorem category_theory.single_obj.map_hom_id (α : Type u) [monoid α] :
⇑(category_theory.single_obj.map_hom α α) (monoid_hom.id α) = 𝟭 (category_theory.single_obj α)
source
theorem category_theory.single_obj.map_hom_comp {α : Type u} {β : Type v} [monoid α] [monoid β] (f : α →* β) {γ : Type w} [monoid γ] (g : β →* γ) :
⇑(category_theory.single_obj.map_hom α γ) (g.comp f) = ⇑(category_theory.single_obj.map_hom α β) f ⋙ ⇑(category_theory.single_obj.map_hom β γ) g
source
@[simp]
theorem category_theory.single_obj.difference_functor_map {C : Type u_1} {G : Type u_2} [category_theory.category C] [group G] (f : C → G) (x y : C) (_x : x ⟶ y) :
(category_theory.single_obj.difference_functor f).map _x = f y * (f x)⁻¹
source
def category_theory.single_obj.difference_functor {C : Type u_1} {G : Type u_2} [category_theory.category C] [group G] (f : C → G) :
C ⥤ category_theory.single_obj 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
source
@[simp]
theorem category_theory.single_obj.difference_functor_obj {C : Type u_1} {G : Type u_2} [category_theory.category C] [group G] (f : C → G) (_x : C) :
(category_theory.single_obj.difference_functor f).obj _x = unit.star()
source
@[reducible]
def monoid_hom.to_functor {α : Type u} {β : Type v} [monoid α] [monoid β] (f : α →* β) :
category_theory.single_obj α ⥤ category_theory.single_obj β

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

Equations
source
@[simp]
theorem monoid_hom.id_to_functor (α : Type u) [monoid α] :
(monoid_hom.id α).to_functor = 𝟭 (category_theory.single_obj α)
source
@[simp]
theorem monoid_hom.comp_to_functor {α : Type u} {β : Type v} [monoid α] [monoid β] (f : α →* β) {γ : Type w} [monoid γ] (g : β →* γ) :
(g.comp f).to_functor = f.to_functor ⋙ g.to_functor
source
def units.to_Aut (α : Type u) [monoid α] :
αˣ ≃* category_theory.Aut (category_theory.single_obj.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.

Equations
source
@[simp]
theorem units.to_Aut_hom (α : Type u) [monoid α] (x : αˣ) :
(⇑(units.to_Aut α) x).hom = ⇑(category_theory.single_obj.to_End α) ↑x
source
@[simp]
theorem units.to_Aut_inv (α : Type u) [monoid α] (x : αˣ) :
(⇑(units.to_Aut α) x).inv = ⇑(category_theory.single_obj.to_End α) ↑x⁻¹
source
def Mon.to_Cat  :
Mon ⥤ category_theory.Cat

The fully faithful functor from Mon to Cat.

Equations
Instances for Mon.to_Cat
source
@[protected, instance]
def Mon.to_Cat_full  :
category_theory.full Mon.to_Cat
Equations
source
@[protected, instance]
def Mon.to_Cat_faithful  :
category_theory.faithful Mon.to_Cat