Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I added a note about this to Grothendieck topos. Also I fixed a mistake that Mike found in the classification at pretopos.
I missed some discussion about this topic in 2015. There, Jonas Frey shows that local smallness cannot follow from the others of Giraud's axioms, even in a fully classical setting, and explains why the Elephant seemed to say (but did not actually say) that it does. So local smallness must be explicitly stated.
That's fine for the classical setting (or even for the weakly predicative constructive setting), but what about strongly predicative foundations? There, it's not valid to state that even $Set$ is locally small; to a strong predicativist, function sets are (or may be) large. This means that what I wrote back in 2010 is wrong; it is not a theorem in predicative mathematics that every category of sheaves (of sets on a small site) is a Grothendieck topos, not by the definition currently on the page. And if we remove local smallness from that definition, then it will no longer be a theorem (even classically) that every Grothendieck topos is a category of sheaves.
So I'd like to find some condition, classically equivalent to local smallness but predicatively weaker, to use in Giraud's axioms, so that it will be a predicative theorem that a Grothendieck topos is precisely a category of sheaves. On a related MathOverflow thread (or rather, in an email that Todd copied there for me), I suggested the existence of a small generating set $G$ such that $\hom(G,X)$ is small for each $X$, combing the local smallness axiom with the generating set axiom. At that time, I wanted it to be the conclusion to a theorem (the predicative version of the alleged theorem that an infinitary pretopos with a generating set must be locally small), but that cannot be. However, could it still work as a hypothesis?
Is it true that every infinitary pretopos with such a generating set $G$ is a category of sheaves? Is it true that every category of sheaves has such a generating set? Classically, yes; even constructively and weakly predicatively, yes; the key is that the map $Hom(X,Y) \to Fun\big(Hom(G,X), Hom(G,Y)\big)$ is an injection when $G$ is generating (that's what it means to be generating), and $Fun\big(Hom(G,X), Hom(G,Y)\big)$ is small in weakly predicative mathematics (that's what it means for any predicativity to be weak^{1}). But is it true in strongly predicative mathematics? (Preferably in strongly predicative, weakly finitist, constructive mathematics.) If not, can we fix the condition on $G$ to make it work?
Possibly the answer to this is obvious, but I write it up while I think about it.
Confusingly, being weakly predicative means making stronger assumptions than being strongly predicative, namely the assumption that function sets are small. This is the opposite of how these adverbs are used with ‘finitist’ (so that a strong finitist makes classically false assumptions but a weak finitist does not). However, the term ‘weakly predicative’ is pretty well established in constructivist circles. ↩
1 to 2 of 2