9.6 Strict categories

Definition 9.6.1.

A strict categoryis 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 extensionof 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 theorysays that these two precategories are isomorphic (not merely equivalent).

单词	96StrictCategories
释义	9.6 Strict categories Definition 9.6.1. A strict categoryis 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 extensionof 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 theorysays that these two precategories are isomorphic (not merely equivalent).
随便看	ProthNumber Proth number ProthPrime Proth prime ProuhetThueMorseConstant Prouhet-Thue-Morse constant ProuhetThueMorseSequence Prouhet-Thue-Morse sequence ProvingThalesTheoremWithVectors proving Thales’ theorem with vectors ProximalNeighborhood proximal neighborhood ProximityContinuous proximity continuous ProximityGeneratedByUniformity proximity generated by uniformity ProximitySpace proximity space PruferDomain PruferRing Prüfer domain Prüfer ring PseudocompactSpace pseudocompact space Pseudocomplement