Definable classes à la Bénabou

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