Timeline for Equivalence between geometric theories and frames internal to the free topos
Current License: CC BY-SA 4.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 9, 2022 at 16:18 | comment | added | user1022117 | @SimonHenry: Thanks for your answer, that helps! | |
| Feb 9, 2022 at 14:18 | comment | added | Simon Henry | @user1022117 : I didn't "learn at the right place" either. I learned topos theory on my own (from books) when I was a PhD student. If you want to learn start from one of the classical textbooks like MacLane and Moerdijk Sheaves in geometry and logic, or volume 3 of Borceux's handbook of categorical algebra. I also like McLarty's Elementary categories, Elementary topos if you want to learn directly through the lens of internal logic. The Elephant is a very valuable resource, but it was never meant to be a textbook : It is an encyclopedia. | |
| Feb 9, 2022 at 14:09 | comment | added | Simon Henry | @user1022117 The part of th D3.2.5 you want is the equivalence between $T$ classifies a one sorted geometric theory (with generic model B) and the morphism $ T \to Set[O]$ corresponding to $B$ is localic. You then have to combined this with the fact that localic geometric morphism $ E \to T$ corresponds to internal frame in $T$. (Ivan gave a reference for this. I couldn't find a reference for this in the Elephant, except section C1.6 which deals with the case where $T$ is localic... ) | |
| Feb 9, 2022 at 13:10 | comment | added | Ivan Di Liberti | I did not study at the right place for topos theory. It is true that it takes an enormous amount of time, though. | |
| Feb 9, 2022 at 13:06 | comment | added | user1022117 | It's sad that one can learn topos theory only if one studies at the right place where people teach it. Many things seem to folklore and scattered through many papers. Very inaccessible to outsiders. | |
| Feb 9, 2022 at 12:59 | comment | added | Ivan Di Liberti | What is you background in topos theory?! Because this is far from being a question at the level of "a topos is a lex reflection of a presheaf category". | |
| Feb 9, 2022 at 12:53 | comment | added | user1022117 | @IvanDiLiberti I don't understand your answer. | |
| Feb 9, 2022 at 12:52 | comment | added | Ivan Di Liberti | @user1022117 Read my answer. | |
| Feb 9, 2022 at 12:46 | comment | added | user1022117 | D3.2.5 states that on object B of a Grothendieck topos E is "pre-bound" (whatever that is) iff there is a single-sorted geometric theory T and an equivalence between E and Set[T] "which identifies B with the underlying object of the generic T-model". Firstly, I don't understand how this is related to the question I am asking. Secondly, what does "identifies B with the underlying ..." mean? | |
| Feb 9, 2022 at 12:42 | comment | added | user1022117 | "A Frame in this topos hence corresponds to a purely propositional geometric theory on top of this theory with one sort and no axiom, so you end-up with exactly a geometric theory with a single sort and as many propositions and geometric axioms as you want" - Can you explain that? I don't understand the "hence". What you are claiming is exactly the theorem I ask about. | |
| Feb 9, 2022 at 12:39 | comment | added | user1022117 | Why is it appropriate to call the object classifier the "free topos"? (I know that usually that refers to Lambek's initial elementary topos.) | |
| Feb 8, 2022 at 22:50 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 87 characters in body
|
| Feb 8, 2022 at 22:37 | history | edited | Simon Henry | CC BY-SA 4.0 |
deleted 480 characters in body
|
| Feb 8, 2022 at 20:51 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 17 characters in body
|
| Feb 8, 2022 at 20:34 | history | answered | Simon Henry | CC BY-SA 4.0 |