Single-object category
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
category_struct.componEnd (single_obj.star α)isflip (*), not(*). This way multiplication onEndagrees with the multiplication onα.By default, Lean puts instances into
category_theorynamespace instead ofcategory_theory.single_obj, so we give all names explicitly.
One and flip (*) become id and comp for morphisms of the single object category.
Equations
- category_theory.single_obj.category_struct α = {to_has_hom := {hom := λ (_x _x : category_theory.single_obj α), α}, id := λ (_x : category_theory.single_obj α), 1, comp := λ (_x _x_1 _x_2 : category_theory.single_obj α) (x : _x ⟶ _x_1) (y : _x_1 ⟶ _x_2), y * x}
Monoid laws become category laws for the single object category.
Equations
- category_theory.single_obj.category α = {to_category_struct := category_theory.single_obj.category_struct α (semigroup.to_has_mul α), id_comp' := _, comp_id' := _, assoc' := _}
Groupoid structure on single_obj α
Equations
- category_theory.single_obj.groupoid α = {to_category := {to_category_struct := category_theory.single_obj.category_struct α (semigroup.to_has_mul α), id_comp' := _, comp_id' := _, assoc' := _}, inv := λ (_x _x_1 : category_theory.single_obj α) (x : _x ⟶ _x_1), x⁻¹, inv_comp' := _, comp_inv' := _}
The single object in single_obj α.
Equations
The endomorphisms monoid of the only object in single_obj α is equivalent to the original
monoid α.
Equations
- category_theory.single_obj.to_End α = {to_fun := (equiv.refl α).to_fun, inv_fun := (equiv.refl α).inv_fun, left_inv := _, right_inv := _, map_mul' := _}
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.
Equations
- category_theory.single_obj.map_hom α β = {to_fun := λ (f : α →* β), {obj := id (category_theory.single_obj α), map := λ (_x _x : category_theory.single_obj α), ⇑f, map_id' := _, map_comp' := _}, inv_fun := λ (f : category_theory.single_obj α ⥤ category_theory.single_obj β), {to_fun := f.map (category_theory.single_obj.star α), map_one' := _, map_mul' := _}, left_inv := _, right_inv := _}
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
- f.to_functor = ⇑(category_theory.single_obj.map_hom α β) f
The units in a monoid are (multiplicatively) equivalent to
the automorphisms of star when we think of the monoid as a single-object category.
The fully faithful functor from Mon to Cat.
Equations
- Mon.to_Cat = {obj := λ (x : Mon), category_theory.Cat.of (category_theory.single_obj ↥x), map := λ (x y : Mon) (f : x ⟶ y), ⇑(category_theory.single_obj.map_hom ↥x ↥y) f, map_id' := Mon.to_Cat._proof_1, map_comp' := Mon.to_Cat._proof_2}
Equations
- Mon.to_Cat_full = {preimage := λ (x y : Mon), (category_theory.single_obj.map_hom ↥x ↥y).inv_fun, witness' := Mon.to_Cat_full._proof_1}