nLab strict category

Redirected from "strict groupoids".
Strict categories

Strict categories

Idea

A strict category is a category together with the structure of a set (or class) on its collection of objects; in particular, the objects can be compared for equality (not merely isomorphism). In contrast, a weak category is a category without such structure. Similarly, a strict functor is one which preserves equality of objects: F(x)=F(y)F(x) = F(y) if x=yx = y. (NB: this is not inherently size-related—both large and small categories can be either strict or weak.)

If we use set-theoretic foundations for category theory, then by definition, a category comes with a set (or class) of objects, and therefore admits the structure of a strict category in a canonical way. Thus, in this case, it is possible to ignore the adjective “strict” in “strict category”, while a “strict functor” simply means a “non-ana functor” (the usual default meaning of ‘functor’, but not necessarily the best concept).

If we additionally assume the (possibly global) axiom of choice, then not only is any category equivalent to a canonical strict category, but every (ana-)functor is naturally isomorphic to a strict functor, so the notions have little to no mathematical content. But in other foundations, these facts may not be true.

Moreover, even in set-theoretic foundations with global ACAC, the notion of strict category is not meaningless: calling a category strict signals that we intend to make use of the equality relation on its objects. When taking the nPOV, we often adopt the philosophical position that category theory is fundamentally about weak categories; see the discussion at principle of equivalence. However, strict categories still do occasionally arise in mathematical practice; see the examples below.

Definition

In order to formulate a foundation-independent definition, we make the following assumptions. Ignoring size issues, suppose that we have a bicategory CatCat consisting of weak categories, functors (some of which are essentially surjective), and natural transformations (some of which are natural isomorphisms). Suppose also that we have a category SetSet consisting of sets and functions, and a functor Disc:SetCatDisc\colon Set \to \Cat taking each set to the discrete category on that set. Note that we do not assume the existence of an “underlying set of objects” functor CatSetCat\to Set.

In this context, a strict category CC consists of

  • a set Ob(C)Ob(C) (to be thought of as the set of objects of CC),
  • a category Wk(C)Wk(C) (to be thought of as the underlying weak category of CC), and
  • an essentially surjective functor cl(C):Disc(Ob(C))Wk(C)cl(C)\colon Disc(Ob(C)) \to Wk(C) (to be thought of as taking each object of CC to its clique, more or less, in CC).

A strict functor FF from CC to DD (both strict categories) consists of

  • a function Ob(F):Ob(C)Ob(D)Ob(F)\colon Ob(C) \to Ob(D),
  • a functor Wk(F):Wk(C)Wk(D)Wk(F)\colon Wk(C) \to Wk(D), and
  • a natural isomorphism cl(F):cl(C);Wk(F)Disc(Ob(F));cl(D)cl(F)\colon cl(C) ; Wk(F) \to Disc(Ob(F)) ; cl(D).

Two strict functors F,G:CDF, G\colon C \to D are equal if

  • Ob(F)=Ob(G)Ob(F) = Ob(G) and
  • there is a (necessarily unique) natural isomorphism from Wk(F)Wk(F) to Wk(G)Wk(G) modulo which cl(F)cl(F) equals cl(G)cl(G).

There is an obvious notion of composition that defines a 1-category StrCatStr Cat of strict categories and (equality classes of) strict functors. Note that this 1-category has a strictly associative and unital composition law, even if CatCat is only a bicategory. (However, StrCatStr Cat is not itself a strict category, unless the assumed category SetSet is strict.) We have a forgetful functor Ob:StrCatSetOb\colon Str Cat \to Set and a pseudofunctor Wk:StrCatCatWk\colon Str Cat \to Cat.

Finally, a natural transformation between two strict functors FF and GG is simply

  • a natural transformation from Wk(F)Wk(F) to Wk(G)Wk(G).

(That is, a natural transformation between strict functors is automatically strict.) With these as 2-cells, we have a strict 2-category of strict categories, strict functors, and natural transformations.

Remark

An equivalent definition is that a strict category is an \mathcal{M}-category whose underlying category of tight morphisms is discrete, while a strict functor is an \mathcal{M}-functor. In this case, the tight morphisms (which are necessarily isomorphisms) are sometimes called special isomorphisms.

Foundational choices

We now make the above schematic definition explicit in terms of various different foundational systems.

Set theory with AC

In classical set-theoretic foundations including the axiom of choice, we take CatCat to be the strict 2-category consisting of (say small) categories, functors, and natural transformations, defined in any of the traditional ways. The functor Disc:SetCatDisc\colon Set \to Cat is left adjoint to the functor Ob:CatSetOb\colon Cat \to Set, and thus StrCatStr Cat is a subcategory of the Freyd cover of CatCat.

In this case, the functor Wk:StrCatCatWk\colon Str Cat \to Cat has a right adjoint which takes a category CC to the strict category Disc(Ob(C))CDisc(Ob(C)) \to C. The adjunction counit is literally the identity, while the adjunction unit consists of equivalences (but not isomorphisms) in the strict 22-category StrCatStr Cat. Thus, StrCatStr Cat is equivalent to CatCat (as a bicategory).

The right adjoint CatStrCatCat \to Str Cat also has a further right adjoint defined as follows: given a strict category CC, let CC' be the category with Ob(C)Ob(C) as its set of objects, and morphisms induced from those in Wk(C)Wk(C). The unit of this adjunction again consists of identities, while the counit consists of equivalences in StrCatStr Cat.

This analysis applies not only to material set theories such as ZFC, but also structural set theories such as ETCS and SEAR, as long as they have the axiom of choice.

Set theory without AC

In this case, it is usually best to define Cat to be the bicategory of categories, anafunctors, and natural transformations. Now although every category has an underlying set of objects, we no longer have a functor Ob:CatSetOb\colon Cat \to Set. It is still true that every category CC admits the structure of a strict category in a canonical way (with Ob(C)Ob(C) its set of objects), but not every strict category necessarily arises in this way, and not every morphism CDC \to D in CatCat (i.e. anafunctor) is a strict functor relative to the canonical strict-category structures of CC and DD. In fact, an anafunctor is a strict functor precisely when it is naturally isomorphic to an ordinary (non-ana) functor.

If we instead defined CatCat to consist only of non-ana functors, then everything would happen exactly as with AC, except that neither adjunction would be an equivalence.

Type and preset theories with equality

We include under this heading all theories in which the basic objects, generally called types or presets (and sometimes even called ‘sets’), come with an equality relation, but the notion of set is a defined one. Generally, the issue is that types (or presets) do not admit quotients, and so a set is defined to be a type equipped with an equivalence relation called “equality” (sometimes called a setoid in this context, especially if the types or presets are themselves confusingly called ‘sets’).

In this case, it is natural to define a category to have only a type/preset of objects, but a set(oid) of morphisms between each pair of objects; see type-theoretic definition of category. Now every category still has an underlying set of objects, but not every set is the set of objects underlying some category; only the completely presented sets have this property.

Again, it is true that every category can be made into a strict one in a canonical way, but that not every strict category arises in this way. This is a different sort of failure than in set theory without ACAC, and can happen even in the presence of full ACAC (even for setoids). For instance, consider the discrete category on the set of real numbers. Of course this depends on specifics, but typically, there is no type of real numbers per se but only a type of Cauchy (pre)sequences of rational numbers (see Cauchy real number). To get the set of real numbers, we must consider this type together with a certain equivalence relation, a setoid. The discrete category on the set of real numbers is essentially the exact same construction, now with a note that parallel morphisms are always defined to be equal. The automatic notion of equality on the objects of this category is equality of Cauchy (pre)sequences, but the desired notion of equality for this discrete category as a strict category is isomorphism, which is equality of real numbers. So while this category may be automatically a strict category, it is a strict category in the wrong way. (This is not a perfect example, since, given ACAC, the discrete category of real numbers is still equivalent to the discrete category of Cauchy sequences and therefore does arise as a canonical strict category, up to equivalence.)

Note that we still have a functor Disc:SetCatDisc\colon Set \to Cat which regards an equivalence relation on a type AA as a groupoid with AA as its type of objects. The resulting structure of strict categories behaves much like it does in set theory without AC.

Type and preset theories without equality

If types or presets do not come with a notion of equality, as in some preset theories and SEAR+?, then a category does not in general even have an “underlying set of objects”, so a category cannot be made into a strict category in any canonical way. But defining sets as presets with equivalence relations as before, we still have Disc:SetCatDisc\colon Set \to Cat, and we can define strict categories, constructing specific examples as wanted.

Homotopy type theory

If type theory is treated as a theory of set-like objects, then it behaves as above, whether extensional or intensional. However, if we take the point of view of homotopy type theory, then the basic objects of the theory are homotopy types, a.k.a. ∞-groupoids. A set is now defined to be an h-set, i.e. a 0-truncated type.

Now the natural definition of (1-)category is something like a complete Segal space, where the type of objects is 1-truncated (a groupoid) and equivalent to the core of the category. Now (even though identity types exist in HoTT), not every category has an underlying set of objects, so again a category cannot be made into a strict category in any canonical way. But again, we still have Disc:SetCatDisc\colon Set \to Cat and we can define strict categories.

Fibered categories

In Jean Bénabou‘s 1985 paper Fibered categories and the foundations of naive category theory?, it is argued that the right notion of a category in/over another category B\mathbf{B} is given by a fibered category p:FBp\colon \mathbf{F} \to \mathbf{B}, possibly with some additional structure corresponding to the “definability” (representability of certain sieves of B\mathbf{B}) of equality of parallel pairs, isomorphisms, etc. (See indexed category for more motivation.) In this context, equality of objects is available precisely when the fibration is split.

In particular, if B\mathbf{B} is locally small and has pullbacks, then an internal category object CC in B\mathbf{B} (in the traditional sense) gives rise to an honest functor B(,C):B opCat\mathbf{B} (-, C)\colon \mathbf{B}^{op} \to Cat and so a split fibration BB(,C)B\int_\mathbf{B} \mathbf{B} (-, C) \to \mathbf{B} by the Grothendieck construction.

Examples

There are some at M-category, to put also here.

Strict higher categories

The notion of strict category is related to the notion of strictness in higher category theory.

For instance, a 2-category must have strict categories as its hom-categories in order to write down the definition of strict 2-category; a similar remark holds for strict 2-functors. As such, strictness in the sense of this page matches the usual sense of strictness in a “local” sense (every strict 2-category is locally a strict 1-category). However, we now get a notion of strict 22-natural transformation as a 2-natural transformation that preserves equality (that is, if two objects are equal, then so are the corresponding components of the natural transformation). (All modifications between strict transformations are automatically strict … until we get to 33-categories, of course!)

On the other hand, the underlying 1-category of a strict 2-category (its objects and 1-morphisms) need not be a strict 1-category. For instance, this is the case for the strict 2-category StrCatStr Cat defined in a structural set theory, such as SEAR, in which there is no equality predicate on sets. For a fully consistent terminology, we could say ‘locally strict 22-category’ in place of ‘strict 22-category’, but this is unlikely to catch on. Some system of numbered strictness (11-strict, 22-strict, etc) might also work.

Last revised on May 16, 2022 at 06:34:50. See the history of this page for a list of all contributions to it.