Problèmes dans les topos
by
translated by Jonathan Sterling
This is a hypertext English translation of Bénabou’s famous report Problèmes dans les topos; errors in translation belong to me alone. I have taken some liberties to ensure readability. Node numberings of the form 1.2.3 are guaranteed to be the same as in the source text; in places, I have introduced more granular node subdivisions than Bénabou; for instance, a subnode of 1.2.3 introduced in translation could be numbered 1.2.3·a. I have added titles to many sections in order to facilitate a useful table of contents.
The original French manuscript of Bénabou can be accessed here.
1. A few reminders [0000]
An elementary topos is a category $\ECat$ satisfying the following conditions:
- $\ECat$ inductive and finite projective limits;
- $\ECat$ admits exponentials: for each $A\in \Ob{\ECat}$, the functor $(-)\times A : \ECat\to\ECat$ admits a right adjoint, written $\prn{-}\Sup{A}$;
- $\ECat$ has an arrow $v : \ObjTerm{\ECat}\to \Omega$ that for each $X\in \Ob{\ECat}$ the arrows from $X$ to $\Omega$ give by fibered product with $v$ exactly the subobjects of $X$.
We can reduce these axiomatics, as recent work by A. Kock and Ch. Mikkelson (Hurd & Loeb, 1974) has shown, and describe for example in the manner of F.W. Lawvere (Lawvere, 1972) an elementary topos as a cartesian closed category in which the notion of a subobject is representable.
We know that for a topos $\ECat$ the embedding functor into the category $\ECat\Sub{p}$ of partial morphisms admits a right adjoint. This property can also be substituted for axiom (3) of 1.1 [0001].
We will describe a different embedding of interest below.
We also know that for each object $X$ of a topos $\ECat$, the category $\Sl{\ECat}{X}$ of objects above $X$ is again a topos, and that each arrow $f : X \to Y$ determines a functor $\InvImg{f} : \Sl{\ECat}{Y}\to\Sl{\ECat}{X}$ which admits both a left adjoint (written $\Sigma\Sub{f}$) and a right adjoint (written $\Pi\Sub{f}$).
If we consider just the subobjects of $X$, we obtain a Heyting algebra $\Opns{X}$ and the functor $\InvImg{f}$ induces $f\Sup{-1} : \Opns{Y}\to \Opns{X}$, which likewise admits a right adjoint ($\forall\Sub{f}$, induced by $\Pi\Sub{f}$) and a left adjoint (written $\exists\Sub{f}$, defined by taking the image). By the cartesian adjunction, the objects of $\Opns{X}$ amount to points of $\Omega\Sup{X}$ and the action of the last three functors can be described by arrows of the topos. Thus restricting the image of $A\times f$ to a subobject of $A\times X$ amounts to composing the cartesian adjoint of its characteristic function with the arrow $\exists\Sub{f} : \Omega\Sup{X}\to\Omega\Sup{Y}$, which corresponds exactly to the restriction of the image of $\Omega\Sup{X}\times f$ to $\in\Sub{X}\rightarrowtail \Omega\Sup{X}\times X$ (the subobject characterized by evaluation).
I have taken some liberties with the wording involving images in 1.3 [0003] in order to conform with English mathematical usage; for instance, I have translated phrases like “prendre l’image par $f$ d’un sous-objet de $X$” as “restricting the image of $f$ to a subobject of $X$”.
We note that Bénabou writes “adjonction cartésienne” to refer to the product-exponential adjunction $\prn{-}\times X \dashv \prn{-}\Sup{X}$. Although this terminology is not current, we have retained it as “the cartesian adjunction”.
Another aspect of Bénabou’s terminology that we have retained is the use of “adjoint” to mean “adjoint transpose”; for instance, Bénabou speaks of the “cartesian adjoint” $T\times X\to Y$ of a morphism $T\to Y\Sup{X}$.
1.4. Relations in a topos [0005]
We may define the category of relations in the topos $\ECat$ (written $\REL{\ECat}$) in the following manner:
- we set $\Ob{\REL{\ECat}} = \Ob{\ECat}$;
- an arrow from $X$ to $Y$ in $\REL{\ECat}$ is a subobject of $X\times Y$ in $\ECat$ — more precisely an arrow from $X\times Y$ into $\Omega$;
- the composition of $\phi:X\times Y\to \Omega$ and $\psi:Y\times Z\to\Omega$ is done by taking the fibered product $P$ over $Y$ of the subobjects corresponding to $\phi$ and $\psi$ and taking the characteristic function of the image of $P$ in $X\times Z$.
The verification of the fact that $\REL{\ECat}$ is a category is left to the reader.
We embed $\ECat$ into $\REL{\ECat}$ by associating to $f : X\to Y$ the arrow $\prn{\Idn{X},f} : X \to X\times Y$; this embedding factors through the (obvious) embedding of $\ECat\Sub{p}$ into $\REL{\ECat}$.
The embedding $I$ of $\ECat$ into $\REL{\ECat}$ admits a right adjoint.
Proof. Since for each $X,Y\in\Ob{\ECat}$ we have
we see that the functors $\REL{\ECat}\brk{I\prn{-},Y}$ are representable.
There is therefore an adjoint, whose value at $Y$ is $\Omega^Y$. Let us explain its value on morphisms: a morphism $\phi:X\to Y$ in $\ECat$ is sent to the morphism $\Omega^\phi:\Omega^X\to \Omega^Y$ in $\REL{\ECat}$ defined as the cartesian adjoint to the characteristic function of the subobject of $\Omega^X\times Y$ obtained by taking the image of the fibered product of $\in\Sub{X}$ and $R\Sub{\phi}$ over $X$.
In $\SET$, we find that $\Omega^\phi$ sends each $X\tick\subseteq X$ to $\brc{y \mid \prn{\exists x} \prn{x\in X\tick \text{ and } \phi\prn{x,y} \text{ is true}}}$.
If $\phi$ corresponds to the graph of an operation $f:X\to Y$, then $X\tick$ is sent to $\brc{y\mid \prn{\exists x}\prn{x\in X\tick \text{ and } y=f\prn{x}}}$. ∎
This suggests that by preceding the adjoint in question by the embedding $I$ we shall obtain the “existential quantification” (which sends $X$ to $\Omega\Sup{X}$ and $f$ to $\exists\Sub{f}$) from $\ECat$ to $\ECat$. Indeed, the image of the fibered product of $\in\Sub{X}$ and $\prn{\Idn{X},f}$ — therefore of $\in\Sub{X}$ — over $\Omega\Sup{X}\times Y$ is indeed the vertical composite depicted below:
2. The object of monos [000A]
Let $X$ and $Y$ be two objects of a topos $\ECat$. We propose to define a subobject of $Y\Sup{X}$ whose points correspond exactly to monomorphism from $X$ to $Y$.
A mono from $X$ to $Y$ is characterized by the fact that its kernel pair is the diagonal of $X$.
The characteristic function of the diagonal $\Delta\Sub{X}$, written $\gl{=\Sub{X}}$, has the arrow ${=\Sub{X}} : \ObjTerm{\ECat}\to \Omega\Sup{X\times X}$ for its cartesian adjoint.
The “kernel pair” operation from $Y\Sup{X}$ to $\Omega\Sup{X\times X}$ (written $\hat{\phi}$) can be obtained as the adjoint of the arrow from $Y\Sup{X}\times X\times X$ to $\Omega$ that classifies the subobject $k:K\rightarrowtail Y\Sup{X}\times X\times X$ equalizing the following two horizontal maps:
(that is to say, in $\SET$, the set of triples $\prn{f,x\Sub{1},x\Sub{2}}$ such that $f\prn{x\Sub{1}} = f\Sub{x\Sub{2}}$).
The object $\ObjMono{X}{Y}$ is then defined by the following fiber product:
We have translated Bénabou’s “équivalence nucléaire” as “kernel pair”. We have translated Bénabou’s “noyau du couple” as “equalizer” — a usage of the French school that is explained by Grothendieck in his 1965-1966 lectures on basic category theory (Introduction Au Langage Fonctoriel, 1966, I.6.3.2). I have also renamed some of the labels in the first commutative diagram of Definition 2.1 [000B] for clarity.
2.2. Universal property of the object of monos [000C]
For each object $T$ of the topos $\ECat$, we have a natural bijection $\Hom{\ECat}{T}{\ObjMono{X}{Y}}\cong \Monos{\Sl{\ECat}{T}}{X\times T}{Y\times T}$ (the second term representing the set of monomorhpisms from $X\times T$ to $Y\times T$ in $\Sl{\ECat}{T}$).
Proof. Via the cartesian adjunction, the arrows $g:T\to Y\Sup{X}$ correspond bijectively to arrows $\hat{g} : T\times X \to Y$; the latter are in bijection with arrows $g\tick = \prn{\hat{g},p} : T\times X \to T\times Y$, where $p$ denotes the projection $T\times X \to T$.
We also show that the condition “$\hat{\phi}$ factors through $=\Sub{X}$” is equivalent to “$g\tick$ is a mono”. But the first amounts to the commutativity of the inner rectangle below:
The annotation $\text{(f.p.)}$ follows Bénabou’s $\text{(p.f.)}$ in the diagram in the proof of Proposition 2.2·a [000D] and denotes a fibered product square, i.e. a cartesian square.
If the rectangle commutes, the composite $\prn{g\times X\times X}\circ\prn{T\times \Delta}$ factors through $K$ as $k\circ\bar{g}$ and the square $(1)$ is a fiber product (taking account of the fact that $T\times\Delta$ is a mono); likewise, if the fibered product of $k$ and $g\times X\times X$ is a square of type $(1)$, then the inner rectangle is commutative (by associativity of fibered products).
The condition on $(1)$ will turn out to be satisfied if and only if $T\times \Delta$ is the equalizer of the composites $\Con{ev}\circ \prn{T\times\pi\Sub{1}}$ and $\Con{ev}\circ \prn{T\times\pi_2}$ (according to a classical lemma) the composites $\hat{g}\circ \prn{T\times\pi\Sub{1}}$ and $\hat{g}\circ\prn{T\times\pi\Sub{2}}$.
It remains to show that this property is equivalent to the fact that $\prn{\hat{g},p}$ is a mono, which can be verified in terms of sets: if we denote by $\prn{t,x\Sub{1},x\Sub{2}}$ an arbitrary element of $T\times X\times X$, the two properties amount to the condition “$\hat{g}\prn{t,x\Sub{1}} = \hat{g}\prn{t,x\Sub{2}}$ entails $x\Sub{1}=x\Sub{2}$”. ∎
If $T=\ObjTerm{\ECat}$, we obtain a natural bijection
Thus the points of $\ObjMono{X}{Y}$ correspond exactly to the monos from $X$ to $Y$ in $\ECat$. But these do not entirely determine the object $\ObjMono{X}{Y}$.
2.3. Composition of monos [000F]
If $X$, $Y$, $Z$ are objects of a topos $\ECat$, there exists a unique arrow from $\ObjMono{X}{Y}\times\ObjMono{Y}{Z}$ to $\ObjMono{X}{Z}$ factorizing the composition $\Con{C}$ from $Z\Sup{Y}\times Y\Sup{X}$ to $Z\Sup{X}$.
Proof. TODO
TODO
Bibliography
-
Kock, A., & Mikkelsen, C. J. (1974). Topos-theoretic factorization of non-standard extensions. In A. Hurd & P. Loeb (Eds.), Victoria Symposium on Nonstandard Analysis (pp. 122–143). Springer Berlin Heidelberg.Details
-
Lawvere, F. W. (1972). Introduction. In F. W. Lawvere (Ed.), Toposes, Algebraic Geometry and Logic (pp. 1–12). Springer Berlin Heidelberg.Details
-
Grothendieck, A. (1966). Introduction au Langage Fonctoriel. https://agrothendieck.github.io/divers/ilfg.pdfDetails