nLab category with class structure

Contents

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Category Theory

Contents

Idea

Just as the notion of an elementary topos is an axiomatization of basic category-theoretic properties of the category of sets, the notion of a “category with class structure” or “category of classes” is an axiomatization of the basic category theoretic properties of the category of classes.

In contrast to the situation for elementary toposes, however, there is no unique such axiomatization with a privileged status in the literature; the field of algebraic set theory includes many variations. Here we describe the first such axiomatization due to Joyal-Moerdijk.

Definition

We work in a category CC that is assumed to be a Heyting pretopos with a natural numbers object. Following Joyal-Moerdijk, we have the following definition.

Definition

A class of open maps (with collection) in CC is a class SS of morphisms in CC that satisfies the following properties:

  • SS contains all isomorphisms and is closed under compositions;
  • SS is closed under base changes;
  • if gSg\in S is a base change of ff along an epimorphism, then fSf\in S;
  • the canonical maps 010\to 1 and 1111\sqcup 1\to 1 belong to SS;
  • SS is closed under binary coproducts in the category of morphisms of CC;
  • if g=fpg=f\circ p, where pp is an epimorphism and gSg\in S, then also fSf\in S;
  • (collection axiom) for any epimorphism p:YXp\colon Y\to X and f:XAf\colon X\to A such that fSf\in S there is an epimorphism h:BAh\colon B\to A, a morphism g:ZBg\colon Z\to B such that gSg\in S, and a morphism w:ZYw:Z\to Y such that hg=fpwh g=f p w and the induced map ZB× AXZ\to B\times_A X is an epimorphism.

Definition

A class of small maps in CC is a class of open maps SS in CC such that every map in SS is exponentiable and there is a universal map π:EU\pi\colon E\to U in SS with the following property: for any fSf\in S we can base change ff along some epimorphism pp such that the resulting morphism ff' is a base change of π\pi along some morphism in CC. Elements of SS are known as small maps. An object XX of CC is small if the map X1X\to 1 is small.

Intuitively, small maps are maps XYX\to Y for which preimages of any element of YY are sets as opposed to proper classes.

In any Heyting pretopos the class of exponentiable maps satisfies all the axioms of a class of open maps with a possible exception of the collection axiom.

The collection axiom can be reformulated by saying that the small powerset functor preserves epimorphisms. One way to define the small powerset of XX is as the free SS-complete suplattice generated by XX.

Definition

A category with a class of small maps admits powerclasses if for any object CC there is an object PCP C with a small relation C×PC\in\subset C\times P C such that any object XX and any small relation RC×XR\subset C\times X there is a unique morphism r:XPCr\colon X\to P C such that RC×XR\to C\times X is the base change of C×PC\in\to C\times P C along the map id C×rid_C \times r. Furthermore, the internal subset relation on PCP C must be small.

Definition

A universal class is an object UU such that any object CC admits a monomorphism UCU\to C.

Definition

A category of classes or a class category is Heyting category with a class of small maps that admits small powerclasses and a universal class.

The full subcategory of small objects and small maps of any class category is an elementary topos.

References

Last revised on November 19, 2022 at 18:12:56. See the history of this page for a list of all contributions to it.