Timeline for Can the real numbers be constructed as/from a Hom-object in a topos?
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 12 at 16:48 | comment | added | Steven Stadnicki | These make sense to me. Thank you! | |
| Nov 12 at 15:56 | comment | added | Simon Henry | In fact the Dedekind real are exactly the one sided Dedekind cut $x$ such that there is another one sided cut $y$ satisfying $x+y = 0$. | |
| Nov 12 at 14:31 | comment | added | Simon Henry | @StevenStadnicki you can define anything you want however you want, but you won't be able to prove any of the expected properties. For example defining $-x$ this way, you don't have $x - x =0$, unless your topos is boolean. While using two sidded cut you get an honest rings. The condition I put in my answer correspodns to the fact that if two real $x$ and $y$ are such that $x <y$, then there exists a real (even a rational) $z$ such that $x <z<y$. So you won't get that either with your definition. | |
| Nov 12 at 7:23 | comment | added | Peter LeFanu Lumsdaine | Absolutely, that issue is “straightforwardly handleable” — but the most straightforward way to handle it is exactly by adding the extra axiom for Dedekind cuts, as this answer suggests. | |
| Nov 12 at 6:56 | comment | added | Steven Stadnicki | I would think that negation could be defined as $f_{-r}(q) = \neg f_r(-q)$, and then subtraction by the formula above. And I'm not sure that my definition needs the fact that $V$ has no minimum; if there is a minimum element $q$ with $f_r(q)=\true$ then we just have $r=q$ (and this does mean there are two functions corresponding to every rational number, but that seems straightforwardly handleable). | |
| Nov 12 at 2:41 | history | edited | Simon Henry | CC BY-SA 4.0 |
deleted 59 characters in body
|
| Nov 12 at 2:30 | history | answered | Simon Henry | CC BY-SA 4.0 |