9.6 Strict categories
A strict category is a precategory whose type of objects is a set.
In accordance with the mathematical red herring principle, a strict category is not necessarily a category. In fact, a category is a strict category precisely when it is gaunt (\autorefct:gaunt). Most of the time, category theory is about categories, not strict ones, but sometimes one wants to consider strict categories. The main advantage of this is that strict categories have a stricter notion of “sameness” than equivalence, namely isomorphism (or equivalently, by \autorefct:cat-eq-iso, equality).
Here is one origin of strict categories.
Let be a precategory and an object. Then there is a precategory as follows:
Its objects consist of an object and a monomorphism . (As usual, is a monomorphism (or is monic) if .)
Its morphisms from to are arbitrary morphisms from to in (not necessarily respecting and ).
An equality of objects in consists of an equality and an equality , which by \autorefct:idtoiso-trans is equivalently an equality . Since hom-sets are sets, the type of such equalities is a mere proposition. But since and are monomorphisms, the type of morphisms such that is also a mere proposition. Thus, if is a category, then is a mere proposition, and hence is a strict category.
This example can be dualized, and generalized in various ways. Here is an interesting application of strict categories.
Let be a finite Galois extension of fields, and its Galois group. Then there is a strict category whose objects are intermediate fields , and whose morphisms are field homomorphisms which fix pointwise (but need not commute with the inclusions into ). There is another strict category whose objects are subgroups , and whose morphisms are morphisms of -sets . The fundamental theorem of Galois theory says that these two precategories are isomorphic (not merely equivalent).
|Title||9.6 Strict categories|