Timeline for Topos extensions
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 18, 2020 at 19:54 | comment | added | Simon Henry | You mean forcing corresponding to general site ? I guess Mike's paper allow to do this by simply applying the Well-founded graph construction to a sheaf topos. Though to get model of ZFC you need a sheaf topos satisfying choice, so you can't get much more general than double negation on a poset: Moerdijk have shown that the only Grothendieck topos satisyfing internal choice are boolean étendu. I'm not quite sure what you get when you apply the construction to a general boolean étendu though, my first guest is that the groupoid part gets ignored, but that's only a guess. | |
| May 18, 2020 at 19:36 | comment | added | Ingo Blechschmidt | Simon, very good answer. I'm wondering, do you have an analogue for the end extensions in set theory? | |
| May 17, 2020 at 17:33 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 330 characters in body
|
| May 17, 2020 at 15:51 | comment | added | Andreas Blass | It may be worth mentioning that the standard set-theoretic forcing constructions correspond to the special case of sheaves where the site is a partially ordered set (viewed as a category) with the double-negation topology. | |
| May 17, 2020 at 15:09 | comment | added | Mohammad Golshani | Thanks for the nice answer. | |
| May 17, 2020 at 14:54 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 2 characters in body
|
| May 17, 2020 at 14:49 | history | answered | Simon Henry | CC BY-SA 4.0 |