24
$\begingroup$

It is a classical theorem of Freyd that if a small category is complete (has all small limits—in fact, having small products suffices), then it is a preorder (has at most one morphism between any two objects). The proof of this theorem (which can be found here or in CWM) is non-constructive, i.e. it uses the Law of Excluded Middle. Therefore, it can potentially fail in the internal logic of an elementary topos. And in fact, it does fail in the effective topos, and more generally in realizability topoi, where there do exist small complete categories that are not preorders.

However, I have heard it said that Freyd's theorem cannot fail in a Grothendieck topos; i.e. that a small complete category in a Grothendieck topos must still be a preorder—despite the fact that the internal logic is still in general intuitionistic, so that Freyd's proof cannot work. Can someone explain why this is, or (even better) give a reference containing a proof?

Improve this question
$\endgroup$
4
  • 3
    $\begingroup$ Good question. Since Grothendieck toposes are complete for higher-order intuitionistic logic we cannot hope to produce an internal argument. We have to use something about Grothendieck toposes, presumably cocompleteness. $\endgroup$
    – Andrej Bauer
    Commented Oct 24, 2010 at 21:31
  • 1
    $\begingroup$ The question can be reduced easily to the following. In a Grothendieck topos, suppose we have a mono $m : A \to B$ such that, for every object $I$, there is a mono $A^I \to B$. What can $A$ be? In $\mathsf{Set}$ it has to be empty or a singleton. $\endgroup$
    – Andrej Bauer
    Commented Oct 25, 2010 at 20:30
  • $\begingroup$ What do you mean formally for "internal complete category"? I find some different definitions about indexed categories (Sketches of an Elephant I, or Indexed Categories and their Applications, LNM 661). I formulate another one in terms of Kan extentions in the 2-cetegory of internal categories. How completeness is definible in the internal topos logic ?. this definition agree with the definitions of completeness of a indexed category? Excuse me for the mistakes and for the bad English, and thank for your time. $\endgroup$
    – Buschi Sergio
    Commented Nov 21, 2010 at 17:20
  • 1
    $\begingroup$ @Buschi, the paper "The Discrete Objects in the Effective Topos" has a fairly exhaustive discussion of the relevant notions of "completeness" for internal categories, in the context of showing that such categories do exist in the effective topos. $\endgroup$
    – Mike Shulman
    Commented Nov 22, 2010 at 0:30

1 Answer 1

Reset to default
13
$\begingroup$

Hi. I mentioned that I had thought about this on nForum a while back - sorry I didn't get back to you sooner. The following sketch of a proof is mainly due to Colin McLarty.

Two features which distinguish a Grothendieck topos from a more general topos are

  1. That it has a geometric morphism to Sets, namely the global sections functor.

  2. That it has an object of generators (i.e. there is an object G such that if $f,g: A \to B$ are not equal then there exists an arrow $h: G \to A$ with $fh \neq gh$)

Let $C$ be a small complete category object in a Grothendieck topos $T$ which is not a preorder. Then $C^G$ is also a small complete category in this topos essentially because exponentials commute. The global sections functor applied to $C^G$ gives a small complete category in the category of sets which is not a preorder (the property of being a small complete category is preserved by geometric morphisms, and the special property of G allows the property of being "not a preorder" to carry through), which is a contradiction.

It is a little easier to think about in the case of sheaves on some topological space. There a small complete category object which is not a preorder would have to fail to be a preorder on some open set, and the sections on that open set would be a small complete category which is not a preorder. $G$ takes the place of this open set above.

If you have any questions about this let me know. In particular I can write out all of the adjunctions showing various properties are preserved, but I don't want to get too nitty gritty if it isn't useful to you.

Kind regards, Steven Gubkin

Improve this answer
$\endgroup$
2
  • 4
    $\begingroup$ Thanks!! Does that proof really use boundedness (the existence of G)? If T is any Set-topos containing a small complete category C, then the adjunction argument seems to say that $\Gamma(C^G)$ is a small complete category in Set for any object G, hence a preorder; and thus the category T(G,C) is a preorder for any object G of T. Which should imply that C is a preorder in the internal logic of T, via Kripke-Joyal semantics. $\endgroup$
    – Mike Shulman
    Commented Dec 31, 2010 at 22:34
  • 5
    $\begingroup$ Also, it appears that the only property of Set used is that it is Boolean. If so, then something stronger is true: no topos which admits a (possibly bounded) geometric morphism to any Boolean topos can contain a small complete category. $\endgroup$
    – Mike Shulman
    Commented Dec 31, 2010 at 22:36

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .