# 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 (\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.

###### Example 9.6.2.

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

• Its objects consist of an object $y:A$ and a monomorphism $m:\hom_{A}(y,x)$. (As usual, $m:\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 $(y,m)=(z,n)$ of objects in $\mathsf{mono}(A,x)$ consists of an equality $p:y=z$ and an equality ${p}_{*}\mathopen{}\left({m}\right)\mathclose{}=n$, which by \autorefct:idtoiso-trans is equivalently an equality $m=n\circ\mathsf{idtoiso}(p)$. 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=n\circ f$ is also a mere proposition. Thus, if $A$ is a category, then $(y,m)=(z,n)$ is a mere proposition, and hence $\mathsf{mono}(A,x)$ 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/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\subseteq K\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\subseteq G$, and whose morphisms are morphisms of $G$-sets $G/H\to G/K$. The fundamental theorem of Galois theory says that these two precategories are isomorphic (not merely equivalent).

Title 9.6 Strict categories
\metatable