Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorTobyBartels
   • CommentTimeAug 6th 2010
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI added a note about this to [[Grothendieck topos]]. Also I fixed a mistake that Mike found in the classification at [[pretopos]].

   I added a note about this to Grothendieck topos. Also I fixed a mistake that Mike found in the classification at pretopos.

2. • CommentRowNumber2.
   • CommentAuthorTobyBartels
   • CommentTimeApr 5th 2017
   • (edited Apr 5th 2017)
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI missed [some discussion about this topic](https://nforum.ncatlab.org/discussion/6753/grothendieck-topos/) 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](http://mathoverflow.net/questions/214737/grothendieck-toposes-in-very-weak-foundation) (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[^weakly]). 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? [^weakly]: 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. Possibly the answer to this is obvious, but I write it up while I think about it.

   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¹). 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.

   ---

   1. 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. ↩