Schreiber categories, functors and natural transformations in SET

• previous chapter: motivation for sheaves, cohomology and higher stacks

• home: sheaves and stacks

• next chapter: presheaf categories with values in small sets

Urs, do you want comments here? I mean that, besides fixing typos and noting out-and-out mistakes, would you like me to make a note if I think that something you've said is poorly explained, or an unjustified conclusion, or so on? —Toby

Sure, I’d appreciate it. – Urs

---

The theme of this chapter is the fundamental concept category.

• we discuss an axiomatization of set theory in terms of an axiomatization of the behaviour of functions between sets: the

Elementary Theory of the Category of Sets, $SET$;

• we then define categories, functors and natural transformations

internal to$SET$;

• we list some important constructions and examples in this context

• we end by characterizing equivalence of categories:

  • every category has a skeleton: an equivalent category in which all isomorphic objects are equal;

  • a functor between categories is an equivalence precisely if it is

  fullyfaithful and essentially surjective

• the next chapter then defines “categories of small sets” and categories of functors with values in these: presheaves

Introductory words on the need and role of foundations

• sheaves $\stackrel{requires}{\to}$ category theory $\stackrel{requires}{\to}$ foundations

We need the language of category theory in order to talk about sheaves. This language is very fundamental to mathematics, so much that in the course of setting it up one has to consider foundational issues: all of mathematics is supposed to be chain of rigorous deduction, but some very basic concepts need to be assumed be be universally understood by grace, and all deduction is based on these universally understood concepts.

• global nature of inclusion relation $\in$ in standard set theory is problematic

This basic concept has traditionally be taken to be that of a collection of elements – a set – with a global binary relation – $\in$ – that determines which sets are elements of other sets. Naïve and obvious as it may seem, there is famously some subtlety hidden here, related to the global nature of the inclusion relation.

• category theory suggests a structural approach

After the advent of category theory it was realized by Lawvere and others, that, roughly, what is truly fundamental is not so much the concept of a set itself, but rather the interrelation between sets in terms of the functions between them. The behaviour of these functions is axiomatized by saying that they form the Category of Sets, denoted $SET$. This notion is the fundamental elementary notion for all the following development: all further constructions take place inside $SET$.

• advantage: different attitudes towards foundations are captured in a unified way

One advantage of this perspective is that it allows to naturally address and handle concerns and disagreement about what actually does count as naive and universally accepted basis of all reasoning. This is because the crucial property of the Category of Sets $SET$ is that it is a topos: a “place” in which mathematics may be developed. When one strictly sticks to constructions within SET, as opposed to, say, the traditional Zermelo-Fraenkel axiomatics for set theory, then essentially all constructions and results make sense internal to any other topos. For instance constructivism is a school of thought which asserts that some axioms about naïve sets are not quite naïve enough and reject them, notably the axiom of excluded middle. This point of view turns out to be perfectly compatible, and in fact enforced, by the topos-theoretic perspective on foundations.

In setting up the concept $SET$ we will deal with elementary concepts in category theory such as category, product, coproduct etc. in a naïve fashion: these constructions are formulated in terms of collections of entities such as “arrows” or “functions” in a way that is supposed to be “universally understood by grace”, very analogous to the way traditional Zermelo-Fraenkel axiomatics assumes that it is “universally understood by grace” what it means for an entity to be element of some set. It is in a second step, when we systematically set up category theory internal to $SET$ that these constructions appear again in terms of formal definitions inside $SET$ itself, or more precisely inside of universes in $SET$.

Elementary Theory of the Category of Sets

• The Elementary Theory of the Category of Sets – ETCS for short – is a “structural” formalization of set theory which combines the rich tradition of naïve (= pre-axiomatic) set theory with the insights of category theory;

• literature:

  • Lawvere and Rosebrugh: Sets for Mathematics, Cambridge University Press

  • Todd Trimble: ETCS I, II, III

• ETCS differs from non-structural material set theory in the way it handles the membership relation $\in$:

  • in ETCS “sets” and “elemens” are of different type: not every element of a set is necessarily a set itself;

  • no element exists in isolation: it always exists relative to the set that it is an element of.

  • a notion of generalized element that comes with its domain of definition plays a crucial role: such generalized elements are just another perspective on functions between sets – called morphisms in $SET$ – and these functions are taken to be the primary concept, while the ordinary notion of an ordinary element of a set is a derived concept;

  • this is a general category theoretic perspective: what matters is the relational structure encoded in the morphisms $S \to T$, and not any imagined “inner structure” of the objects $S$, $T$:

this inner structure, the the extent that it makes sense to speak of it, is determined by the behaviour of the morphisms.

• in techical terms, which will not concern us further for the time being, the Categroy of Sets $SET$ to be described now is

  • a topos;

  • which is well-pointed;

  • satisfies the axiom of choice;

  • and is equipped with a natural numbers object

Now the definition.

The stuff and structure of SET

SET consists of

• a collection of “objects” called “sets” and usually denoted by capital letters, often from the middle of the alphabet $S, T, \cdots$;

• a collection of “arrows” called “morphisms” or “functions” that go between pairs of objects, denoted $f : S \to T$ etc.

  • for every object $S$ a morphism denoted $Id_S : S \to S$, called the identity function on $S$;

• a composition operation $(R \stackrel{f}{\to} S , S \stackrel{g}{\to} T) \mapsto (R \stackrel{g \circ f}{\to} T)$ on all pairs of composable morphisms;

  • such that the associativity law is respected: composition of any three composable morphisms $R \stackrel{f_1}{\to}S \stackrel{f_2}{\to} T \stackrel{f_3}{\to}U$ is uniquely defined;

  • such that the morphisms of the form $Id_S$ are units with respect to this compositon: $S \stackrel{Id_S}{\to} S \stackrel{f}{\to} T = S \stackrel{f}{\to} T = S \stackrel{f}{\to} T \stackrel{Id_T}{\to} T$;

Remark to those readers who already know categories: So far this would say that SET is a category: but the point is that we take the above as a primitive notion and avoid saying “it is a category with a set/class of objects, etc.”. Rather, ETCS is thought of as having a “collection” of objects in a pre-axiomatic sense. The possibly familiar notion of a small or large

category appears below as a concept internal to SET.

Notation

• A function $s : T \to S$ we also call an element $s \in S$ of $S$ with domain $T$ (or “stage of definition” $T$).

• If we allow ourselves to denote comopsition $g \circ f$ simply by juxtaposition $g f := g \circ f$ then for $f : S \to T$ a function and $x : U \to S$ another function regarded as an element of $S$ over domain of definition $U$, the notation $f x : U \to T$ denotes consistently both the composition of two functions and the application of the function $f$ to the element $x$.

  • This is the sense in which ETCS is “structural”: there is no separate notion of element, everything is in the relational structure defined by composition of morphisms.

Terminology and further concepts

• A morphism $f : S \to T$ is a

monomorphism if for every

$x : U \to S$ and $y : U \to S$, $f \circ x = f \circ y$ implies $x = y$.

• In different but equivalent language: a function $f: S \to T$ is injective if for all elements $x, y \in S$ over the same domain, $f x = f y$ implies $x = y$.

• A morphism $f : S \to T$ is an

epimorphism if for every

$g : T \to R$ and $h : T \to R$ the condition $g \circ f = h \circ f$ implies $g = h$.

• In different but equivalent language: a function $f: S \to T$ is surjective if it is a monomorphism.

• a morphism $f : S \to T$ is an isomorphism if there exists a morphism $f^{-1} : T \to S$ such that $f f^{-1} = Id_T$ and $f^{-1} f = Id_S$.

  • in terms of functions of sets an isomorphism is called a bijection.

After the defining properties on $SET$ are imposed in the following section, all these notions will reproduce their expected familar meaning.

• Given a monomorphism $i: S \to T$ we may think of it as defining a subset $S$ of $T$, whose (generalized) elements correspond to those elements $z \in T$ which factor (evidently uniquely) through $i$. It is in that sense that we say $z \in T$ also “belongs to” a subset $S$, while, contrary to non-structural

set theory, strictly speaking

every element in the language of ETCS is element only of one single set.

• A relation from $S$ to $T$ is an injective function or subset $R \hookrightarrow S \times T$.

The above structure of SET is required to satisfy the following axioms.

The properties of SET

Axiom of products.

• Set admits finite products.

• This means first of all: For any two sets $S, T$, there is a set $C$ and functions $p_1: C \to S$, $p_2: C \to T$, such that given two elements $x \in S, y \in T$ over the same domain, there exists a unique element $\langle x, y \rangle \in C$ over that domain for which

$$p_1\langle x, y \rangle = x \qquad p_2\langle x, y \rangle = y$$

• In terms of morphisms this means: given two morphisms $x : U \to S$ and $y : U \to T$ , there exists a unique morphism $\langle x, y \rangle : U \to C$ such that the following diagram commutes

$$\array{ && U \\ & {}^x \swarrow &\downarrow^{\langle x , y \rangle}& \searrow^{y} \\ S &\stackrel{p_1}{\leftarrow}& C &\stackrel{p_2}{\to}& T }$$

Notice that the crucial condition is that $\langle x,y\rangle$ exists and exists uniquely. This witnesses the universal property of the product.

A choice of product $C$ is usually denoted $S \times T$. To make a bridge with naive set-theory notation, we may suggestively write

$$S \times T :=_i \{\langle x, y \rangle: x \in S, y \in T\}$$

where the funny equality sign and bracketing notation on the right simply mean that the cartesian product is uniquely defined up to isomorphism by its collection of (generalized) elements, which correspond to pairs of elements.

• Moreover, admitting finite products also means that the empty product exists: there is an object $*$ in Set

  • which has a unique element $x \in *$ over any domain;

  • equivalently: such that for every other object $S$ there is a unique morphism $S \to *$

Notation

The above implies in particular that for two functions $f : S \to S'$ and $g : T \to T'$ there is canonically a function denoted

$$f \times g : S\times T \to S' \times T'$$

induced by the universal property of $S' \times T'$ by from the existence of the two functions $f p_1 : S \times T \to S'$ and $g p_2 : S \times T \to T'$

Axiom of equalizers.

For any two functions $\displaystyle f, g: S \rightrightarrows T$, there exists a function $i: E \to S$ such that

1. $f i = g i$,
2. Given $x \in S$ over some domain such that $f x = g x$, there exists a unique $x' \in E$ over the same domain such that $i (x') = x$.

Equivalently, in morphism language:

1. $(E \stackrel{i}{\to} S \stackrel{f}{\to} T) = (E \stackrel{i}{\to} S \stackrel{g}{\to} T)$,
2. Given any other $x : U \to S$ such that $(U \stackrel{x}{\to} S \stackrel{f}{\to} T) = (U \stackrel{x}{\to} S \stackrel{g}{\to} T)$, there exists a unique morphism $x' : U \to E$ such that the following diagram commutes

$$\array{ && U \\ &{}^{x'}\swarrow& \downarrow^{x} \\ E &\stackrel{i}{\to}& S &\stackrel{\stackrel{g}{\to}}{\stackrel{f}{\to}}& T }$$

An equalizer $i: E \to S$ is again defined up to isomorphism by its collection of generalized elements, denoted $E :=_i \{x \in S: f(x) = g(x)\} \hookrightarrow S$.

Consequence: pullbacks

The axiom of products and the axiom of equalizers already ensure that Set has pullbacks.

Given functions $f: S \to C, g: T \to C$ there exists a set $S \times_C T$ and functions $p_1 : S \times_C T \to S$ and $p_2 : S \times_C T \to T$ such that the diagram

$$\array{ S \times_C T &\stackrel{p_2}{\to}& T \\ \downarrow^{p_1} && \downarrow^{g} \\ S &\stackrel{f}{\to}& C }$$

commutes and such that that $S \times_C T$ is universal with respect to this property: for every other such diagram

$$\array{ U &\stackrel{y}{\to}& T \\ \downarrow^{x} && \downarrow^{g} \\ S &\stackrel{f}{\to}& C }$$

there is a unique function $\langle x,y\rangle : U \to S \times_S T$ such that

$$\array{ && U \\ & {}^x \swarrow &\downarrow^{\langle x , y \rangle}& \searrow^{y} \\ S &\stackrel{p_1}{\leftarrow}& S \times_C T &\stackrel{p_2}{\to}& T }$$

One checks that indeed $S \times_C T$ is equivalently the equalizer of $f p_1$ and $g p_2$:

$$S \times_C T \hookrightarrow S \times T \stackrel{\stackrel{g p_2}{\to}}{\stackrel{f p_1}{\to}} C \,.$$

Hence we may write

$$S \times_C T \simeq \{\langle x, y \rangle \in S \times T: f x = g y\}$$

Here $S \times_C T$ is the fiber product of $f$ with $g$: over $c \in C$ it is the product of the fibers $f^{-1}c = \{x | f x = c\}$ and $g^{-1}c = \{y | g y = c\}$.

Axiom of power sets.

For every set $S$ there is a set denoted $P(S)$ or $\mathbf{2}^S$ and called the power set of $S$ and a relation $\in_S \hookrightarrow S \times \mathbf{2}^S$ to be thought of as “$s \in S$ is element of subset $U \subset S$ in $S$” so that for every relation $R \hookrightarrow T \times S$, there exists a unique function $\chi_R: T \to \mathbf{2}^S$ such that $R$ is obtained up to isomorphism as the pullback

$$\{\langle x, y \rangle \in T \times S: y \in_S \chi_R(x)\} \,.$$

i.e the universal commutative diagram

$$\array{ R &\to& S \times T \\ \downarrow && \downarrow^{Id \times \chi_R} \\ \in_S &\hookrightarrow& S \times \mathbf{2}^S }$$

In other words, $\langle x, y \rangle$ belongs to $R$ if and only if $\langle y, \chi_R(x) \rangle$ belongs to $\in_S$.

Axiom of strong extensionality.

For functions

$$f, g: S \to T,$$

we have $f = g$ if and only if $f x = g x$ for all “ordinary” elements $x: * \to S$.

It is this axiom which allows to translate between the structural formulation of $SET$ and other traditional ways of talking about sets.

Notice that this axiom will not hold in a general topos, only in a well-pointed topos.

Axiom of natural numbers object.

There is a set $\mathbb{N}$, together with an element $0: * \to \mathbb{N}$ and a function $s: \mathbb{N} \to \mathbb{N}$, which is initial among sets equipped with such data. That is, given a set $S$ together with an element $x: * \to S$ and a function $f: S \to S$, there exists a unique function $h: \mathbb{N} \to S$ such that

• in function notation $h(0) = x; \qquad h s = f h$

• equivalently in elementwise notation, $h(n+1) = f h(n)$ for every (generalized) element $n \in \mathbf{N}$, where $n+1$ means $s(n)$.

• equivalently in diagrammatic notation

$$\array{ * &\stackrel{0}{\to}& \mathbb{N} &\stackrel{s}{\to}& \mathbb{N} \\ & {}_x\searrow & \downarrow^{h} && \downarrow^{h} \\ && S &\stackrel{f}{\to} & S }$$

Axiom of choice.

Every surjective function $p: S \to T$ admits a section, i.e., a function $\sigma: T \to S$ such that $p \sigma = Id_T$, the identity function.

Remark. This formulation makes the role played by the axiom of choice, which in other contexts may look a bit mysterious, quite transparent. See axiom of choice for further remarks. Notice that even if one assumes the axiom of choice in SET, it may generally fails in other topoi, and for quite natural reasons.

categories, functors and natural transformations

• Recall that a monoid is like a group, but without the requirement that every element has an inverse. A

category is like a monoid, but with an only partially

defined composition operation: every element is assigned a source and a target object and composition is only defined if the target of one element matches the source of the other. These “elements” are then called morphisms.

• Alternatively, a category can be thought of as a

directed graph equipped with a composition operation on its edges.

• A functor between categories is a map of objects and of morphisms, such that all this structure is preserved. It may be thought of as a homomorphism of directed graphs which preserves the composition of morphisms.

• One may also think of a category as (the fundamental category of) a directed space with morphisms the possible directed paths in that space. A functor is then thought of as a map of spaces. From this perspective a natural transformation between functors is like a homotopy between maps of spaces.

category

internal formulation

A category $C$ in $SET$ consists of

• an object $C_0$ in the collection of objects of $SET$, called the set of

objects of $C$ – often also denoted $Obj(C)$;

• an object $C_1$ in the collection of objects of $SET$, called the set of morphisms of $C$ – often also denoted $Mor(C)$;

together with

• source and target morphisms $s,t: C_1 \to C_0$ in $SET$;

• an identity assigning morphism $e: C_0 \to C_1$ in $SET$;

• a composition morphism $c: C_1 \times_{C_0} C_1 \to C_1$ in $SET$, where $C_1 \times_{C_0} C_1$ denotes the pullback of $s : C_1 \to C_0$ and $t : C_1 \to C_0$;

such that the following diagrams commute;

• laws specifying the source and target of identity morphisms:

$$\array{ C_0 & \stackrel{e}{\to} & C_1 \\ {} & 1\searrow & \darr s \\ {} & {} & C_0 } \quad\quad\quad\quad \array{ C_0 & \stackrel{e}{\to} & C_1 \\ {} & 1\searrow & \darr t \\ {} & {} & C_0 }$$

• laws specifying the source and target of composite morphisms:

$$\array{ C_1 \times_{C_0} C_1 & \stackrel{c}{\to} & C_1 \\ {}^{p_1}\downarrow & {} & \downarrow^{s} \\ C_1 & \stackrel{s}{\to} & C_0 } \quad\quad\quad\quad \array{ C_1 \times_{C_0} C_1 & \stackrel{c}{\to} & C_1 \\ {}^{p_2}\downarrow & {} & \downarrow^{t} \\ C_1 & \stackrel{t}{\to} & C_0 }$$

• the associative law for composition of morphisms:

$$\array{ C_1 \times_{C_0} C_1 \times_{C_0} C_1 & \stackrel{c\times_{C_0} 1}{\to} & C_1 \times_{C_0} C_1 \\ {}^{1\times_{C_0}c}\downarrow & {} & \downarrow^{c} \\ C_1 \times_{C_0} C_1 & \stackrel{c}{\to} & C_1 }$$

• the left and right unit laws for composition of morphisms:

$$\array{ C_1 \times_{C_0} C_1 & \stackrel{e \times_{C_0} 1}{\to} & C_1 \times_{C_0} C_1 & \stackrel{1 \times_{C_0} e}{\leftarrow} & C_1 \times_{C_0} C_1 \\ {} & {}^{p_2}\searrow & \downarrow^{c} & \swarrow^{p_1} & {} \\ {} & {} & C_1 & {} & {} }$$

Here, the pullback $C_1 \times_{C_0} C_1$ is defined via the square

$$\array{ C_1 \times_{C_0} C_1 & \stackrel{p_2}{\to} & C_1 \\ {}^{p_1}\downarrow & {} & \downarrow^{s} \\ C_1 & \stackrel{t}{\to} & C_0 }$$

Notice that the required pullbacks here do indeed exist due to the axioms of $SET$.

in components

If we write $C_1 = \{ a \stackrel{f}{\to} b\}$ for the set of morphisms, then we may denote the various operations above on ordinary elements on $C_1$ and $C_0$ as

• source map: $s : (a \stackrel{f}{\to} b) \mapsto a$

• target map: $t : (a \stackrel{f}{\to} b) \mapsto b$

• identity assigning map : $e : a \maptos (a \stackrel{e}{\to} a)$

• composition map: $c : (a \stackrel{f}{\to} b, b \stackrel{g}{\to} c) \mapsto a \stackrel{g \circ f}{\to}c$.

Then

• the unit laws say that $Id_b \circ f = f = f \circ \Id_a$

• the associativity law says that for all triples of composable morphisms $a \stackrel{f}{\to} b \stackrel{g}{\to} c \stackrel{h}{\to} d$ we have $(f \circ g) \circ h = f \circ (g \circ h)$

This looks now as before in the description of $SET$ itself.

further concepts and examples

• hom-set

• morphism

  • identity

  • epimorphism

  • monomorphism

  • inverse

  • isomorphism

  • endomorphism

  • automorphism

• object

  • initial object

  • terminal object

  • zero object

• opposite category

• subcategory

• general examples

  • discrete category

  • poset

  • groupoid

  • monoid: every monoid $A$ defines a category $\mathbf{B}A$ with $(\mathbf{B}A)_0 = \star$, with $(\mathbf{B}A)_1 = A$

  • group: every group $G$ defines a groupoid $\mathbf{B}G$ with $(\mathbf{B}G)_0 = \star$, with $(\mathbf{B}G)_1 = G$

  • arrow category

    • comma category

    • subobject

• concrete examples

  • point

  • globe

  • simplex category

  • fundamental groupoid

The “classical examples” such as Set, Top, Vect etc. are discussed in the next section after the introduction of universes and small sets.

functor

internal definition

For $C$ and $D$ cateories in $SET$ as above, a functor $F : C \to D$ from $C$ to $D$ in $SET$ is

• a morphism of objects $F_0 : C_0 \to D_0$ in $SET$;

• a morphisms of morphisms $F_1 : C_1 \to D_1$ in $SET$;

• such that the following diagrams commute

  • respect for the source map: $\array{ C_1 &\stackrel{f_1}{\to}& D_1 \\ \downarrow^s && \downarrow^s \\ C_0 &\stackrel{f_0}{\to}& D_0 }$;

  • respect for the target map: $\array{ C_1 &\stackrel{f_1}{\to}& D_1 \\ \downarrow^t && \downarrow^t \\ C_0 &\stackrel{f_0}{\to}& D_0 }$;

  • respect for identities $\array{ C_0 &\stackrel{f_0}{\to}& D_0 \\ \downarrow^i && \downarrow^i \\ C_1 &\stackrel{f_1}{\to}& D_1 }$;

  • respect for composition $\array{ C_1 \times_{t,s} C_1 &\stackrel{f_1\times_{t,s} f_1}{\to}& D_1 \times_{t,s} D_1 \\ \downarrow^{\circ} && \downarrow^{\circ} \\ C_1 &\stackrel{f_1}{\to}& D_1 }$.

in components

A functor $F : C \to D$ maps morphisms in $C$ to morphisms in $D$ while repsecting the composition of morphisms:

$$\begin{aligned} F : (a \stackrel{f}{\to} b \stackrel{g}{\to} c) & \mapsto (F(a) \stackrel{F(f)}{\to} F(b) \stackrel{F(g)}{\to} F(c)) \\ = F(a) \stackrel{F(g \circ f)}{\to} F(c) \end{aligned} \,.$$

concepts and examples

• for $G$, $H$ two groups, functors $\mathbf{B}G \to \mathbf{B}H$ are group homomorphisms

• stuff, structure, property

  • essentially surjective functor

  • full functor

  • faithful functor

  • subcategory

• a functor $\mathbf{B}G \to \mathbf{B}H$ is necessarily essentially surjective. It gives a group isomorphism precisely if it is also full and faithful functor.

natural transformation

In as far as a functor is like a map of spaces, a natural transformation is like a homotopy between maps of spaces.

Another way to understand the following definition of natural transformations is to note that it follows from demanding that categories form a cartesian closed category. This is the topic of the section on monoidal categories.

internal definition

For $F, G : C \to D$ two functors in $SET$, a natural transformation $\eta : F \Rightarrow G$ also denoted

$$\array{ & \nearrow\searrow^F \\ C &\Downarrow^\eta& D \\ & \searrow \nearrow_{G} }$$

is

• a component map $\eta : C_0 \to D_1$ in $SET$

• such that

$$\array{ C_1 &\stackrel{(\eta \circ s) \times G}{\to}& D_1 \times_{D_0} D_1 \\ \downarrow^{F \times (\eta \circ t)} && \downarrow^{comp_D} \\ D_1 \times_{D_0} D_1 &\stackrel{comp_D}{\to}& D_1 }$$

in components

In terms of elements this means that for all morphisms $c_1 \stackrel{f}{\to} c_2$ in $C$, the diagram

$$\array{ F(c_1) &\stackrel{\eta(c_1)}{\to}& G(c_1) \\ \downarrow^{F(f)} && \downarrow^{G(f)} \\ F(c_2) &\stackrel{\eta(c_2)}{\to}& G(c_2) }$$

commutes.

It is helpful and turns out to make good sense to think of this square literally as a homotopy between the image path $F(f)$ and the image path $G(f)$ in the “space” $D$.

examples

• a natural transformation between two functors of the form $F_1, F_2 : \mathbf{B}G \to \mathbf{B}H$ is a element $h \in H$ such that $F_1 = \mathrm{Ad}_h \circ F_1$.

equivalence of categories

Since natural transformations are morphisms between functors, two functors can be different while still being isomorphic. If two functors are inverses of each other up to such natural isomorphism, their source and target categories are “the same for all practical purposes”: they are equivalent.

Definition

A functor $F : C \to D$ is an equivalence of categories if there exists a functor $G : D \to C$ and natural isomorphisms

$$F \circ G \stackrel{\simeq}{\rightarrow} Id_D$$

and

$$G \circ F \stackrel{\simeq}{\rightarrow} Id_C \,.$$

Definition

A skeleton of a category $C$ is a category $C'$ equivalent to $C$ such that all isomorphic objects in $C'$ are equal.

Lemma

Every category $C$ has a skeleton $C'$ which is a full subcategory $C' \hookrightarrow C$.

Proof.

• choose a representative object in each isomorphism class;

• the full subcategory on these objects has the desired property

• notice: this makes crucially use of the axiom of choice which holds in $SET$ by definition

Proposition

A functor $F : C \to D$ is an equivalence of categories if and only it is full and faithful and essentially surjective.

Proof.

• assuming that $F : C \to D$ is an equivalence, choose a weak inverse $\bar F : D \to C$. The components of the natural isomorphism $F \circ \bar F \simeq Id_D$ exhibit $F$ as essentially surjective, full and faithful;

• assuming that $F : C \to D$ is essentially surjective, full and faithful,

  • one finds that $F_0 : C_0 \stackrel{\simeq}{\to} C \stackrel{F}{\to} D \stackrel{\simeq}{\to} D_0$ is an isomorphism with (strict) inverse $F_0^{-1}$, for $C_0$ and $D_0$ the skeleton of $C$ and $D$ respectively;

  • and that $D \stackrel{\simeq}{\to} D_0 \stackrel{F_0^{-1}}{\to} C_0 \stackrel{\simeq}{\to} C$ is a weak inverse for $F$.

Example.

Every groupoid $C$ in $SET$ that is connected (has only a single isomorphism class of objects) is equivalent to a groupoid of the form $\mathbf{B}G$ for $G$ a group: the automorphism group $Aut(a)$ of any object $a \in C$.