9.6 Strict categories

Definition 9.6.1.

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 (ct: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 ct:cat-eq-iso, equality).

Here is one origin of strict categories.

Example 9.6.2.

Let $A$ be a precategory and $x\mathrm{:}A$ an object. Then there is a precategory $\mathrm{mono}\mathit{}\mathrm{(}A\mathrm{,}x\mathrm{)}$ as follows:

• Its objects consist of an object $y:A$ and a monomorphism $m:{\mathrm{hom}}_A(y,x)$. (As usual, $m:{\mathrm{hom}}_A(y,x)$ is a monomorphism (or is monic) if $(m\circ f=m\circ g)\Rightarrow (f=g)$.)

• Its morphisms from $(y,m)$ to $(z,n)$ are arbitrary morphisms from $y$ to $z$ in $A$ (not necessarily respecting $m$ and $n$).

An equality $\mathrm{(}y\mathrm{,}m\mathrm{)}\mathrm{=}\mathrm{(}z\mathrm{,}n\mathrm{)}$ of objects in $\mathrm{mono}\mathit{}\mathrm{(}A\mathrm{,}x\mathrm{)}$ consists of an equality $p\mathrm{:}y\mathrm{=}z$ and an equality $p_{\mathrm{*}}\mathrm{\left(}m\mathrm{\right)}\mathrm{=}n$, which by ct:idtoiso-trans is equivalently an equality $m\mathrm{=}n\mathrm{\circ }\mathrm{idtoiso}\mathit{}\mathrm{(}p\mathrm{)}$. Since hom-sets are sets, the type of such equalities is a mere proposition. But since $m$ and $n$ are monomorphisms, the type of morphisms $f$ such that $m\mathrm{=}n\mathrm{\circ }f$ is also a mere proposition. Thus, if $A$ is a category, then $\mathrm{(}y\mathrm{,}m\mathrm{)}\mathrm{=}\mathrm{(}z\mathrm{,}n\mathrm{)}$ is a mere proposition, and hence $\mathrm{mono}\mathit{}\mathrm{(}A\mathrm{,}x\mathrm{)}$ is a strict category.

This example can be dualized, and generalized in various ways. Here is an interesting application of strict categories.

Example 9.6.3.

Let $E\mathrm{/}F$ be a finite Galois extension of fields, and $G$ its Galois group. Then there is a strict category whose objects are intermediate fields $F\mathrm{\subseteq }K\mathrm{\subseteq }E$, and whose morphisms are field homomorphisms which fix $F$ pointwise (but need not commute with the inclusions into $E$). There is another strict category whose objects are subgroups $H\mathrm{\subseteq }G$, and whose morphisms are morphisms of $G$-sets $G\mathrm{/}H\mathrm{\to }G\mathrm{/}K$. The fundamental theorem of Galois theory says that these two precategories are isomorphic (not merely equivalent).

Title	9.6 Strict categories