Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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 k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum 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 sheaves 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

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 6th 2013
    • (edited Mar 6th 2013)

    Mentions of the category SetSet 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 SetSet is not a topos according to predicative mathematics. This could be very confusing. Similarly, there are some pages in the nLab that assume SetSet satisfies AC without batting an eye, while others discuss arcane weaker choice principles that SetSet 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 SetSet, 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 SetSet, 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 SetSet, 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 SetSet, say for example “SetSet 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.

    • CommentRowNumber2.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 6th 2013
    • (edited Mar 6th 2013)

    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.

    • CommentRowNumber3.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 6th 2013

    Thanks for mentioning this, David.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeMar 6th 2013

    The new intro looks nice to me, thanks! (Why would one say “axises”?)

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 6th 2013

    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”.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeMar 6th 2013

    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.

    • CommentRowNumber7.
    • CommentAuthorAndrew Stacey
    • CommentTimeMar 6th 2013

    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.

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 6th 2013
    • (edited Mar 6th 2013)

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

    • CommentRowNumber9.
    • CommentAuthorAndrew Stacey
    • CommentTimeMar 6th 2013

    Thinking further, “axises” and “basises” sounds a bit like Gollum doing mathematics.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeMar 6th 2013

    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 SetSet, only that it depends on whatever foundational system we choose. In ZFC, SetSet turns out to be a model of ETCS which also satisfies replacement. If ETCS is the foundation, then we’ve asserted directly that SetSet is a model of ETCS. If we use a foundation like IZF, then SetSet is an elementary topos, but is not Boolean and doesn’t satisfy choice. If we use a predicative foundation like CZF instead, then SetSet is only a Π\Pi-pretopos. Etc.

    • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 6th 2013
    • (edited Mar 6th 2013)

    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 XX as in Set/XSet/X, or a continuous domain as in Sh(X)Sh(X), 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 SetSet) and by Cohen, which are ostensibly categories of “constant sets”, both involve passage through a universe of variable sets (e.g., Set Set^\mathbb{N} on the way toward an ultraproduct Set /𝒰Set^{\mathbb{N}}/\mathcal{U} where the filterquotient is conceived as “freezing the variation” (Lawvere) at an ideal point = ultrafilter 𝒰\mathcal{U}). 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 SetSet, we might potentially mean a category of variable sets? Technically, the assumption that 11 is a generator is an effective way of restricting attention to “constant sets” and excluding the rest, and indeed the article Set declares that SetSet 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 SetSet 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 SetSet in the definition or Statement section. That would be fine with me if we are allowing ourselves to think of SetSet as potentially any topos (or Π\Pi-pretopos, etc.), but it would seem rather restrictive in scope if we insisted on the well-pointedness requirement for SetSet – and I think some rewriting would be in order to widen the scope to an appropriate degree. (Just mentioning SetSet 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!)

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeMar 6th 2013

    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. Set Set^{\mathbb{N}}) on the way to objects which look a little more set-like (e.g. Set /𝒰Set^{\mathbb{N}}/\mathcal{U}) 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, Set /𝒰Set^{\mathbb{N}}/\mathcal{U} 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.

    • CommentRowNumber13.
    • CommentAuthorTobyBartels
    • CommentTimeMar 7th 2013

    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, SetSet is special, in that one often (essentially if not directly) specifies the foundational axioms by specifying certain elementary properties of SetSet; and also because one shifts views by internalising in another category CC so as to treat CC as if it were SetSet. (But in both cases, SetSet is not always adequate; one may need to use Grpd\infty Grpd instead to capture everything.) So we should somewhere write about our pluralist approach to foundations, and we should also say on SetSet what that implies for what we believe about SetSet 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 EE 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 EE is in some sense SetSet; for example, EE need not even be well-pointed (although, like every topos, it will be internally well-pointed). So if one defines, say, WISCWISC as stating some property of SetSet, then points out that WISCWISC fails in the internal logic of EE, that doesn't mean that one thinks that EE might be SetSet.

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

    • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 7th 2013

    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 f,g:XYf, g: X \to Y, fx=gxf x = g x for all x:1Xx: 1 \to X implies f=gf = g. 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 EE 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 SetSet, then points out that WISC fails in the internal logic of EE, that doesn’t mean that one thinks that EE might be SetSet.

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

    • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeMar 7th 2013

    I would distinguish WISCWISC, tout court, from WISCWISC in EE. Any elementary statement about SetSet can be internalised into any topos (which is pretty much what I mean by ‘elementary’ in this context), and so this converts WISCWISC to WISCWISC in EE. But WISCWISC itself, as an axiom of mathematics, is the statement about SetSet.

    And it's only tradition and convenience that make all of these axioms about mathematics be statements about SetSet. You could take, as an axiom of mathematics, that the category Vect\mathbb{Q} Vect has enough projectives, and this would be different (weaker, I think) from COSHEPCOSHEP aka Aczel's presentation axiom, which is the statement that SetSet has enough projectives. (And then if you internalise this axiom in a topos EE, then it becomes yet another statement.)

    • CommentRowNumber16.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 7th 2013

    Okay, that’s a useful terminological point to keep in mind – thanks Toby. I think I now have enough information to go on.

    • CommentRowNumber17.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 7th 2013

    Indeed, Andreas Blass considers the axiom “AbAb has enough injectives” in his paper on SVC.

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeMar 8th 2013

    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

    SetSet 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 SetSet 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.

    • CommentRowNumber19.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 8th 2013

    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

    • SetSet satisfies AC,

    • Set ex/lexSet_{ex/lex} is a topos,

    • Set ex/lexSet_{ex/lex} 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 EE such that E ex/lexE_{ex/lex} is a topos but AC fails in EE, and there is a topos EE such that E ex/lexE_{ex/lex} is well-powered but not a topos. But I don’t know whether these statements still hold if EE is assumed to be well-pointed (and therefore I don’t know this for SetSet, 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?

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeMar 8th 2013

    A good question! I think the answer lies in an answer to the question “what is the internal ex/lex completion of a topos EE?” My first guess at what such a thing should be is the following: consider the self-indexing of EE, 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 EE. I don’t really have any intuition for whether, say, those counterexamples of Menni will still be counterexamples under this different construction.

    • CommentRowNumber21.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 9th 2013
    • (edited Mar 11th 2013)

    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.

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeMar 9th 2013

    (1) applies to me.

    • CommentRowNumber23.
    • CommentAuthorTobyBartels
    • CommentTimeMar 11th 2013

    I seem to have missed something vis-a-vis (2).

    • CommentRowNumber24.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 11th 2013
    • (edited Mar 11th 2013)

    Toby: [redacted] please, never mind. Sorry for noise.

    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeMar 11th 2013

    Even with the secret kept, I am not sure I understand: the entry would/should include a citation or acknowledgement. (?)

    • CommentRowNumber26.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 11th 2013

    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.

    • CommentRowNumber27.
    • CommentAuthorTobyBartels
    • CommentTimeMar 12th 2013
    • (edited Mar 18th 2013)

    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!