« Home

Person. Jean Bénabou [jeanbénabou]

Backlinks

Successor algebras [00CM]

November 1, 2023
Jon Sterling
[joyal-moerdijk-1995]

These results are attributed by Joyal and Moerdijk to Jean Bénabou and Mamuka Jibladze.

Definition. Successor algebra [00C9]

October 30, 2023
Jon Sterling
[joyal-moerdijk-1995]

Let $\mathbb {T}$ be a monad on a category $\mathcal {C}$ . A successor algebra for $\mathbb {T}$ is defined to be a algebra $X$ for $\mathbb {T}$ together with a morphism ${X}\xrightarrow {{s_{X}}}{X}$ in $\mathcal {C}$ called the successor map.

Definition. Homomorphism of successor algebras [00CA]

October 30, 2023
Jon Sterling
[joyal-moerdijk-1995]

A homomorphism of successor algebras is a monad algebra homomorphism ${X}\xrightarrow {{h}}{Y}$ that preserves the successor operation:

Definition. The successor restriction of a successor algebra [00CC]

October 30, 2023
Jon Sterling
[joyal-moerdijk-1995]

Let $\mathbb {T}$ be a monad on a category $\mathcal {C}$ , and let $X$ be an successor algebra for $\mathbb {T}$ . We define the successor restriction of $X$ to be the weak algebra $s\cdot X :\equiv s_{X}\cdot X$ defined by restricting $X$ along its successor map.

Construction. The induced successor algebra on a fixed point [00CN]

November 1, 2023
Jon Sterling

Let $\mathbb {T}\equiv {\mathopen {}\left (T,\eta ,\mu \right )\mathclose {}}$ be a monad on a category $\mathcal {C}$ , and let $X$ be a weak algebra for $\mathbb {T}$ . The monad algebra $\bar {X}$ induced by $X$ can be equipped with the structure of a successor algebra by defining ${X}\xrightarrow {{s_{\bar {X}}}}{X}$ to be the following map:

Converting between weak algebra and successor algebra homomorphisms [00DB]

November 5, 2023
Jon Sterling

Lemma. Lifting homomorphisms to the induced successor algebra [00CR]

November 1, 2023
Jon Sterling
[joyal-moerdijk-1995]

Let $\mathbb {T} \equiv {\mathopen {}\left (T,\eta ,\mu \right )\mathclose {}}$ be a monad on a category $\mathcal {C}$ and let $I$ be an invertible weak algebra for $\mathbb {T}$ ; let $X$ be an arbitrary successor algebra. Then a homomorphism ${I}\xrightarrow {{j}}{s\cdot X}$ also tracks a successor algebra homomorphism ${\bar {I}}\xrightarrow {{j}}{X}$ , where $\bar {I}$ is the induced successor algebra of $I$ and $s\cdot X$ is the successor restriction of $X$ .

Proof.

November 1, 2023
Jon Sterling

We have already seen that ${I}\xrightarrow {{j}}{s\cdot X}$ tracks an algebra homomorphism ${\bar {I}}\xrightarrow {{j}}{X}$ . It remains to show that this homomorphism preserves the successor operation.

We first unfold the successor operation of the induced successor algebra on $I$ .
Then we use the algebra property of ${I}\xrightarrow {{j}}{s\cdot X}$ .
Then we unfold the restricted algebra structure.
Finally we the unitality of the monad algebra $X$ .

Lemma. From successor algebra homomorphisms to weak algebra homomorphisms [00D9]

November 5, 2023
Jon Sterling
[joyal-moerdijk-1995]

Let $\mathbb {T} \equiv {\mathopen {}\left (T,\eta ,\mu \right )\mathclose {}}$ be a monad on a category $\mathcal {C}$ and let $I$ be an invertible weak algebra for $\mathbb {T}$ ; let $X$ be an arbitrary successor algebra. Then a successor algebra homomorphism ${\bar {I}}\xrightarrow {{j}}{X}$ also tracks a weak algebra homomorphism ${I}\xrightarrow {{j}}{s\cdot X}$ , where $\bar {I}$ is the induced successor algebra of $I$ and $s\cdot X$ is the successor restriction of $X$ .

Proof.

November 5, 2023
Jon Sterling

We work backwards.

First, we unfold the algebra structure of the successor restriction.
We then use the successor algebra homomorphism property of ${\bar {I}}\xrightarrow {{j}}{X}$ .
Next we use the algebra homomorphism property of ${\bar {I}}\xrightarrow {{j}}{X}$ .
We unfold the definition of the induced monad algebra.
We unfold the successor map on the induced successor algebra.
We contract the composition of the initial (weak) algebra map with its inverse.
Finally, we use the unit law of the monad $\mathbb {T}$ .

Corollary. Weak algebra homomorphisms and successor algebra homomorphisms are interchangeable [00DA]

November 5, 2023
Jon Sterling

Let $\mathbb {T}$ be a monad on a category $\mathcal {C}$ and let $I$ be an invertible weak algebra for $\mathbb {T}$ ; let $X$ be an arbitrary successor algebra. Then a morphism ${I}\xrightarrow {{j}}{X}$ in $\mathcal {C}$ tracks a weak algebra homomorphism ${I}\xrightarrow {{j}}{s\cdot X}$ if and only if it tracks a successor algebra homomorphism ${\bar {I}}\xrightarrow {{j}}{X}$ , where $\bar {I}$ is the induced successor algebra of $I$ and $s\cdot X$ is the successor restriction of $X$ .

Proof.

November 5, 2023
Jon Sterling

This follows from the following two lemmas:

Lifting homomorphisms to the induced successor algebra;
From successor algebra homomorphisms to weak algebra homomorphisms.

Theorem. From initial weak algebras to initial successor algebras [00D8]

November 5, 2023
Jon Sterling
[joyal-moerdijk-1995]

Let $I$ be the initial weak algebra for a monad $\mathbb {T}$ on a category $\mathcal {C}$ . Then the induced successor algebra $\bar {I}$ is the initial successor algebra for $\mathbb {T}$ .

Proof.

November 5, 2023
Jon Sterling

Let $X$ be a successor algebra; we have shown that weak algebra homomorphism ${I}\xrightarrow {{\iota }}{s\cdot X}$ from $I$ to the successor restriction of $X$ also tracks a successor algebra homomorphism ${\bar {I}}\xrightarrow {{\iota }}{X}$ . To see that this homomorphism is unique, fix any successor algebra homomorphism ${\bar {I}}\xrightarrow {{j}}{X}$ ; we have also shown that such a homomorphism also tracks a (weak algebra) homomorphism ${I}\xrightarrow {{j}}{s\cdot X}$ . But ${I}\xrightarrow {{\iota }}{s\cdot X}$ is the such weak algebra homomorphism, so we have $\iota = j$ .

Jack Romo on homotopy bicategories of complete 2-fold Segal spaces [0091]

September 15, 2023
Jon Sterling
Yorkshire and Midlands Category Theory Seminar #32

Jack Romo gave a talk about homotopy bicategories of complete 2-fold Segal spaces. The goal of the work is to convert (∞,2)-categories to their (homotopy) bicategories; he has managed to define the homotopy bicategory, but I believe it is not yet functorial (part of the problem is to find the appropriate “category” for the domain of this “functor”).

The model of (∞,2)-category used is complete 2-fold Segal space, which is like an iteration of the Segal conditions. A complete Segal space is a simplicial diagram of (∞,1)-groupoids satisfying certain lifting conditions — the Segal condition says the projection of n-simplices to their “spines” should be a trivial fibration (contractible fibers!) A complete 2-fold Segal space is a simplicial diagram of complete Segal spaces satisfying similar conditions.

Computing the homotopy bicategory is non-trivial as various properties (existence of certainly lifts in the complete 2-fold Segal space) must be converted into structure (explicit associators, etc.). Jack is using an unbiased definition of bicategory due to Tom Leinster that is known to be equivalent to the bicategories of Jean Bénabou.

Chapter 3: the theory of universes [0011]

January 19, 2023
Jon Sterling

Universes started their life in the Grothendieck school of algebraic geometry as a technical device to circumvent the annoyance that there cannot be a “set of all sets”; a universe is a set of enough sets, and whilst a universe cannot contain itself, it may nonetheless lie within an even bigger universe. Several important developments in the theory of universes from the 1970s onward by Bénabou, Martin-Löf, Dybjer, Hofmann, Streicher, Awodey, and others have collided to deliver the present-day understanding of the centrality of universes in semantics: a model of type theory is just a special kind of universe in a special kind of category. This chapter provides expository background on the theory of universes, including a novel account of open and closed subuniverses to reflect the recollement theory of topoi from Chapter 2. These open and closed subuniverses will play a critical role in the development of synthetic Tait computability in subsequent chapters.

Reference. Fibred categories à la Jean Bénabou [streicher-fcjb]

December 16, 2022
Thomas Streicher
10.48550/arXiv.1801.02927

These are notes about the theory of Fibred Categories as I have learned it from Jean Bénabou. I also have used results from the Thesis of Jean-Luc Moens from 1982 in those sections where I discuss the fibered view of geometric morphisms. Thus, almost all of the contents is not due to me but most of it cannot be found in the literature since Bénabou has given many talks on it but most of his work on fibered categories is unpublished. But I am solely responsible for the mistakes and for misrepresentations of his views. And certainly these notes do not cover all the work he has done on fibered categories. I just try to explain the most important notions he has come up with in a way trying to be as close as possible to his intentions and intuitions. I started these notes in 1999 when I gave a course on some of the material at a workshop in Munich. They have developed quite a lot over the years and I have tried to include most of the things I want to remember.

@unpublished{streicher-fcjb,
  author = {Streicher, Thomas},
  year = {2021},
  eprint = {1801.02927},
  eprintclass = {math.CT},
  eprinttype = {arXiv},
  title = {Fibered Categories \`{a} la {Jean B\'{e}nabou}},
}

Definable classes à la Bénabou [frct-002L]

Jon Sterling

A class of sets $\mathfrak {C}$ is sometimes said to be formally definable when there is a formula ${\mathopen {}\left (x \mid \phi _{\mathfrak {C} {\mathopen {}\left (x\right )\mathclose {}}}\right )\mathclose {}}$ in the language of set theory such that a set $S$ lies in $\mathfrak {C}$ if and only if $\phi _{\mathfrak {C}}{\mathopen {}\left (S\right )\mathclose {}}$ 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. We will refer to an element of $\mathscr {M}$ as a set, and a subcollection of $\mathscr {M}$ as a class.

Definition. Representable class of sets [frct-002U]

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}$ .

Definition. Definable class of sets [frct-002V]

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 these definitions to an arbitrary fibration, in such a way that the general fibered notion of definable class is equivalent in the fundamental self-indexing $\underline {\mathscr {M}}$ to that of definable classes.

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

Jon Sterling

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.

Construction. Closure of a class of sets under base change [frct-002M]

Let $\mathfrak {C}\subseteq \mathscr {M}$ be a class of sets; there exists a class $\bar {\mathfrak {C}}$ of families of sets that contains ${\mathopen {}\left (S_{i}\right )\mathclose {}}_{i\in I}$ exactly when each $S_{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 ${\mathopen {}\left (S_{i}\right )\mathclose {}}_{i\in I}$ lies in $\bar {\mathfrak {C}}$ , then for any $u:J\to I$ , the base change ${\mathopen {}\left (S_{uj}\right )\mathclose {}}_{j\in J}$ also lies in $\bar {\mathfrak {C}}$ .

Construction. From classes of families to classes of sets [frct-002N]

Conversely to the closure of a class of sets under change of base, we may take a class of families of sets $\mathfrak {F}$ to the the class of sets $\mathfrak {F}_{1}\subseteq {\mathscr {M}}$ spanned by sets $S$ such that the singleton family ${\mathopen {}\left \{S\right \}\mathclose {}}$ lies in $\mathfrak {C}$ .

Definition. Definable class of families of sets [frct-002P]

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

Intuition. [frct-002R]

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.

Lemma. Characterization of definable classes of families [frct-002T]

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 ${\mathopen {}\left (S_{i}\right )\mathclose {}}_{i\in I}$ not necessarily lying in $\bar {\mathfrak {C}}$ . Because $\mathfrak {C}$ is definable, the intersection $\mathfrak {C}\cap \bigcup _{i\in I}S_{i}$ is represented by a set $U$ . We therefore take the subset $J = {\mathopen {}\left \{i \in I\mid S_i\in U\right \}\mathclose {}}\subseteq I$ , and verify that the base change ${\mathopen {}\left (S_{j}\right )\mathclose {}}_{j\in J}$ is the largest approximation of ${\mathopen {}\left (S_{i}\right )\mathclose {}}_{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 ${\mathopen {}\left (u\right )\mathclose {}}_{u\in U}$ ; because $\bar {\mathfrak {C}}$ is definable, there is a largest subset $V\subseteq U$ such that the change of base ${\mathopen {}\left (v\right )\mathclose {}}_{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$ .

Bénabou’s notion of definability [frct-002S]

Jon Sterling

We will now construe set-theoretic definability as the instantiation at the fundamental self-indexing $\underline {\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, Jacobs, and Streicher.

Definition. Definable class in a fibration [frct-002W]

Jon Sterling

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_{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}$ .

Remark. [frct-002O]

Jon Sterling

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 fundamental self-indexing $\underline {\mathscr {M}}$ over $\mathscr {M}$ . Furthermore, $\mathscr {M}$ a definable class in $\underline {\mathscr {M}}$ if and only if it is a definable class of families of sets.

Opposite categories [frct-000Q]

Jon Sterling

We adapt Bénabou’s construction as reported by Streicher. Our first construction works for an uncloven fibration, but it has the downside that it requires us to treat the collection of cartesian lifts as a set that can be quotiented, whereas our second construction avoids this by virtue of a cleaving. Up to equivalence, the two constructions coincide for a cloven fibration, which shows that our second construction is independent of the chosen cleaving.

Construction. The opposite of an uncloven fibration [frct-001Z]

Let $E$ be fibered over $B$ ; we may define the opposite fibered category $E^{\mathsf {op}}$ over $B$ like so:

An object of $E^{\mathsf {op}}_{x}$ is given by an object of $E_{x}$ .
Given ${x}\xrightarrow {{f}}{y}\in B$ , a morphism $\bar {x}\xrightarrow [f]{} \bar {y}$ in $E^{\mathsf {op}}$ is given in terms of $E$ by a cartesian map ${\bar {y}_{x}}\xrightarrow [f]{\bar {y}_{f}}{\bar {y}}$ together with a vertical map ${\bar {y}_{x}}\xrightarrow [1_{x}]{h}{\bar {x}}$ as depicted below:

such that ${\mathopen {}\left \{\bar {x} \leftarrow \bar {y}_{x}^{1}\to \bar {y}\right \}\mathclose {}}$ is identified with ${\mathopen {}\left \{\bar {x}\leftarrow \bar {y}_{x}^{2}\to \bar {y}\right \}\mathclose {}}$ when they agree up to the unique vertical isomorphism $\bar {y}_{x}^{1}\cong \bar {y}_{x}^{2}$ induced by the universal property of cartesian maps in the sense that the following diagram commutes:

Construction. The opposite of a cloven fibration [frct-003W]

March 11, 2023
Jon Sterling

Let $E$ be a cloven fibration over $B$ ; in this case, we may use the cleaving of $E$ to give a simple construction of the opposite fibration $E^{\mathsf {op}}$ .

A displayed object of $E^{\mathsf {op}}$ over $x\in B$ is given by an object of $E$ over $x$ .
Given ${x}\xrightarrow {{f}}{u}\in B$ , a displayed morphism $\bar {x}\xrightarrow [f]{}\bar {y}$ in $E^{\mathsf {op}}$ is given by a vertical map ${f^{*}\bar {y}}\xrightarrow [1_{x}]{h}{\bar {x}}$ .

Going forward, we will not be sensitive to the difference between the two constructions of opposite fibrations.

Cartesian maps in the opposite category [frct-000T]

There is a simple characterization of cartesian maps in $E^{\mathsf {op}}$ .

Lemma. Characterization of cartesian maps [frct-0020]

A morphism ${\bar {x}}\xrightarrow [f]{\bar {f}}{\bar {y}}\in E^{\mathsf {op}}$ is cartesian over ${x}\xrightarrow {{f}}{y}$ if and only if the vertical leg of $f$ is an isomorphism.

Proof.

Suppose that ${\bar {x}}\xrightarrow [f]{\bar {f}}{\bar {y}}$ is represented by a span ${\mathopen {}\left \{\bar {x}\leftarrow \bar {y}_{x}\to \bar {y}\right \}\mathclose {}}$ in $E$ in which the vertical leg $\bar {x}\leftarrow \bar {y}_{x}$ is an isomorphism. We must show that ${\bar {x}}\xrightarrow [f]{\bar {f}}{\bar {y}}$ is cartesian in $E^{\mathsf {op}}$ . We fix a morphism ${\bar {w}}\xrightarrow [m;f]{\bar {h}}{\bar {y}}\in E^{\mathsf {op}}$ where ${w}\xrightarrow {{m}}{x}$ , depicted below in terms of $E^{\mathsf {op}}$ :

We must define the unique intervening map ${\bar {w}}\xrightarrow [m]{}{\bar {x}}$ in $E^{\mathsf {op}}$ . We first translate the above into the language of $E$ by unfolding definitions:

The desired intervening map $\bar {w}\xrightarrow [m]{} \bar {x}\in E^{\mathsf {op}}$ shakes out in the language of $E$ to be a span ${\mathopen {}\left \{\bar {w}\xleftarrow [1_{w}]{} \bar {y}_{w}\xrightarrow [m]{} \bar {x}\right \}\mathclose {}}$ in which the left-hand leg is vertical and the right-hand leg is cartesian over ${w}\xrightarrow {{m}}{x}$ . But the left-hand span ${\mathopen {}\left \{\bar {w}\xleftarrow [1_{w}]{}\bar {y}_{w}\to \bar {y}_{x}\cong \bar {x}\right \}\mathclose {}}$ in the diagram above is exactly what we need.

We leave the converse to the reader.

Cartesian lifts in the opposite category [frct-000U]

The foregoing characterization of cartesian maps in $E^{\mathsf {op}}$ immediately implies that $E^{\mathsf {op}}$ is fibered over $B$ .

Corollary. [frct-0021]

The displayed category $E^{\mathsf {op}}$ is a cartesian fibration.

Proof.

Fixing $\bar {y}\in E^{\mathsf {op}}_{y}$ and $f:x\to y\in B$ , we must exhibit a cartesian lift $\bar {f} : \bar {x}\xrightarrow [f]{}\bar {y}\in E^{\mathsf {op}}$ . By the characterization it suffices to find any map over $f$ whose vertical component is an isomorphism. Writing $\bar {y}_{x}\xrightarrow [f]{}\bar {y}$ for the cartesian lift of $f$ in $E$ , consider the map in $E^{\mathsf {op}}$ presented by the following span in $E$ :

Exegesis of opposite categories [frct-000S]

The construction of fibered opposite categories does appear quite involved, but it can be seen to be inevitable from the perspective of the fiber categories $E^{\mathsf {op}}_{x}$ . Indeed, let $u,v\in E^{\mathsf {op}}_{x}$ and fix a vertical map $h : u \to v\in E^{\mathsf {op}}_{x}$ ; by unfolding definitions, we see that the vertical map $h : u \to v$ is uniquely determined by a morphism $v\to u\in E_{x}$ .

Proof.

A displayed morphism $u\xrightarrow [1_{x}]{} v\in E^{\mathsf {op}}$ is determined by a span ${\mathopen {}\left \{u\leftarrow v_{x} \to v\right \}\mathclose {}}\in E$ where the right-hand map is cartesian over $1_{x} : x\to x$ and the left-hand map is vertical, taken up to the identification of different cartesian lifts $v_{x}\to x$ . A displayed morphism that is cartesian over the identity is an isomorphism; hence, displayed morphisms $u\xrightarrow [1_{x}]{} v\in E^{\mathsf {op}}$ are equivalently determined by vertical maps $v\to u \in E$ .

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

Jon Sterling

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.

Construction. Closure of a class of sets under base change [frct-002M]

Let $\mathfrak {C}\subseteq \mathscr {M}$ be a class of sets; there exists a class $\bar {\mathfrak {C}}$ of families of sets that contains ${\mathopen {}\left (S_{i}\right )\mathclose {}}_{i\in I}$ exactly when each $S_{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 ${\mathopen {}\left (S_{i}\right )\mathclose {}}_{i\in I}$ lies in $\bar {\mathfrak {C}}$ , then for any $u:J\to I$ , the base change ${\mathopen {}\left (S_{uj}\right )\mathclose {}}_{j\in J}$ also lies in $\bar {\mathfrak {C}}$ .

Construction. From classes of families to classes of sets [frct-002N]

Conversely to the closure of a class of sets under change of base, we may take a class of families of sets $\mathfrak {F}$ to the the class of sets $\mathfrak {F}_{1}\subseteq {\mathscr {M}}$ spanned by sets $S$ such that the singleton family ${\mathopen {}\left \{S\right \}\mathclose {}}$ lies in $\mathfrak {C}$ .

Definition. Definable class of families of sets [frct-002P]

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

Intuition. [frct-002R]

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.

Lemma. Characterization of definable classes of families [frct-002T]

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 ${\mathopen {}\left (S_{i}\right )\mathclose {}}_{i\in I}$ not necessarily lying in $\bar {\mathfrak {C}}$ . Because $\mathfrak {C}$ is definable, the intersection $\mathfrak {C}\cap \bigcup _{i\in I}S_{i}$ is represented by a set $U$ . We therefore take the subset $J = {\mathopen {}\left \{i \in I\mid S_i\in U\right \}\mathclose {}}\subseteq I$ , and verify that the base change ${\mathopen {}\left (S_{j}\right )\mathclose {}}_{j\in J}$ is the largest approximation of ${\mathopen {}\left (S_{i}\right )\mathclose {}}_{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 ${\mathopen {}\left (u\right )\mathclose {}}_{u\in U}$ ; because $\bar {\mathfrak {C}}$ is definable, there is a largest subset $V\subseteq U$ such that the change of base ${\mathopen {}\left (v\right )\mathclose {}}_{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$ .

Contributions

Reference. Distributors between fibrations [bénabou-streicher-2002]

2002
Jean Bénabou, Thomas Streicher
https://www2.mathematik.tu-darmstadt.de/~streicher/FIBR/DibFi.pdf

Reference. Fibered categories and the foundations of naïve category theory [benabou-1985]

1985
Jean Bénabou
The Journal of Symbolic Logic
10.2307/2273784

En hommage à Alexandre Grothendieck.

@article{benabou-1985,
  author = {B\'{e}nabou, Jean},
  publisher = {Cambridge University Press},
  year = {1985},
  doi = {10.2307/2273784},
  journal = {The Journal of Symbolic Logic},
  number = {1},
  pages = {10--37},
  title = {Fibered categories and the foundations of naive category theory},
  volume = {50},
}