{"action":"opened","issue":{"url":"https://api.github.com/repos/purescript/purescript-prelude/issues/144","repository_url":"https://api.github.com/repos/purescript/purescript-prelude","labels_url":"https://api.github.com/repos/purescript/purescript-prelude/issues/144/labels{/name}","comments_url":"https://api.github.com/repos/purescript/purescript-prelude/issues/144/comments","events_url":"https://api.github.com/repos/purescript/purescript-prelude/issues/144/events","html_url":"https://github.com/purescript/purescript-prelude/issues/144","id":268621312,"number":144,"title":"Need more careful definition of a `DivisionRing` from a `Ring`","user":{"login":"midfield","id":545720,"avatar_url":"https://avatars2.githubusercontent.com/u/545720?v=4","gravatar_id":"","url":"https://api.github.com/users/midfield","html_url":"https://github.com/midfield","followers_url":"https://api.github.com/users/midfield/followers","following_url":"https://api.github.com/users/midfield/following{/other_user}","gists_url":"https://api.github.com/users/midfield/gists{/gist_id}","starred_url":"https://api.github.com/users/midfield/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/midfield/subscriptions","organizations_url":"https://api.github.com/users/midfield/orgs","repos_url":"https://api.github.com/users/midfield/repos","events_url":"https://api.github.com/users/midfield/events{/privacy}","received_events_url":"https://api.github.com/users/midfield/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2017-10-26T03:50:50Z","updated_at":"2017-10-26T03:50:50Z","closed_at":null,"author_association":"NONE","body":"Adapted from a reddit conversation with paf31:\r\n\r\nThe way you define a `DivisionRing` from a `Ring` is\r\n\r\n``` data Ratio a = Ratio a a\r\ninstance (Ring a) => DivisionRing (Ratio a) ```\r\n\r\nThis is a problem because you're taking all pairs of elements from the original ring, e.g. you're allowing everything in the denominator.\r\n\r\nThe usual definition of localization of rings `R` with respect to a multiplicative system `S` (= things allowed in the denominator; needs to include the multiplicative unit and be closed under multiplication, so we can do addition) is: form a ring of pairs (ratios) with the equivalence relation `a1/b1 = a2/b2` if there exists a `t` in `S` so that `t(a1b2 - a2b1) = 0`; addition and multiplication follow the usual rules for fractions; the additive unit is `0/1` and the multiplicative unit is `1/1`. In particular `a/b = ax/b*x` for any `x` in `S`, so if `0` is in `S`, then everything is zero and you have the zero ring. More generally, if you have zero divisors in `S`, then the usual map `R -> R[S^-1]` is not injective.\r\n\r\nEven if you don't want to use the usual equivalence relation, some of this weirdness is forced, just from the usual rules for adding and multiplying fractions. For example\r\n\r\n```0/1*a/0 = 0/0```\r\n\r\nwhich implies that `0/0` is the zero element (since `0*x = 0` in any ring.) So you need at least some kind of equivalence relation. But then\r\n\r\n```a/b = 0/0 + a/b = (0b + a0)/(0*b) = 0/0```\r\n\r\nso every element is zero.\r\n\r\nSorry this is kind of rambling, I'm also not remembering my algebra crisply."}}
{"actor":{"display_login":"midfield"}}