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.
Mentions of the category occur all over the nLab, but with quite a bit of plasticity of meaning. I thought it might be good to have another look at the entry Set and try to describe this plasticity as considered along various axes, to help readers who might be puzzled by “just what does the nLab think the category of sets is?” For example, one reads that the category of sets has marvelous properties such as being a well-pointed topos, and then a little further down one sees that is not a topos according to predicative mathematics. This could be very confusing. Similarly, there are some pages in the nLab that assume satisfies AC without batting an eye, while others discuss arcane weaker choice principles that might satisfy. I think we need to be a just a bit more up-front about this, right on the page Set.
In the definition section on Set, I made a meager start on this by declaring that the nLab adopts a ’pluralist’ position on the matter of sets and , and jotted down a few of the possible axes (“axises”, if I were James Dolan) of meaning and interpretation that guide how one thinks of , e.g., predicative vs. impredicative, classical vs. intuitionist, selection of choice principles, and others. I didn’t think really hard about this, but it might suggest useful ways of organizing the page.
I left out other axes such as “structural vs. material”, and said nothing about type theory. The page set talked more about this; I envision Set as concentrating more on properties of the category of sets.
I got to thinking about this when I began to wonder how Toby thinks about , which is maybe different from how I usually think about it. (Usually it feels slightly alien to me to posit say WISC as a possible choice principle for the category of sets, which for me usually connotes a model of ETCS – normally I’d think of WISC instead as a possible axiom for a topos or a pretopos.) I was wondering whether Toby had a kind of “bottom line” for , say for example “ for me means at least a well-pointed topos with NNO, unless I choose to adopt a predicative mode”, or something like that. Anyway, discussion is invited.
Regarding WISC, there are models of ZF in which it fails, which give perfectly nice locally small cocomplete well-pointed toposes; I’m sure people would want to call the objects in those cases sets.
NB one of these was not intentionally created to break WISC, but was cooked up by a set theorist in the 80s, for entirely material set-theoretic purposes.
Regarding Toby’s position, I asked him this a little while back when I was first on Google+. I can’t remember the reply, but it wasn’t as minimal as I thought.
Thanks for mentioning this, David.
The new intro looks nice to me, thanks! (Why would one say “axises”?)
Because otherwise it looks just like the plural of ’ax’, maybe? (I say “ax-ees” if I want the plural of “axis”; what do other people say?)
Jim also says “basises”.
Yes, I’ve always known “ax-ees” as the correct plural of “axis”. My tongue stumbles over “axises”.
I suppose “ax-ees” might lead an unwary reader to say “ax-ee” for the singular? I have occasionally heard unwary speakers say “simplic-ee” instead of “simplex”. (-: But I really think this is somewhere that one should adhere to the established English language.
To add another data point, I say “aksees” for the plural of “axis” and “aksus” (well, somewhere between “aksus” and “akses”) for the plural of “axe”. No idea what an “ax” might be. Is it an old form of cow?
I think we’re probably safe under the contextual aegis here and can use “axes” with impunity.
Okay, sorry – it was a bit of a private joke, I admit. I’ll erase. (Andrew: I had originally written “axe”! then removed the e)
Okay, it’s gone now. But it amused me to note that my spellchecker thought “axises” was completely fine! (It did cough on “basises”, however.)
Thinking further, “axises” and “basises” sounds a bit like Gollum doing mathematics.
I also pronounce the plurals of “axis” and “axe” differently, even though they are spelled the same. The second vowel in the latter is a schwa for me.
But I apologize for derailing the conversation; now maybe we can get back to mathematics. (-: Personally, I wouldn’t say that I have any “bottom line” for , only that it depends on whatever foundational system we choose. In ZFC, turns out to be a model of ETCS which also satisfies replacement. If ETCS is the foundation, then we’ve asserted directly that is a model of ETCS. If we use a foundation like IZF, then is an elementary topos, but is not Boolean and doesn’t satisfy choice. If we use a predicative foundation like CZF instead, then is only a -pretopos. Etc.
Thanks, Mike. Let me make my question more precise.
Right, so here is the particular axis that prompted my looking into this in the first place: variability vs. constancy, which was a theme recurring in Lawvere’s Chicago Notes (1976 I think, and titled I think “Variable Sets, Etendu, and Variable Structure in Topoi”). As I read it, he was saying that the typical sort of Grothendieck topos, involving sets which vary over some domain (e.g. a discrete domain as in , or a continuous domain as in , or some other more complicated ’gros’ domain like finitely presented commutative rings), can lay legitimate claim to being a fundamental type of category of sets. He mentions that the universes of sets constructed by Robinson (an ultraproduct of ) and by Cohen, which are ostensibly categories of “constant sets”, both involve passage through a universe of variable sets (e.g., on the way toward an ultraproduct where the filterquotient is conceived as “freezing the variation” (Lawvere) at an ideal point = ultrafilter ). Likewise, according to the categorical point of view on forcing, we construct a “Cohen topos” of variable sets given by sheaves on an appropriately constructed complete Boolean algebra based on forcing conditions, and again “freezing” by modding out by an ultrafilter on the object of truth values (close to the Scott-Solovay method based on Boolean-valued sets).
So this is a plug for topos theory as a form of set theory – one leg of the elephant.
Now my question is: to what degree do we admit this axis in the nLab: that when we write , we might potentially mean a category of variable sets? Technically, the assumption that is a generator is an effective way of restricting attention to “constant sets” and excluding the rest, and indeed the article Set declares that is a well-pointed topos (provided that we are not wearing a predicativist’s hat). That sounds to me like a hidden commitment to taking “constancy” as a bottom line. Extending what you wrote, “if we use a foundation like IZF”, then is a not just a topos, but a well-pointed topos according to a traditional view. Is that well-pointedness a “bottom line”? That question was really what I was driving at in the penultimate sentence of #1.
See, a number of articles (e.g., the one on COSHEP or the one on WISC) refer specifically to in the definition or Statement section. That would be fine with me if we are allowing ourselves to think of as potentially any topos (or -pretopos, etc.), but it would seem rather restrictive in scope if we insisted on the well-pointedness requirement for – and I think some rewriting would be in order to widen the scope to an appropriate degree. (Just mentioning in an Idea section I would have no trouble with. Definitions are another story.)
(Some of my own contributions in such articles, recent and not-so-recent, were really about Grothendieck toposes, not constant sets. No one complained at the time!)
To me, a “set” is by nature I think what Lawvere would call a “constant” object. If we have a topos of variable objects, then that is not the category of sets, at least not in our current foundational system. But, we can instead move into a topos of variable objects and obtain a new internal mathematics in which the variable objects are treated as sets — but internally they are no longer visibly “variable” (although they may be, say, intuitionistic whereas our original constant sets were classical). However, I would always reserve the word “set” for something which our currently-in-force glasses view as non-variable.
I think this process of “internalization” is always what is happening when constructing a new model of set theory: we start with some “constant” notion of set, then we build some new objects which are not sets — but we can internalize and put on glasses which view those new objects as the (constant) sets. The fact that we pass through some objects which look a little less set-like (e.g. ) on the way to objects which look a little more set-like (e.g. ) seems to me irrelevant: neither of these kinds of objects are sets in the original world, so in both cases we have to put on internalization glasses to treat them as such.
In particular, yes, I would always insist that the category of sets is well-pointed, but well-pointedness is not what defines the category of sets, it’s merely a property of the category of sets. For instance, is well-pointed, but it is not the category of sets. If we ignore size considerations, then for me there is always (that is, no matter what pair of glasses I am currently looking through) only one “category of sets”, even if changing my glasses changes the referent of that phrase.
I think that it's good that we talk about this, but I'm not sure that Set is the right place for it. We could just as well go to, say, Grp and talk about how various elementary features of that category (such as whether it has enough projectives) depend on which foundational axioms we adopt. Of course, is special, in that one often (essentially if not directly) specifies the foundational axioms by specifying certain elementary properties of ; and also because one shifts views by internalising in another category so as to treat as if it were . (But in both cases, is not always adequate; one may need to use instead to capture everything.) So we should somewhere write about our pluralist approach to foundations, and we should also say on what that implies for what we believe about in particular, but those are two slightly different subjects.
Another issue is that if you want to show that a certain result is not valid, say, constructively, then one way to do it is to find a model of (constructive) mathematics in which it fails. In particular, if you can find a topos with NNO in whose internal logic the result is false, then we know that it can't be proved constructively (at least for one reasonable definition of ‘constructive’). But that doesn't mean that is in some sense ; for example, need not even be well-pointed (although, like every topos, it will be internally well-pointed). So if one defines, say, as stating some property of , then points out that fails in the internal logic of , that doesn't mean that one thinks that might be .
And to comment on something important: both ‘ax’ and ‘axe’ are accepted spellings (at least in the U.S.) for the singular of ‘axes’ (when pronounced with a neutral vowel in the second syllable).
Thanks to you both, Mike and Toby, for your responses.
Toby, is there a current page where you think this general discussion would be better situated?
neither of these kinds of objects are sets in the original world
Sure, I think we can all agree on that as a truism. :-) More telling and useful to me were the phrases that came before (“a little less set-like… a little more set-like”).
In particular, yes, I would always insist that the category of sets is well-pointed, but well-pointedness is not what defines the category of sets, it’s merely a property of the category of sets.
Of course I agree well-pointedness doesn’t define the category of sets. No property can “define” the category of sets. (We agree of course that “well-pointedness” refers to an external property of the topos, that for , for all implies . Internal well-pointedness being vacuous.) Otherwise, it’s good to have you respond with definiteness on this particular “variability-constancy” axis.
Another issue is that if you want to show that a certain result is not valid, say, constructively, then one way to do it is to find a model of (constructive) mathematics in which it fails. In particular, if you can find a topos with NNO in whose internal logic the result is false, then we know that it can’t be proved constructively (at least for one reasonable definition of ‘constructive’).
Okay, thanks very much for the corroboration here. I’ll go back through some of the nLab pages where I made some recent additions, to make sure I remembered to check in the internal logic of the topos. (And I should probably go back to CSB, to make the comment on internalness look like less of an afterthought.)
So if one defines, say, WISC as stating some property of , then points out that WISC fails in the internal logic of , that doesn’t mean that one thinks that might be .
The last phrase is consonant with what Mike said, and I agree. But I still think it would make sense to state WISC or COSHEP or axiom of multiple choice so that the property could refer to any topos, not just “the category of sets”. For example, it’s very handy to know that COSHEP holds in simplicial sets, and in the effective topos.
So unless an objection is voiced, I would like to make appropriate changes in those statements. (If one wants to comment that some such choice principle originally cropped up in constructivist set theory per se, that’s of course fine with me.)
I would distinguish , tout court, from in . Any elementary statement about can be internalised into any topos (which is pretty much what I mean by ‘elementary’ in this context), and so this converts to in . But itself, as an axiom of mathematics, is the statement about .
And it's only tradition and convenience that make all of these axioms about mathematics be statements about . You could take, as an axiom of mathematics, that the category has enough projectives, and this would be different (weaker, I think) from aka Aczel's presentation axiom, which is the statement that has enough projectives. (And then if you internalise this axiom in a topos , then it becomes yet another statement.)
Okay, that’s a useful terminological point to keep in mind – thanks Toby. I think I now have enough information to go on.
Indeed, Andreas Blass considers the axiom “ has enough injectives” in his paper on SVC.
No property can “define” the category of sets.
Okay, agreed. I think my phrase that this replies to was partly in response to what you wrote:
…the category of sets, which for me usually connotes a model of ETCS
and
“ for me means at least a well-pointed topos with NNO, unless I choose to adopt a predicative mode”
which seemed to me to suggest you were viewing as (or at least suggesting that some might view it as) defined by being a category with some properties. But I guess you were just saying that whatever foundation one is working in, the category of sets always happens to have such and such properties, although those properties do not define it (cf. difference between “connote” and “denote” I guess).
But I still think it would make sense to state WISC or COSHEP or axiom of multiple choice so that the property could refer to any topos
Sure! (Although “COSHEP” is probably not a good name for an axiom referring to arbitrary topoi; perhaps we should use “presentation axiom” instead, or just say that the topos “has enough projectives”.) It may get a little bit fiddly, though, since in the general case some axioms of this sort have distinct “external” and “internal” versions, e.g. external AC is strictly stronger than internal AC for a topos. But as long as we’re clear what we mean, I think this is a good idea.
But I guess you were just saying that whatever foundation one is working in, the category of sets always happens to have such and such properties, although those properties do not define it
Yes, that’s exactly what I meant. :-)
So as long as we’re talking about this, let me run something past you guys. Recently I added some material to generic proof which intimated that the sequence of conditions
satisfies AC,
is a topos,
is well-powered
should be strictly decreasing in strength (which one of you, Mike I think it was, thought would be true but were asking about). What I actually indicated, by referring to work of Menni, is that there is a topos such that is a topos but AC fails in , and there is a topos such that is well-powered but not a topos. But I don’t know whether these statements still hold if is assumed to be well-pointed (and therefore I don’t know this for , whatever is meant by that). Can this be beefed up to a demonstration which would settle Mike’s question? For example, can the second and third conditions be recast in “elementary” form, in Toby’s sense in #15?
A good question! I think the answer lies in an answer to the question “what is the internal ex/lex completion of a topos ?” My first guess at what such a thing should be is the following: consider the self-indexing of , take its fiberwise ex/lex completion, and then stack-complete the result. (Richard Garner pointed out when I mentioned this to him today that it’s not a priori obvious that the result of stack completion will still be fiberwise exact. I think it ought to be, but if it isn’t, then you might have to iterate.) In general this seems like even the fiber over 1 of this resulting stack may be quite different from the “external” ex/lex completion of . I don’t really have any intuition for whether, say, those counterexamples of Menni will still be counterexamples under this different construction.
Thanks, Mike! Incidentally, I noticed there’s no nLab article on stack completion. [redacted, but mentioned possibilities labeled (1) and (2)]
Anyway, thanks for your (and Richard’s) thoughts. Definitely gives food for thought.
(1) applies to me.
I seem to have missed something vis-a-vis (2).
Toby: [redacted] please, never mind. Sorry for noise.
Even with the secret kept, I am not sure I understand: the entry would/should include a citation or acknowledgement. (?)
Urs: it goes without saying that appropriate citations etc. should be included. Otherwise, please – never mind. It was stupid to have brought this up. I’m redacting prior comments now, and I doubly apologize for noise.
Now I seem to have missed something in a 6-hour period between when Todd made a comment and when he edited it. But that's OK!
1 to 27 of 27