12
$\begingroup$

There is on the nLab page "Grothendieck topos" a part about the theory of Grothendieck toposes in weak foundation.

It claims that the equivalence for a category between the Giraud's axioms and being a category of sheaves over a site can be proved under very weak foundation: predicative (even without small set of functions), finitarist, constructive.

I would really like to know if there is some references about this or if someone has thought about it and could explain some details about this that seems a bit obscure to me.

I am especially concern by the absence of sets of functions: without them Grothendieck toposes shouldn't be expected to be locally small, hence it does not seem possible to associate a sheave to an object $X$ being given a set of generators (because the sheave should be $Hom( \_ , X)$ which might not be a set). Maybe the theorem still holds by constructing a localization functor from a presheaves category to the "category of sheaves" but without a right adjoint, hence sheaves should not be set valued functors.

Also, it is not clear what a Grothendieck topology should be (more precisely what should be small ? this might explains the fact that sheafication don't preserve smallness )

I would also be interested in knowing if it is possible to weaken even further the foundations, for example by getting ride of quotient sets and still have a result of this kind.

Improve this question
$\endgroup$
5
  • 3
    $\begingroup$ The section "Weak Foundations" first appears in Revision number 27, written by Toby Bartels. I may drop him a note about your post. $\endgroup$
    – Todd Trimble
    Commented Aug 13, 2015 at 20:42
  • 1
    $\begingroup$ Simon, you may be interested to know that there are (non-Grothendieck) boolean toposes that are not locally small: as such they have internal homs, which are the 'correct' 'set' of functions (working in the internal logic). These correspond to certain class-forcing models. Regarding a Grothendieck topology, one could replace it by a Lawvere-Tierney topology/local operator and see what one gets. $\endgroup$
    – David Roberts ♦
    Commented Aug 14, 2015 at 0:20
  • 1
    $\begingroup$ That is indeed interesting. But Under weak fundation Grothendieck toposes are not going to be elementary topos, they are not expected to be cartesian closed if "sets" is not, and they are not going to have power objects if there is no power objects in "sets", so I'm sure one can use locale operators here either. $\endgroup$
    – Simon Henry
    Commented Aug 14, 2015 at 7:59
  • 1
    $\begingroup$ We can think about universal closure operators instead of local operators. $\endgroup$
    – Zhen Lin
    Commented Aug 14, 2015 at 9:35
  • 1
    $\begingroup$ Indeed we can, but as I mentioned it is not clear that sheaves should be a subcategory of small presheaves (the situation might be similar to what happen when you have a large site: the sheafification of a small presheaves might not be a small presheaf and what we want to consider is the category sheaves which are sheafication of small presheaves), in which case the closure operation is not a solution either... $\endgroup$
    – Simon Henry
    Commented Aug 14, 2015 at 10:02

1 Answer 1

Reset to default
5
$\begingroup$

(Toby Bartels wrote back, explaining that he was having some trouble logging in to his account here, but asking if I could post some comments he had. I'm going to post them under my name as Community Wiki, and invite him to edit this answer further once he's back, if he'd like -- or he can post separately of course.)

I believe that local smallness follows (in conventionally strong foundations) from the other axioms (this is what the Elephant seems to say in C.2.2.8.vii), so the right thing to do should just be to remove it from the list of axioms, which I have now done at the nLab. However, it would be good to have the argument written out in a clearly predicative way, to be certain. I no longer have access to my copy of the Elephant (I had to check the wording of C.2.2.8 in Google Books), which I believe was my guide the last time that I was thinking through this, but hopefully I can find it in the library and extract an explicitly predicative and constructive argument from its proofs.

More speculatively, the classical proof that Giraud's axioms imply local smallness might have a strongly predicative variation proving, say, that there is a small generating set (possibly smaller than the original one) $G$ such that $\hom(G,X)$ is small for each $X$. That solves your problem of getting a Set-valued sheaf from an object, and it's trivial (but impredicative) to prove that a category with such a generating set must be locally small. But I'm not sure that it's actually correct!

Improve this answer
$\endgroup$
7
  • 1
    $\begingroup$ Thank you ! If the last paragraph is true that would be indeed very interesting... But I don't really see how one can get something like that. Or maybe we take it as an additional assumption on the sets of generators ? $\endgroup$
    – Simon Henry
    Commented Aug 14, 2015 at 10:05
  • 1
    $\begingroup$ Ok, reading the elephant it seems that the trick is that one ask for the object of the separating sets to have have small set of maps out of it... $\endgroup$
    – Simon Henry
    Commented Aug 14, 2015 at 20:31
  • 1
    $\begingroup$ I've gotten back into M.O, but I'm not ready to answer yet, since I'm waiting on getting ahold of the Elephant again. In the meantime, Simon's last comment seems very plausible. Then my last paragraph would not be a theorem, but would have to be an additional hypothesis. If so, I'll edit the nLab article accordingly. (Or if anybody else feels confident about this, then you also have the right to edit the nLab article.) $\endgroup$
    – Toby Bartels
    Commented Aug 25, 2015 at 21:08
  • 1
    $\begingroup$ For now, I've added some hedging and a pointer here to the nLab page. $\endgroup$
    – Toby Bartels
    Commented Aug 25, 2015 at 21:20
  • 1
    $\begingroup$ On the question whether local smallness is implied by the axioms in classical strong foundations, what is wrong with the following counterexample? Assume that U and V are two Grothendieck universes, with U contained in V. Then V is exact and extensive and has a U-small coproducts and a U-small separating set (in fact 1 alone separates). Thus V satisfies the hypotheses of Giraud's theorem relative to U. However, V is not locally small relative to U. This shows that local smallness is not implied by Giraud's axioms. Did I overlook something? $\endgroup$
    – Jonas Frey
    Commented Aug 26, 2015 at 13:21

You must log in to answer this question.

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