As in WeberYS2T, a classifying discrete opfibration in a finitely complete 2-category is a discrete opfibration such that for any , the functor
given by pullback of , is full and faithful.
The canonical example is when is some 2-category of “large categories” and is the category of (small) sets. More generally, we could take to be the 2-category and the category of sets of cardinality bounded by some cardinal .
When is equipped with a classifying discrete opfibration, we make the following definitions. * A discrete opfibration is small if it is in the image of the above functor. * A discrete object is small if is a small discrete opfibration. * If has a duality involution, we say an object is locally small or arrow-small if the discrete opfibration corresponding to the 2-sided fibration is small. * A not-necessarily-discrete object is small if it is locally small and admits an eso from a small discrete object.
If lacks a duality involution, then merely giving the discrete opfibration doesn’t suffice to characterize the notion of “smallness,” since we can’t define what it means to be locally small. This suggests the definition of a size structure.
We may impose additional axiom on a classifying discrete opfibration, many of which assert closure conditions of the class of small maps.
Some immediate consequences are:
We will see some further consequences of these axioms below.
Suppose that is a classifying discrete opfibration for which identity maps are small. Then there is a comma square
in which the map classifies the discrete opfibration .
A map is the same as a discrete opfibration equipped with a section with . Thus, it suffices to show that giving such data is equivalent to giving a square
in which the left-hand vertical map classifies . But the composite classifies , so since pullback of is full and faithful into discrete opfibrations, giving such a 2-cell is the same as giving a map of discrete opfibrations over , which is precisely to give a section of .
Suppose that is a CDO which is exponentiable. Then for any object , we call the exponential
the object of (small) families in . It comes with a projection to which “assigns to each family its indexing set.” Moreover, as observed in our study of exponentials, since is an opfibration and is a fibration, then is also a fibration, as we would expect.
has a universal property that can be directly expressed as follows. Evidently, to give a morphism is equivalent to giving a map together with a map over . But is simply the discrete opfibration classified by , and a map to over is just an arbitrary map to . Thus to give a map is the same as to give a small discrete opfibration together with a map : in other words, an -indexed family of small sets, each of which indexes a family of objects of .
(This sort of thing is closely related to the construction of generic families in Algebraic Set Theory.)
Now consider the special case when . As above, to give a map is to give a small discrete opfibration and a map . But a map is in turn equivalent to a small discrete opfibration . Thus is naturally equivalent the category of composable pairs of small discrete opfibrations. Recalling that any map between discrete opfibrations over is again a discrete opfibration, we observe that the 1-category consists of composable pairs of discrete opfibrations; thus is naturally a full subcategory of this category.
On the other hand, we can consider another full subcategory of determined by those composable pairs in which and the composite are small. This is precisely the subcategory , where consists of small discrete opfibrations, and is thus equivalent to . It follows that this second full subcategory of is equivalent to . Clearly these two subcategories agree if and only if small discrete opfibrations are closed under composition and have full slices, in the terminology defined above. Thus we have proven:
Let be an exponentiable classifying discrete opfibration; the following are equivalent.
When these conditions hold, we clearly have a natural equivalence lying over , and therefore, by the Yoneda lemma, an equivalence over between and the codomain fibration .
(Note the slight peculiarity of this result: it is more common, when showing that two things are equivalent under certain conditions, to construct a canonical map between them which always exists and happens to be an equivalence in the cases of interest. Here instead we have constructed a canonical cospan which induces an equivalence in the cases of interest.)
Colloquially speaking, this theorem says that the category of sets satisfies the “replacement axiom” if and only if the “naive indexing” of over itself is equivalent to its “self-indexing” . In classical material set theory, this is well-known to be equivalent to the usual axiom of replacement.
Note, though, that depending on what is, may not be the “naive indexing” at all. For instance, if is the category of stacks on a topos , then the self-indexing of is a classifying discrete opfibration in , which always satisfies the “axiom of replacement,” essentially by construction. Analogous facts are well-known in algebraic set theory, and are one reason why “the axiom of replacement” is a bit slippery in structural set theory. Generally, in intuitionistic logic, the axioms of replacement and collection add no extra proof-theoretic strength because they can be made to hold internally in suitable (2-)topoi of sheaves/stacks; it is the axiom of separation which carries all the power distinguishing IZF from IETCS.
Given a classifying discrete opfibration, we can use finite 2-categorical limits and the “internal logic” to construct all the usual concrete categories out of the object . For instance, if small discrete opfibrations are a subcategory, so that is a cartesian object, then we have the composite of the diagonal with the “binary products” morphism which, intuitively, takes a set to the set . Now the inserter of this composite and can be considered “the category of sets equipped with a function ,” i.e. the category of magmas.
Now we have a forgetful morphism , and also a functor which takes a magma to the triple product , and there are two 2-cells relating these constructed from two different composites of the inserter 2-cell defining the category of magmas. It makes sense to call the equifier of these 2-cells “the category of semigroups” (sets with an associative binary operation). Proceeding in this way we can construct the categories of monoids, groups, abelian groups, and eventually rings.
A more direct way to describe these categories with a universal property is as follows. Since is a cartesian object, each hom-category has finite products, so we can define the category of rings internal to it. Then the category is equipped with a forgetful functor which has the structure of a ring in , and which is universal in the sense that we have a natural equivalence . The above construction then just shows that such a representing object exists.
If has a duality involution and is a classifying discrete opfibration, then is a “classifying discrete fibration,” and therefore also a classifying discrete opfibration in .
A classifying discrete opfibration in is not inherited by any category of truncated objects in , since and will generally not be truncated. However, it is inherited by (op)fibrational slices.
Recall first that opfibrations in can be identified with morphisms in whose underlying morphism in is an opfibration. Moreover, such an opfibration is discrete if and only if its underlying morphism in is so. Thus, it is natural to hope for the following.
If has exponentials and a classifying discrete opfibration, then each 2-category has a classifying discrete opfibration, and the small opfibrations in are those whose underlying opfibrations in are small.
Recall that when has exponentials, is comonadic over ; let denote the comonad. For any , write for the category of small discrete opfibrations over . Then our goal is for to be representable. But we have
Therefore, defining we obtain a classifying discrete opfibration in that classifies the desired small opfibrations.
If has exponentials, a duality involution, and a classifying discrete opfibration, then each 2-category also has a classifying discrete opfibration.
This follows from Theorem 2 since . The classifying object is explicitly given by , although the small maps are not as explicitly characterized.