Subtoposes of Eff

Subtoposes of Eff

[Prof. Peter Johnstone]

Readers of Jaap van Oosten's new book on realizability will have
come across the statement on p. 235 that the question "Is Set the
only Grothendieck topos which occurs as a subtopos of the effective
topos?", which Ieke Moerdijk asked him at his Ph.D. viva in 1991,
is still unanswered. In fact I've known the answer to this question
for at least five years: I referred to it in my talks at the European
category theory meeting in Haute-Bodeux (September 2003) and the
meeting on Ramifications of Category Theory in Firenze (November 2003).
However, the proof hasn't been published anywhere (it will of course be in
volume 3 of the Elephant when that is published -- and please don't
ask me to predict when that will be!), so I thought I should let people
know about it.

We work in the realizability topos over an arbitrary pca A (all
unexplained notation can be found in Jaap's book). Andy Pitts showed
in his thesis that local operators on this topos correspond to maps
j: PA --> PA whch "are nuclei in the logic of A-realizability", and
that the corresponding subtopos of sheaves is equivalent to Set (or
degenerate) iff the intersection \bigcap_{a \in A} j({a})
is inhabited. Suppose this condition fails;
we shall show that the subtopos of j-sheaves is not complete.
Let A_1 denote the assembly with underlying set A and
[[a \in A_1]] = {a} for all a, and A_2 the assembly with the
same underlying set and [[a \in A_2]] = j({a}). Note that A_2 is the
j-closure of A_1 in \nabla A, and hence its associated j-sheaf.
Also, by the assumption we've made, it is not the whole of \nabla A.

We claim that the product of A copies of A_2 cannot exist in the
topos of sheaves: if it did, it would obviously be a subobject of
\nabla(A^A) (the latter being the product of A copies of \nabla A)
and hence an assembly; moreover, its underlying set would be the
whole of A^A since the forgetful functor from assemblies to Set
(is representable, and hence) preserves all products which exist.
Writing P for the product, for each a \in A the a^th projection
A^A --> A must be trackable as a morphism P --> A_2; let e_a be
an element of A which tracks it. Since A_2 is not the whole of
\nabla A, we can find f(a) such that e_aa \not \in [[f(a) \in A_2]]
(if e_aa is undefined, choose f(a) to be any element of A). Then
f: A --> A has no realizers as a member of P.

Peter Johnstone