A discrete category is a Category with no morphisms other than identities. A discrete category is the same thing as a Set (“a bare-object category is a set: a category with no structure”, DaoFP §8.1; 7 Sketches Example 3.74: the discrete category on a set is a left adjoint to the underlying set). The Discrete Preorder is the thin case.
Sources: DaoFP §8.1, §10.11; 7 Sketches Example 3.74, 3.94, Exercise 3.83; Kittenlab Lecture 9; CTfS Example 4.1.2.32, Exercises 4.1.2.33–4.1.2.34, 4.3.2.6, 4.5.1.14, Example 4.5.3.10
- A Functor out of a discrete category is just a family of objects; a Diagram indexed by the discrete category with objects has as Limit the -fold Product and as Colimit the -fold Coproduct (Example 3.94; Kittenlab Lecture 9: “-ary coproducts by making the discrete category with objects”).
- The discrete category on two objects has no Terminal Object (7S Exercise 3.83).
- Counting (CTfS Exercises 4.1.2.33, 4.3.2.6): the discrete category on has exactly 4 morphisms (the identities); functors are just functions (there are 8), and there are no non-identity natural transformations between them, so the functor category is itself discrete with 8 objects. In a discrete category a product exists iff (CTfS Exercise 4.5.1.14).
- ; see Codiscrete Category.
#check CategoryTheory.Discrete -- Discrete α: objects α, only identity morphisms
#check CategoryTheory.Discrete.functor -- a family α → C gives Discrete α ⥤ C