# Grothendieck Topos

If,

1. A Grothendieck Topos is equivalent to the Category of sheaves on some site (C,J).
2. A presheaf (on site (C,J)) is a contravariant functor P, from category C to the category of sets. A sheaf is a pre-sheaf equipped with a matching families map, from the sieves of J(B) to elements of PB (for any object B of category C).
3. A Grothendieck Topos is also an Elementary Topos which obeys Giraud's axioms.

Then,

The main definition of a Grothendieck Topos in 1 and 2, explicitly refers to the category of sets. Sets can be formalized several different ways: PA, ZF(C), NBG. I presume this choice would impact in turn the definition of Grothendieck Topos.

The alternative definition in 3 of Grothendieck Topos, through Elementary Topoi, does not explicitly refer to sets or the category of sets. What formalization of sets is assumed in this definition? Else, what have I overlooked?

• I don't know what definition of Grothendieck topology in terms of elementary topoi you have in mind, but the category of sets is usually assumed to be axiomatized by ZFC. There aren't any common variations that make any difference other than perhaps removing choice-note for instance that NBG, as a conservative extension of ZFC, has the same category of sets in a strong sense. – Kevin Carlson Jul 3 '17 at 16:35
• I am referring to ncatlab.org/nlab/show/Grothendieck+topos#Giraud. What is interesting is that section seems to say that Elementary Topoi do not require a choice wrt to Sets. It seems Giraud's theorem, which bridges the concepts of Grothendiek Topos and Elementary Topos, is the step where the choice of sets comes in... – dumb0 Jul 3 '17 at 16:42
• Ok, but nothing at your link says anything about a link between elementary toposes and Grothendieck topologies. Are you aware that topologies and toposes are not the same thing? – Kevin Carlson Jul 3 '17 at 18:00
• I was being sloppy with terminology and have corrected the question since. A Grothendieck topology is the mapping J. My question refers not to a Grothendieck topology but a Grothendieck topos. – dumb0 Jul 3 '17 at 18:57
• Giraud's axioms stand on their own; they don't require the Grothendieck topos to (a priori) be an elementary topos. In sufficiently strong foundations, they imply that a Grothendieck topos is an elementary topos, but in weaker foundations this can't be proven. – Derek Elkins Jul 3 '17 at 23:21

Giraud's axioms do explicitly refer to the category of sets, through every use of the term "small". E.g. taking the formulation at ncatlab, the category of sets is explicitly referred to by the requirement that $E$ be locally small, and that $E$ have all small coproducts.
I don't know nearly as much about it as I like, but I understand you can replicate broad swaths of the theory of Grothendieck toposes starting from any base topos $S$: you can talk about internal sites, internal presheaves, and internal sheaves, and then the toposes $E$ that comes with a bounded geometric morphism $E \to S$ are precisely those toposes that are equivalent to a categories of internal sheaves over an internal site. e.g. see base topos and bounded geometric morphism from ncatlab.
You don't necessarily have to see $Set$ as classical set theory axiomatized by e.g. $ZFC$, $NBG$ or the like. Instead you can think of $Set$ as being characterized as an abstract category without any reference to classical set theory (i.e. without reference to membership relation).