Mistake in definition of order on rationals

[pglutz]

Mistake in definition of order on rationals

[rzach]

This seems right to me; @timbutton ?

[timbutton]

@rzach yes, this needs fixing, and I appreciate @pglutz's suggestion as to how.
I am frantic with admin tasks for the next two weeks, so won't be able to fix it for a little while. @rzach, feel free to fix it if you like; otherwise, I'll get to it in mid-February.

[rzach]

Is the proposal to change the definition of ℚ to be equivalence classes of pairs [a,b] where a, b ∈ ℤ but b is positive? I wonder if an easier (ie, more local) fix would be to leave the definition of ℚ the same and just redefine ≤ on ℚ as

[a,b] ≤ [c,d] iff [c,d] - [a,b] ~ [e_ℤ,f_ℤ] for some e ∈ ℕ, 0 ≠ f ∈ ℕ

(that is, p ≤ q iff q-p is not negative).
I think nothing else has to be changed since the verification that ℚ is an ordered field is left as an exercise. I don't know if that exercise would be harder with this definition of ≤ (where only the verification of the order properties would change) or @pglutz 's (where all the field properties would change).

[pglutz]

@rzach I think you misunderstood the fix I suggested but your fix is probably better than what I had in mind anyway.

In case you're curious, the fix I had in mind was to leave the definition of Q the same but change the definition of the order to:

[a, b] \leq [c, d] iff for some [a', b'] ~ [a, b] and some [c', d'] ~ [c, d] we have b' > 0, d' > 0 and a'd' \leq c'b'.

This does not require changing the definition of Q but it is more of a mouthful and to show it defines an order requires justifying why every ~ equivalence class [a, b]_~ contains an element [a', b'] such that b' > 0.

Your fix is nice because it seems a bit cleaner and less ad-hoc.

[timbutton]

This seems great to me. Does the 0 need a "naturals" subscript? Can't recall and only have my phone!

…

On Thu, 27 Jan 2022, 02:10 Richard Zach, ***@***.***> wrote: Is the proposal to change the definition of ℚ to be equivalence classes of pairs [a,b] where a, b ∈ ℤ *but b is positive*? I wonder if an easier (ie, more local) fix would be to leave the definition of ℚ the same and just redefine ≤ on ℚ as [a,b] ≤ [c,d] iff [c,d] - [a,b] ~ [e_ℤ,f_ℤ] for some e ∈ ℕ, 0 ≠ f ∈ ℕ (that is, p ≤ q iff q-p is not negative). I think nothing else has to be changed since the verification that ℚ is an ordered field is left as an exercise. I don't know if that exercise would be harder with this definition of ≤ (where only the verification of the order properties would change) or @pglutz <https://github.com/pglutz> 's (where all the field properties would change). — Reply to this email directly, view it on GitHub <#296 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AM5CQB7TYXA7ZK6WH4ANRS3UYCSRPANCNFSM5MZQ4ZVA> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you were mentioned.Message ID: ***@***.***>