Timeline for Sheaf-theoretic approach to forcing
Current License: CC BY-SA 4.0
33 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 12, 2021 at 23:33 | vote | accept | Peter Scholze | ||
| Mar 5, 2021 at 8:57 | answer | added | Peter Scholze | timeline score: 18 | |
| Mar 4, 2021 at 23:42 | history | edited | Wojowu | CC BY-SA 4.0 |
edited title
|
| Mar 4, 2021 at 20:03 | history | edited | Asaf Karagila♦ | CC BY-SA 4.0 |
En-dash II, the en-dashening.
|
| Mar 4, 2021 at 18:44 | history | became hot network question | |||
| Mar 4, 2021 at 17:45 | answer | added | Mike Shulman | timeline score: 28 | |
| Mar 4, 2021 at 17:07 | comment | added | Simon Henry | Regarding question 1, I don't want to give a definitive answer without thinking more about it, because there are many details involved. but it should work. This construction is mentioned in example A.2.1.13 of Sketches of an elephant and in more details in Johnstone's older book "Topos theory" (section 9.4). It is not going to fully answer your question as these references don't specifically discuss ETCS nor replacement, but that should already considerably reduce what is left to prove. | |
| Mar 4, 2021 at 16:59 | history | edited | Mike Shulman | CC BY-SA 4.0 |
These aren't "sheaves on S" with respect to any topology.
|
| Mar 4, 2021 at 15:36 | answer | added | Zhen Lin | timeline score: 22 | |
| Mar 4, 2021 at 15:31 | comment | added | Tim Campion | I also occurs to me that the techniques used in topos theory to get a localic cover of a sheaf topos over a general site (cf. C.5.2 in the Elephant or A.4.3.1 in SAG) sound a lot like "giving names" to the objects / morphisms of the site. I wonder if this has anything to with the "names" which appear in forcing. | |
| Mar 4, 2021 at 15:26 | history | edited | Peter Scholze | CC BY-SA 4.0 |
added 66 characters in body
|
| Mar 4, 2021 at 15:25 | comment | added | Asaf Karagila♦ | Objection, your honour, the comment by @Mike is written in an internal language to an internal sheaf topos! :-) | |
| Mar 4, 2021 at 15:24 | comment | added | Asaf Karagila♦ | Thanks, @Peter. When I was working on iterations of symmetric extensions, I realised that the "generic semi-direct product" has a strong categorical flavour. One of the other students would explain sheaves to me about twice a month. My advisor even said at some point that maybe that approach would clarify the construction, but I'm pretty sure that he was pulling my legs. I still don't fully grasp what sheaves are... :-) | |
| Mar 4, 2021 at 15:23 | comment | added | Mike Shulman | @AsafKaragila And yet, set theorists seem to object when I point out that you can also do everything internally in the internal language of a sheaf topos. | |
| Mar 4, 2021 at 15:23 | comment | added | Peter Scholze | Sorry, Mike! I'll add the double negation in, but I didn't know the tex command... | |
| Mar 4, 2021 at 15:22 | comment | added | Mike Shulman | I really don't think you should call this topos $\mathrm{Sh}(S)$. That seems to be asking for trouble, since when $S$ is a topological space, "$\mathrm{Sh}(S)$" has a standard meaning, and this isn't it. | |
| Mar 4, 2021 at 15:22 | comment | added | Asaf Karagila♦ | @Tim: Yes, that's exactly right. Part of what I was going for in my "long comment" is the fact we can do everything internally, so the model doesn't really play a significant role. Of course, we can do without that, given a model of ZFC, build a model of ZFC+CH or ZFC+MA, etc. The true strength of forcing is that it can be done internally, rather than externally. | |
| Mar 4, 2021 at 15:20 | comment | added | Peter Scholze | The above description seems perfectly definable to me, but I don't really know what definable means. @AsafKaragila: I think it's fair to consider $C=\mathrm{Sh}(S)$ as the "structural" version of the class of P-names. | |
| Mar 4, 2021 at 15:16 | comment | added | Tim Campion | One issue that set theorists often bring up about the sheaf-theoretic approach to forcing is the fact that for set theorists, it seems to be essential to have good control over definability properties of the forcing model in terms of the ground model (I think the main thing is that the forcing relation should be definable in the ground model?). I've gotten the impression that in the sheaf-theoretic approach, it's not obvious how to control these definability properties. My hunch is that this is not really an issue in the end, but I've never seen this point carefully addressed. | |
| Mar 4, 2021 at 15:00 | comment | added | Asaf Karagila♦ | @Jacob: Just to see that I follow this, C is the class of P-names, right? | |
| Mar 4, 2021 at 14:36 | comment | added | Peter Scholze | The forcing poset defines a complete boolean algebra, which by Stone duality corresponds to an extremally disconnected profinite set. The subsheaves of $\ast$ in $\mathrm{Sh}(S)$ are in bijection with open and closed subsets $U\subset S$, so for all I can tell the maximal filters (used in Exercise VI.6 of MacLane--Moerdijk) are exactly given by the points $s\in S$. But Jacob's comment makes me believe I'm still stuck down in my platonic universe and need to free my mind more... | |
| Mar 4, 2021 at 14:24 | comment | added | Jacob Lurie | If V is a model of set theory, then you can do the first part of this construction "in V" to produce some category C that V thinks is a Grothendieck topos. In some ambient universe, C is a Boolean pretopos having an underlying Stone space X. In your example, I think X is Spec(B), where B is the Boolean algebra of clopen subsets of your S? In particular S sits inside X as "the points of the spectrum that V knows about". The usual forcing construction is to take a "stalk" of C at some point of X which is "V-generic": that is, very far from belonging to S. | |
| Mar 4, 2021 at 14:15 | comment | added | Mike Shulman | Or is it that when you say "sheaves on $S$" you really mean "sheaves on some site whose objects happen to be related to $S$ in some way but are not actually a point-set topology on the set $S$"? | |
| Mar 4, 2021 at 14:14 | comment | added | Mike Shulman | I'll have more to say later, but for now, can you explain how to get your profinite set $S$ starting from a forcing poset? I'm a little confused because I think of the forcing poset as the Lindenbaum algebra of the geometric theory of the object we want to adjoin, which in general might have no models at all in the theory we start with, so that it would correspond to a locale without any points; but a topological space always has enough points, so where do they come from? | |
| Mar 4, 2021 at 12:32 | comment | added | David Roberts♦ | The countability of the base model is to have en.wikipedia.org/wiki/Rasiowa%E2%80%93Sikorski_lemma available, from what I understand, so that one can get the generic filter in the forcing poset. This seems to me to be linked to getting the filter in the subobjects of the terminal object of the sheaf topos, to actually perform the filterquotient construction, so that the subobject classifier in the new topos is $1+1$. (And, it's exercise VI.6.iii) in Mac Lane and Moerdijk, not 7, that you want: note the filter!) | |
| Mar 4, 2021 at 11:36 | history | edited | Asaf Karagila♦ | CC BY-SA 4.0 |
Em-dashes and en-dashes
|
| Mar 4, 2021 at 11:34 | history | edited | Peter Scholze | CC BY-SA 4.0 |
edited body
|
| Mar 4, 2021 at 11:21 | history | edited | Peter Scholze | CC BY-SA 4.0 |
added 94 characters in body
|
| Mar 4, 2021 at 11:21 | answer | added | Asaf Karagila♦ | timeline score: 16 | |
| Mar 4, 2021 at 11:18 | history | edited | Peter Scholze | CC BY-SA 4.0 |
added 94 characters in body
|
| Mar 4, 2021 at 11:06 | comment | added | Alec Rhea | @AsafKaragila Shivs are more prone to applications than theory. | |
| Mar 4, 2021 at 11:01 | comment | added | Asaf Karagila♦ | Much safer than the shiv theoretic approach to forcing, I say. | |
| Mar 4, 2021 at 10:43 | history | asked | Peter Scholze | CC BY-SA 4.0 |