{"action":"created","issue":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/254","labels_url":"https://api.github.com/repos/UniMath/UniMath/issues/254/labels{/name}","comments_url":"https://api.github.com/repos/UniMath/UniMath/issues/254/comments","events_url":"https://api.github.com/repos/UniMath/UniMath/issues/254/events","html_url":"https://github.com/UniMath/UniMath/issues/254","id":120778826,"number":254,"title":"definition of field","user":{"login":"DanGrayson","id":700228,"avatar_url":"https://avatars.githubusercontent.com/u/700228?v=3","gravatar_id":"","url":"https://api.github.com/users/DanGrayson","html_url":"https://github.com/DanGrayson","followers_url":"https://api.github.com/users/DanGrayson/followers","following_url":"https://api.github.com/users/DanGrayson/following{/other_user}","gists_url":"https://api.github.com/users/DanGrayson/gists{/gist_id}","starred_url":"https://api.github.com/users/DanGrayson/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/DanGrayson/subscriptions","organizations_url":"https://api.github.com/users/DanGrayson/orgs","repos_url":"https://api.github.com/users/DanGrayson/repos","events_url":"https://api.github.com/users/DanGrayson/events{/privacy}","received_events_url":"https://api.github.com/users/DanGrayson/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":11,"created_at":"2015-12-07T13:56:02Z","updated_at":"2015-12-11T14:41:47Z","closed_at":null,"body":"Here is our definition of \"field\".\r\n\r\n```\r\nDefinition invpair (X:monoid) (x:X) := Σ x':X, ( x' * x = 1 ) × ( x * x' = 1 ).\r\nDefinition multinvpair ( X : rig ) ( x : X ) := invpair ( rigmultmonoid X ) x .\r\nDefinition isafield (X:commrng) := isnonzerorng X  ×  ∀ x:X, multinvpair X x ⨿ (x = 0).\r\nDefinition fld := Σ X, isafield X.\r\n```\r\n\r\nAre there any examples worthy of being considered as fields that satisfy only the weaker condition \r\nthat ` x != 0 -> multinvpair X x ` ?\r\n\r\nThe construction of the field of fractions for an integral domain, as a result of this, requires the\r\nadditional hypothesis that the ring has decidable equality.  I can imagine that being counterintuitive\r\nwhen we start formalizing commutative algebra, and we want to associate a field to each\r\nprime ideal of a commutative ring.\r\n\r\nI'm tempted to weaken the definition to allow more natural developments, even if there are\r\nno interesting examples.\r\n"},"comment":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/comments/163951636","html_url":"https://github.com/UniMath/UniMath/issues/254#issuecomment-163951636","issue_url":"https://api.github.com/repos/UniMath/UniMath/issues/254","id":163951636,"user":{"login":"vladimirias","id":424011,"avatar_url":"https://avatars.githubusercontent.com/u/424011?v=3","gravatar_id":"","url":"https://api.github.com/users/vladimirias","html_url":"https://github.com/vladimirias","followers_url":"https://api.github.com/users/vladimirias/followers","following_url":"https://api.github.com/users/vladimirias/following{/other_user}","gists_url":"https://api.github.com/users/vladimirias/gists{/gist_id}","starred_url":"https://api.github.com/users/vladimirias/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/vladimirias/subscriptions","organizations_url":"https://api.github.com/users/vladimirias/orgs","repos_url":"https://api.github.com/users/vladimirias/repos","events_url":"https://api.github.com/users/vladimirias/events{/privacy}","received_events_url":"https://api.github.com/users/vladimirias/received_events","type":"User","site_admin":false},"created_at":"2015-12-11T14:41:47Z","updated_at":"2015-12-11T14:41:47Z","body":"I still think that “a field” and “an apartness field” are the best names with fld and apfld as UniMath abbreviations.\n\nThis thinking comes from a feeling that I had even back 20 years ago when I knew nothing about constructive mathematics - that fields such as, for example, the field of functions of a henselization of Z in p are somehow more algebraic objects than completions such as Z_p. In the constructive setting this feeling gets a precise expression - the field of functions of a henzelization, which has decidable equality, is a field while Z_p is an object of a different class that is located slightly away from algebra in the direction of where the study of ordered algebraic structures lies.\n\nVladimir.\n\n> On Dec 11, 2015, at 8:07 AM, Daniel R. Grayson <notifications@github.com> wrote:\n> \n> Another point in favor of modifying the definition of \"field\" is so it will cover (complete) local fields, such as the p-adic numbers. Their Galois theory is important, too.\n> \n> —\n> Reply to this email directly or view it on GitHub <https://github.com/UniMath/UniMath/issues/254#issuecomment-163932823>.\n> \n\n"}}