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 categoryMathworldPlanetmath. In fact, a category is a strict category precisely when it is gaunt (\autorefct:gaunt). Most of the time, category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath 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 isomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath (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 mono(A,x) as follows:

  • Its objects consist of an object y:A and a monomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmath m:homA(y,x). (As usual, m:homA(y,x) is a monomorphism (or is monic) if (mf=mg)(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 mono(A,x) consists of an equality p:y=z and an equality p*(m)=n, which by \autorefct:idtoiso-trans is equivalently an equality m=nidtoiso(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=nf is also a mere proposition. Thus, if A is a category, then (y,m)=(z,n) is a mere proposition, and hence 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 extensionMathworldPlanetmath of fields, and G its Galois group. Then there is a strict category whose objects are intermediate fields FKE, 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 HG, and whose morphisms are morphisms of G-sets G/HG/K. The fundamental theorem of Galois theoryMathworldPlanetmath says that these two precategories are isomorphic (not merely equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath).

Title 9.6 Strict categories