{"action":"created","issue":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/796","repository_url":"https://api.github.com/repos/UniMath/UniMath","labels_url":"https://api.github.com/repos/UniMath/UniMath/issues/796/labels{/name}","comments_url":"https://api.github.com/repos/UniMath/UniMath/issues/796/comments","events_url":"https://api.github.com/repos/UniMath/UniMath/issues/796/events","html_url":"https://github.com/UniMath/UniMath/pull/796","id":279182223,"number":796,"title":"Actions of monoids, groups, and rings","user":{"login":"siddharthist","id":4294323,"avatar_url":"https://avatars3.githubusercontent.com/u/4294323?v=4","gravatar_id":"","url":"https://api.github.com/users/siddharthist","html_url":"https://github.com/siddharthist","followers_url":"https://api.github.com/users/siddharthist/followers","following_url":"https://api.github.com/users/siddharthist/following{/other_user}","gists_url":"https://api.github.com/users/siddharthist/gists{/gist_id}","starred_url":"https://api.github.com/users/siddharthist/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/siddharthist/subscriptions","organizations_url":"https://api.github.com/users/siddharthist/orgs","repos_url":"https://api.github.com/users/siddharthist/repos","events_url":"https://api.github.com/users/siddharthist/events{/privacy}","received_events_url":"https://api.github.com/users/siddharthist/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":10,"created_at":"2017-12-04T22:59:27Z","updated_at":"2017-12-13T17:46:28Z","closed_at":null,"author_association":"COLLABORATOR","pull_request":{"url":"https://api.github.com/repos/UniMath/UniMath/pulls/796","html_url":"https://github.com/UniMath/UniMath/pull/796","diff_url":"https://github.com/UniMath/UniMath/pull/796.diff","patch_url":"https://github.com/UniMath/UniMath/pull/796.patch"},"body":"Summary:\r\n * I define `hasinv`, etc. as propositions expressing \"this element has an (left/right) inverse under this binary operation\". This is more granular than saying \"this operation is (left/right) invertible\". We might want to rephrase the latter definitions in terms of the former, but I wanted to get feedback before making those changes.\r\n * I define the submonoid of elements with inverses, and show that it is actually a group.\r\n * I define the endomorphism monoid, automorphism group, and endomorphism ring (in an additive category), and define monoid (group) actions and ring actions as homomorphisms into these.\r\n\r\nThis PR might need a little reorganization (including the first bullet point above). Let me know where things should go! "},"comment":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/comments/351468108","html_url":"https://github.com/UniMath/UniMath/pull/796#issuecomment-351468108","issue_url":"https://api.github.com/repos/UniMath/UniMath/issues/796","id":351468108,"user":{"login":"DanGrayson","id":700228,"avatar_url":"https://avatars1.githubusercontent.com/u/700228?v=4","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},"created_at":"2017-12-13T17:46:28Z","updated_at":"2017-12-13T17:46:28Z","author_association":"OWNER","body":"This is an important issue of style, for which we need a uniform solution, and it goes back to choices Vladimir made in 2010.  He loved even such identifiers as `coconustot`."}}
{"actor":{"display_login":"DanGrayson"}}