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.
I’ve finally knocked my scrappy notes for my IHES talk into shape, modulo the statement of Theorem 3; you can see the pdf notes here. I aimed for an informal tone, since these are not going to be published, but they are the only written record of this stuff, and it would take me longer, given my current time constraints, to write a full account.
Comments are most welcome.
Nice notes!
Since it is illegal to discuss good material on the nForum which is not reflected on the nLab, I have added pointer to them here.
p. 2, bottom: “beha[v]iour”
p. 3, what’s the purpose of footnote 6?
p. 9 bottom: “axiom [of] choice”
Thanks, Urs!
p. 3, what’s the purpose of footnote 6?
Not much, just a curiosity that at the time I thought was cool. I’ll take it out.
Alternatively, you could tell us what you had in mind (I wasn’t able to guess in the seconds I pondered it).
Hmm, I thought it was in the Elephant, then the Baby Elephant, and on looking I was forming the union of Exercises 1.1 and 1.2 in the latter. Ex 1.1 is the usual reduction of cartesian closed + … to finite limits plus power objects, and Ex 1.2 takes the ’finite limts + cartesian closed + subobject classifier ’ definition and reduces limits to finite products plus pullbacks of global elements of .
Goldblatt in Exercise 4.7.3 has some vague assertion about ’pullbacks of appropriate pairs of arrows’ being enough to define a topos (together with finite products and power objects).
I guess in principle one could track down exactly which pullbacks are needed to get the usual theorems that get the longer definitions off the ground, but, as I said, it was just a curiosity. My point in the notes is that power objects get you a lot and so the continuum function is important to understand, but in the development I do need the longer definition, even using Heyting pretoposes with subobject classifiers.
Has that footnote been removed already? The current footnote 6 (still on page 3) doesn’t seem to justify the comments above.
Yes, I removed it.
Yes, it seems it’s been removed: the current 6 is the old 7. Roughly it was referring to centipede-like conditions on which types of finite limits you can assume in the power-object definition of topos and still get a topos.
Another typo: ‘combinarics’, page 5.
@Toby
I vaguely recall seeing someone claim that not all finite limits are needed, together with power objects, to get a topos. I was repeating this claim in a vague way, but now that I’m pressed I can’t find where I think I originally read it. It’s also not terribly illumination for the purposes of the notes.
Another typo
Thanks!
And from the bottom of that page:
complete Boolean algeb[r]a
Thanks again. I really just wanted to get this off my chest in some form, and I hope the flow is coherent to the point that people are only nitpicking typos! (not to mention the loose end Theorem 3…)
I haven't gotten to Theorem 3, but I can follow it so far, and/but I don't know much about forcing.
On page 6, you hyphenate ‘Mo-erdijk’. You can put \hyphenation{moer-dijk} near the beginning of the document to fix this and other potential occurrences.
Ah, cool. That was irritating.
For some reason I think I never made the connection before between the stuff forcing people do with “generic ultrafilters” and a topos-theoretic filterquotient. Is the former really just a special case of the latter? Isn’t there also some weird business about having to do the forcing inside a countable submodel so that a generic ultrafilter exists?
Yes, in a countable model one can appeal to the Rasiowa-Sikorski lemma so that the generic exists. But filterquotients work for more general setups. As for the existence of the appropriate filter, I once knew how it worked, but I can’t recall off the top of my head.
p. 6, “eq[u]ipped”
1 to 17 of 17