Properties of fibrations

4. Properties of fibrations [000E]

4.1. Locally small fibrations [000F]

There are a number of (equivalent) variations on the definition of a locally small fibration. We attempt to provide some intuition for these definitions.

4.1.1. Warmup: locally small family fibrations [000G]

An ordinary category $E$ is called locally small when for any $x,y\in E$ the collection of morphisms $x\to y$ is a set. This property of $E$ can be rephrased in terms of its family fibration () $\FAM{E}$ over $\SET$ as follows.

Consider an index set $I\in \SET$ and two families $u,v\in C^I$. We may define an $I$-indexed collection $[u,v]\Sub{i\in I}$ consisting (pointwise) of all the morphisms $u\Sub{i}\to v\Sub{i}$ in $C$:

If $C$ is locally small, $[u,v]\Sub{i\in I}$ is in fact a family of sets for any $I\in\SET$ as each $[u,v]\Sub{i}$ is a set. Conversely, if $[u,v]\Sub{i\in I}$ is a family of sets for any $I\in \SET$, then $C$ is locally small as we may consider in particular the case that $I=\mathbf{1}$.

4.1.2. A more abstract formulation [000H]

We will reformulate the above in a way that uses only the language that makes sense for an arbitrary cartesian fibration, though for now we stick with $\FAM{C}$. Given $u,v\in \FAM{C}[I]$, we have a “relative hom family” $[u,v]\in\Sl{\SET}{I}$, defined in . The fact that each $[u,v]\Sub{i}$ is the set of all morphisms $u\Sub{i}\to v\Sub{i}$ can be rephrased more abstractly.

First we consider the restriction of $u\in \FAM{C}[I]$ to $\FAM{C}[[u,v]]$ as follows: Explicitly the family $\InvImg{[u,v]}u$ is indexed in a pair of an element $i\in I$ and a morphism $u\Sub{i}\to v\Sub{i}$. We can think of $\InvImg{[u,v]}u$ as the object of elements of $u\Sub{i}$ indexed in pairs $(i,u\Sub{i}\to v\Sub{i})$.

There is a canonical map $\epsilon\Sub{[u,v]}:\InvImg{[u,v]}u\to\Sub{p\Sub{[u,v]}} v$ that “evaluates” each indexing morphism $u\Sub{i}\to v\Sub{i}$.

That each $[u,v]\Sub{i}$ is the set of all morphisms $u\Sub{i}\to v\Sub{i}$ can be rephrased as a universal property: for any family $h\in\Sl{\SET}{I}$ and morphism $\epsilon\Sub{h} : \InvImg{h}u\to\Sub{h} v$ in $\FAM{C}$, there is a unique cartesian map $\InvImg{h}u\to \InvImg{[u,v]}u$ factoring $\epsilon\Sub{h}$ through $\epsilon\Sub{[u,v]}$ in the sense depicted below:

To convince ourselves of this, we note that the family $H \coloneqq \brc{u\Sub{i}\to v\Sub{i}}\Sub{i\in I}$ itself satisfies the universal property above. Indeed, fix a candidate $h \in \Sl{\SET}{I}$ equipped with a map $\epsilon\Sub{h} : \InvImg{h}u \to_h v$. Unfolding the meaning of this map in set theoretical notation, we see that it amounts to a family of maps $\epsilon\Sub{h}[i] : \prod\Sub{x\in h_i} \brc{u_i\to v_i}$ for each $i\in I$; such a family immediately induces the desired map $h\to H$. ∎

4.1.3. The definition of local smallness [000I]

Based on our explorations above, we are now prepared to write down (and understand) the proper definition of local smallness for an arbitrary cartesian fibration $E$ over $B$, which should be thought of as a (potentially large) category relative to $B$.

[001C] Definition 4.1.3·a (Hom candidates).

For any $x\in B$ and displayed objects $u,v\in E\Sub{x}$, we define a hom candidate for $u,v$ to be a span $u\leftarrow \bar{h} \rightarrow v$ in $E$ in which the left-hand leg is cartesian:

In the above, $h$ should be thought of as a candidate for the “hom object” of $u,v$, and $\epsilon\Sub{h}$ should be viewed as the structure of an “evaluation map” for $h$. This structure can be rephrased in terms of a displayed category $\CandHom{x}{u}{v}$ over $\Sl{B}{x}$:

Given $h\in \Sl{B}{x}$, an object of $\CandHom{x}{u}{v}\Sub{h}$ is given by a hom candidate whose apex in the base is $h$ itself. We will write $\bar{h}$ metonymically for the entire hom candidate over $h$.
Given $\alpha:l\to h\in\Sl{B}{x}$ and hom candidates $\bar{l}\in \CandHom{x}{u}{v}\Sub{l}$ and $\bar{h}\in \CandHom{x}{u}{v}\Sub{h}$, a morphism $\bar{h}\to\Sub{\alpha} \bar{l}$ is given by a cartesian morphism $\bar\alpha:\bar{l}\to\Sub{\alpha}\bar{h}$ in $E$ such that the following diagram commutes:

[001B] Definition 4.1.3·b (Locally small fibration).

A cartesian fibration $E$ over $B$ is locally small if and only if for each $x\in B$ and $u,v\in E\Sub{x}$, the total category $\TotCat{\CandHom{x}{u}{v}}$ has a terminal object.

4.2. Globally small fibrations [000J]

In ordinary category theory, a category $C$ is called small when the objects of $C$ can be arranged into a set, and so can for every $x,y\in C$ the collection of morphisms $x\to y$. It is useful to separate these two conditions when we generalize them to fibrations. The latter is called local smallness and is discussed and defined in ; the former is called global smallness by Jacobs (Categorical Logic and Type Theory, 1999) and factors through an important concept: the generic object.

[001D] Definition 4.2·a.

An ordinary category is called globally small when it has a set of objects.

4.2.1. Generic objects [000K]

Up to equivalence of categories, we may detect global smallness of a category $C$ from the perspective of the family fibration $\FAM{C}$ (). In particular, a category is equivalent to a globally small category when its family fibration has a generic object in the following sense.

[001E] Definition 4.2.1·a (Generic object).

Let $E$ be a cartesian fibration over $B$; a generic object for $E$ is defined to be an object $\bar{u}\in \TotCat{E}$ such that for any $\bar{z}\in \TotCat{E}$ there exists a cartesian map $\bar{z}\to \bar{u}$.

Warning. Our terminology differs from that of Jacobs (Categorical Logic and Type Theory, 1999); what we refer to as a generic object here is Jacobs’ weak generic object. We prefer the unqualified terminology, as generic objects in the stronger sense are very rare.

[000L] Theorem 4.2.1·b (Globally small categories).

An ordinary category $C$ is equivalent to a globally small category if and only if the fibration $\FAM{C}$ has a generic object.

Proof. To see that this is the case, suppose that $C$ has a set of objects. Then $C\in\SET$ and we define $\lfloor{C}\rfloor$ to be the displayed object $\brc{x}\Sub{x\in C}\in \FAM{C}[C]$. Fixing $I\in \SET$ and $z\in C^I$, we consider the cartesian map displayed over $z : I \to C$:

Conversely assume that $\FAM{C}$ has a generic object $\bar{u}\in\FAM{C}[U]$ for some $U\in \SET$; then we may equip $U$ with the structure of a globally small category such that $U$ is equivalent to $C$, using a construction that is similar to our implementation of the opposite fibration (). In particular we define a morphism $x\to y\in U$ to be given by the following data:

a cartesian map $a\to\Sub{x} \bar{u}$ over $x : 1\to U$,
a cartesian map $b\to\Sub{y} \bar{u}$ over $y : 1\to U$,
and a vertical map $h:a\to b$ in $\FAM{C}[1]\simeq C$,

such that $(a\Sub{1},b\Sub{1},h\Sub{1})$ is identified with $(a\Sub{2},b\Sub{2},h\Sub{2})$ when $h_1$ and $h_2$ are equal modulo the (unique) vertical isomorphisms between the cartesian lifts in the sense depicted below:

Remember that a cartesian map $a\to\Sub{x}\bar{u}$ is standing for a choice of an object of $C$ encoded by $x\in U$. Because such choices are unique only up to isomorphism, we must include them explicitly in the data. ∎

[000P] Definition 4.2·b (Globally small fibration).

A cartesian fibration $E$ over $B$ is called globally small when it has a generic object in the sense of .

4.3. Separators for cartesian fibrations [002E]

Let $E$ be an ordinary category. In general, to compare two morphisms $f,g:x\to y$ in $E$, it is not enough to see if they agree on global points $u:1\to x$, because the behavior of $u,v$ may differ only on generalized elements. In some cases, however, there is a family of objects $\prn{s\Sub{i}}\Sub{i\in I}\in E$ are together adequate for comparing morphisms of $E$ in the sense of below.

[002G] Definition 4.3·a (Separating family for a category).

Given an ordinary category $E$, a set-indexed family $\prn{s\Sub{i}}\Sub{i\in I}$ of $E$-objects is called a small separating family for $E$ when, assuming that for all $i\in I$ and all $u:s_i\to x$ we have $u;f=u;g$, we then have $f=g$.

The intuition of is that to compare two morphisms $f,g:x\to y\in E$, it suffices to check that they behave the same on all $s\Sub{i}$-shaped figures when $\prn{s\Sub{i}}\Sub{i\in I}$ is a separating family for $E$.

[002F] Example 4.3·b (Well-pointedness of the category of sets).

In the category of sets, to compare two morphisms it is enough to check that they agree on global points. This means that the unary family $\brc{\ObjTerm{\SET}}$ is a separator for $\SET$, a property referred to more generally as well-pointedness.

We will now generalize to the case of a cartesian fibration.

[002I] Definition 4.3·c (Agreement on a class of figure shapes).

Let $\bar{s}$ be a displayed object in a cartesian fibration $E$ over $B$. A pair of displayed morphisms $f,g:\bar{x}\to \bar{y}\in E$ are said to agree on $\bar{s}$-figures when for any $\bar{s}$-figure $h : \bar{z}\to \bar{x}$ in the sense of , we have $h;f = h;g : \bar{z}\to \bar{y}$.

[002H] Definition 4.3·d (Small separator for a fibration).

Let $E$ be a cartesian fibration over $B$ such that $B$ has binary products. A displayed object $\bar{s}\in E\Sub{s}$ is said to be a small separator for $E$ when any two vertical maps $f,g:\bar{u}\to\Sub{\Idn{x}}\bar{v}\in E\Sub{x}$ are equal when they are agree on $\bar{s}$-figures in the sense of .

4.4. Definable classes à la Bénabou [002L]

A class of sets $\mathfrak{C}$ is sometimes said to be formally definable when there is a formula $\prn{x \mid \phi\Sub{\mathfrak{C}}\prn{x}}$ in the language of set theory such that a set $S$ lies in $\mathfrak{C}$ if and only if $\phi\Sub{\mathfrak{C}}\prn{S}$ holds. This concept is a bit sensitive, as it presupposes that we have a notion of “class” whose constituents are not all definable in this sense.

A better behaved notion of definability for sets than the formal one is given model-theoretically, i.e. relative to a model $\mathscr{M}$ of set theory in some ambient set theory (Bénabou, 1985). We will refer to an element of $\mathscr{M}$ as a set, and a subcollection of $\mathscr{M}$ as a class.

[002U] Definition 4.4·a (Representable class of sets).

A class of sets $\mathfrak{C}\subseteq\mathscr{M}$ is called representable when there is a set $C\in\mathscr{M}$ such that $U\in C$ if and only if $U\in\mathfrak{C}$.

[002V] Definition 4.4·b (Definable class of sets).

A class of sets $\mathfrak{C}\subseteq\mathscr{M}$ is called definable when for any representable class $\mathfrak{S}$, the class $\mathfrak{C}\cap\mathfrak{S}$ is representable.

Bénabou then generalizes the definitions above to an arbitrary fibration, in such a way that the general fibered notion of definable class is equivalent in the canonical self-indexing $\SelfIx{\mathscr{M}}$ to that of definable classes in the sense of .

4.4.1. Set-theoretic intuition for Bénabou's definability [002Q]

To motivate Bénabou’s general notion of definability, we will first develop an alternative perspective on definability for classes of sets in terms of families of sets.

[002M] Construction 4.4.1·a (Closure of a class of sets under base change).

Let $\mathfrak{C}\subseteq\mathscr{M}$ be a class of sets; there exists a class $\bar{\mathfrak{C}}$ of families of sets that contains $\prn{S\Sub{i}}\Sub{i\in I}$ exactly when each $S\Sub{i}$ lies in $\mathfrak{C}$. We will refer to $\bar{\mathfrak{C}}$ as the closure under base change of $\mathfrak{C}$, a name motivated by the fact that when $\prn{S\Sub{i}}\Sub{i\in I}$ lies in $\bar{\mathfrak{C}}$, then for any $u:J\to I$, the base change $\prn{S\Sub{uj}}\Sub{j\in J}$ also lies in $\bar{\mathfrak{C}}$.

[002N] Construction 4.4.1·b (From classes of families to classes of sets).

Conversely to we may take a class of families of sets $\mathfrak{F}$ to the the class of sets $\mathfrak{F}\Sub{1}\subseteq{\mathscr{M}}$ spanned by sets $S$ such that the singleton family $\brc{S}$ lies in $\mathfrak{C}$.

[002P] Definition 4.4.1·c (Definable class of families of sets).

A class of families of sets $\mathfrak{F}$ is said to be definable when it is stable and moreover, for any family of sets $\prn{S\Sub{i}}\Sub{i\in I}$, there exists a subset $J\subseteq I$ such that the base change $\prn{S\Sub{j}}\Sub{j\in J}$ lies in $\mathfrak{F}$, and moreover, such that $u:K\to I$ factors through $J\subseteq I$ whenever the base change $\prn{S\Sub{uk}}\Sub{k\in K}$ lies in $\mathfrak{F}$.

[002R] Intuition 4.4.1·d.

In other words, a stable class of families of sets is definable when any family of sets can be restricted to a “biggest” subfamily that lies in the class.

[002T] Lemma 4.4.1·e (Characterization of definable classes of families).

Let $\mathfrak{C}\subseteq\mathscr{M}$ be a class of sets; then $\bar{\mathfrak{C}}$ is a definable class of families of sets if and only if $\mathfrak{C}$ is a definable class of sets.

Proof. Suppose that $\mathfrak{C}$ is a definable class of sets. To check that $\bar{\mathfrak{C}}$ is a definable class of families of sets, we fix a family $\prn{S\Sub{i}}\Sub{i\in I}$ not necessarily lying in $\bar{\mathfrak{C}}$. Because $\mathfrak{C}$ is definable, the intersection $\mathfrak{C}\cap \bigcup\Sub{i\in I}S\Sub{i}$ is represented by a set $U$. We therefore take the subset $J = \brc{i \in I\mid S_i\in U}\subseteq I$, and verify that the base change $\prn{S\Sub{j}}\Sub{j\in J}$ is the largest approximation of $\prn{S\Sub{i}}\Sub{i\in I}$ by a family lying in $\bar{\mathfrak{C}}$.

Conversely suppose that $\bar{\mathfrak{C}}$ is a definable class of families of sets. To see that $\mathfrak{C}$ is definable, we fix a class $\mathfrak{U}$ represented by a set $U\in\mathscr{M}$ to check that $\mathfrak{C}\cap\mathfrak{U}$ is representable. We consider the family of sets $\prn{u}\Sub{u\in U}$; because $\bar{\mathfrak{C}}$ is definable, there is a largest subset $V\subseteq U$ such that the change of base $\prn{v}\Sub{v\in V}$ lies in $\bar{\mathfrak{C}}$, i.e. such that each $v\in V$ lies in $\mathfrak{C}$. Therefore $\mathfrak{C}\cap\mathfrak{U}$ is represented by the set $V$. ∎

4.4.2. Bénabou's notion of definability [002S]

We will now construe as the instantiation at the canonical self-indexing $\SelfIx{\mathscr{M}}$ of a more general notion of definability for classes of objects in a cartesian fibration, defined forthwith. The following definition of definability in a cartesian fibration is due to Bénabou, but is discussed in print by Borceux (Handbook of Categorical Algebra 2 – Categories and Structures, 1994), Jacobs (Categorical Logic and Type Theory, 1999), Streicher (Fibred Categories à La Jean Bénabou, 2018).

[002W] Definition 4.4.2·a (Definable class in a fibration).

Let $E$ be a cartesian fibration over $B$. A definable class $\mathfrak{F}$ in $E$ is a stable subcollection of the displayed objects of $E$ such that for any $\bar{u}\in E\Sub{u}$, there exists a cartesian map $\bar{v}\to \bar{u}$ lying over a monomorphism $v\rightarrowtail u$ such that $\bar{v}\in \mathfrak{F}$ and, moreover, any cartesian morphism $\bar{w}\to\bar{u}$ such that $\bar{w}\in\mathfrak{F}$ factors through $\bar{v}\to\bar{u}$.

[002O] Remark 4.4.2·b.

Let $\mathscr{M}$ be a model of ETCS; and let $\mathfrak{C}$ be a class of families of sets in $\mathscr{M}$. Then $\mathfrak{C}$ is a class of objects in the canonical self-indexing $\SelfIx{\mathscr{M}}$ over $\mathscr{M}$. Furthermore, $\mathscr{M}$ a definable class in $\SelfIx{\mathscr{M}}$ in the sense of if and only if it is a definable class of families of sets in the sense of .

Bibliography