Timeline for Constructing ordered fields with lattice structure from ordered fields without lattice structure, and vice versa, in constructive mathematics
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 5, 2022 at 22:08 | comment | added | François G. Dorais | I agree with Andrej, but I also don't understand the first part. In $K(t)$ we know that $1 < 2$ and therefore we should also have $1 < t \lor t < 2$, no? | |
| Jul 5, 2022 at 21:32 | comment | added | Andrej Bauer | Could you be a bit more precise about the reverse direction, or provide a reference? What does it mean to "generate an ordered field"? How is the order playing a role in the generation? | |
| Jul 5, 2022 at 20:20 | comment | added | Geoffrey Irving | The first construction certainly works for Heyting fields, as by assumption $t$ is transcendental. Thus, any nonconstant rational function is invertible, and if $K$ is Heyting then any nonzero is invertible. The second construction should also work for Heyting fields, but it's not quite as obvious. | |
| Jul 5, 2022 at 20:11 | vote | accept | Madeleine Birchfield | ||
| Jul 6, 2022 at 1:09 | |||||
| Jul 5, 2022 at 20:10 | comment | added | Madeleine Birchfield | Minor question, which I probably should have made it clear in the questions above, and in my original reference request, but are the constructive ordered fields here Heyting fields, with respect to the canonical tight apartness relation defined by $a \# b := a \lt b \vee b \lt a$? Other definition of fields do exist which are not Heyting, such as the residue fields from Peter Johnstone's Rings, Fields, and Spectra. | |
| Jul 5, 2022 at 19:48 | history | answered | Geoffrey Irving | CC BY-SA 4.0 |