Timeline for Equivalence between geometric theories and frames internal to the free topos
Current License: CC BY-SA 4.0
34 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 8, 2022 at 12:02 | history | edited | Ivan Di Liberti | CC BY-SA 4.0 |
added 1 character in body
|
| Feb 9, 2022 at 20:07 | comment | added | David Roberts♦ | @user1022117 I think one needs to be conscious that there is something else called "the free topos", namely the initial object in the (2-)category of elementary toposes and logical morphisms. Edit: ah, I see from another comment you know this already! As you were... | |
| Feb 9, 2022 at 16:56 | comment | added | Ivan Di Liberti | @user1022117 I have a thick skin. If we happen to meet at a conference come and say hi to me, we'll laugh about this story in front of a beer. | |
| Feb 9, 2022 at 16:21 | comment | added | user1022117 | @IvanDiLiberti I just want to say thanks again for all your help and sorry that I was a bit overwhelmed at first. I will come back to your answer again and again as I keep learning more topos theory! | |
| Feb 9, 2022 at 13:46 | comment | added | user1022117 | @IvanDiLiberti Thanks! | |
| Feb 9, 2022 at 13:42 | comment | added | Ivan Di Liberti | The forgetful functor Topoi $\to \text{Cat}^\text{op}$ is representable and has a left adjoint. Set$[\mathbb{O}]$ is the free object on $1$. | |
| Feb 9, 2022 at 13:40 | comment | added | user1022117 | Thanks! But in which sense is the object classifier "free"? That question is pretty connected to my main question: the question uses the word "free topos", and an essential step towards the answer is to realize that this doesn't refer to the initial topos. | |
| Feb 9, 2022 at 13:37 | comment | added | Ivan Di Liberti | @user1022117 The original reference would probably be "The Symmetric topos" by Bunge and Carboni. Good luck with that. | |
| Feb 9, 2022 at 13:36 | comment | added | Ivan Di Liberti | @user1022117 I do not think at all that you are stupid, you are asking good questions, but you just lamented my storm of references, and this question in particular is not that connected to the main question you asked. I was trying to save you time! | |
| Feb 9, 2022 at 13:29 | comment | added | Ivan Di Liberti | About the free topos, the best reference is Anel-Joyal "Topo-logie". It builts on an analogy with posets. I would not say that it is so telling for you. Concerning internal frames in a presheaf category, as I wrote, the correct intuition is that of hyperdoctrines. Fin are the variables, and P(n) is the frame of formulas in those variables. | |
| Feb 9, 2022 at 13:21 | comment | added | user1022117 | Is there any intuitive reason why geometric theories are frames internal to the free topos? How does one think about theories internal to a topos? Why is the object classifier called the free topos? | |
| Feb 9, 2022 at 13:16 | history | edited | Ivan Di Liberti | CC BY-SA 4.0 |
deleted 12 characters in body
|
| Feb 9, 2022 at 13:11 | vote | accept | user1022117 | ||
| Feb 9, 2022 at 13:08 | comment | added | user1022117 | I won't downvote. Probably your answer is very helpful in 10 years when I have the right background to be able to read it. :-) | |
| Feb 9, 2022 at 13:04 | comment | added | Ivan Di Liberti | I disagree, but feel free to downvote my answer. | |
| Feb 9, 2022 at 13:02 | comment | added | user1022117 | Firstly, I didn't ask about Hahn-Banach. Secondly, prebounds don't occur in the statement I asked about. Thirdly, you don't need to know about Banach spaces to state and prove the Hahn-Banach theorem. I really don't get your analogy. | |
| Feb 9, 2022 at 13:01 | comment | added | Ivan Di Liberti | Similarly, you are asking for a proof of Morely categoricity theorem in Model theory, but you want it to be completely elementary and not mentioning saturated models and Lachlan's theorem? I mean, it's not in-accessible, but "One does not simply walk into Mordor". | |
| Feb 9, 2022 at 12:58 | comment | added | Ivan Di Liberti | @user1022117 The gist of what I said, is the "Construction" in my answer. A lot of the answer also depends on what you intend by "geometric theory", that is if you a geometric theory is the data of its presentation or if it is essentially its classifying topos. In case your notion of geometric theory is a bunch of symbols and formulas, one can take a very neat shortcut. Concerning the accessibility of TT, you must understand that you asked for "Can you prove Han Banach theorem" and you do not even accept that I need to define what is a Banach space (prebounds are a basic notion)? | |
| Feb 9, 2022 at 12:52 | comment | added | user1022117 | So basically one needs to read papers of Freyd, Caramello, and Johnstone in addition to 1000 pages of the Elephant to understand the proof? Topos theory is really accessible. :-) | |
| Feb 9, 2022 at 12:19 | history | edited | Ivan Di Liberti | CC BY-SA 4.0 |
added 284 characters in body
|
| Feb 9, 2022 at 12:07 | history | edited | Ivan Di Liberti | CC BY-SA 4.0 |
added 131 characters in body
|
| Feb 9, 2022 at 11:53 | history | edited | Ivan Di Liberti | CC BY-SA 4.0 |
added 26 characters in body
|
| Feb 9, 2022 at 11:51 | comment | added | Ivan Di Liberti | @DavidRoberts I was thinking about Grothendieck topoi the whole time. | |
| Feb 9, 2022 at 11:51 | comment | added | Ivan Di Liberti | @ZhenLin, what I have in mind are Lemmas C.1.6.9 and Cor. C.1.6.10 in Sketches of an Elephant. | |
| Feb 9, 2022 at 11:42 | comment | added | David Roberts♦ | By "topos", do you mean elementary or Grothendieck topos? | |
| Feb 9, 2022 at 11:40 | comment | added | Zhen Lin | Why do internal frames give rise to functors into the category of Heyting algebras? (Specifically, why do the reindexing maps preserve the implication?) | |
| Feb 9, 2022 at 11:35 | history | edited | Ivan Di Liberti | CC BY-SA 4.0 |
added 568 characters in body
|
| Feb 9, 2022 at 11:29 | history | edited | Ivan Di Liberti | CC BY-SA 4.0 |
added 568 characters in body
|
| Feb 9, 2022 at 11:17 | history | edited | Ivan Di Liberti | CC BY-SA 4.0 |
added 16 characters in body
|
| Feb 9, 2022 at 11:03 | history | edited | Ivan Di Liberti | CC BY-SA 4.0 |
added 135 characters in body
|
| Feb 9, 2022 at 10:57 | history | edited | Ivan Di Liberti | CC BY-SA 4.0 |
added 135 characters in body
|
| Feb 9, 2022 at 10:49 | history | edited | Ivan Di Liberti | CC BY-SA 4.0 |
added 4 characters in body
|
| Feb 9, 2022 at 10:42 | history | edited | Ivan Di Liberti | CC BY-SA 4.0 |
added 503 characters in body
|
| Feb 9, 2022 at 10:36 | history | answered | Ivan Di Liberti | CC BY-SA 4.0 |