{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/mathlib/issues/473","repository_url":"https://api.github.com/repos/leanprover/mathlib","labels_url":"https://api.github.com/repos/leanprover/mathlib/issues/473/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/mathlib/issues/473/comments","events_url":"https://api.github.com/repos/leanprover/mathlib/issues/473/events","html_url":"https://github.com/leanprover/mathlib/pull/473","id":380461983,"node_id":"MDExOlB1bGxSZXF1ZXN0MjMwNjU0NzY1","number":473,"title":"feat(category_theory/limit): limits and colimits","user":{"login":"semorrison","id":477956,"node_id":"MDQ6VXNlcjQ3Nzk1Ng==","avatar_url":"https://avatars1.githubusercontent.com/u/477956?v=4","gravatar_id":"","url":"https://api.github.com/users/semorrison","html_url":"https://github.com/semorrison","followers_url":"https://api.github.com/users/semorrison/followers","following_url":"https://api.github.com/users/semorrison/following{/other_user}","gists_url":"https://api.github.com/users/semorrison/gists{/gist_id}","starred_url":"https://api.github.com/users/semorrison/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/semorrison/subscriptions","organizations_url":"https://api.github.com/users/semorrison/orgs","repos_url":"https://api.github.com/users/semorrison/repos","events_url":"https://api.github.com/users/semorrison/events{/privacy}","received_events_url":"https://api.github.com/users/semorrison/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2018-11-13T22:59:11Z","updated_at":"2018-11-13T23:01:37Z","closed_at":null,"author_association":"CONTRIBUTOR","pull_request":{"url":"https://api.github.com/repos/leanprover/mathlib/pulls/473","html_url":"https://github.com/leanprover/mathlib/pull/473","diff_url":"https://github.com/leanprover/mathlib/pull/473.diff","patch_url":"https://github.com/leanprover/mathlib/pull/473.patch"},"body":"Limits, products, equalizers, pullbacks, binary_products, terminal objects, and all the dual notions, too.\r\n\r\nThe basic design centres around:\r\n\r\n```\r\n/--\r\nA `c : cone F` is:\r\n* an object `c.X` and\r\n* a natural transformation `c.π : c.X ⟹ F` from the constant `c.X` functor to `F`.\r\n-/\r\nstructure cone (F : J ⥤ C) :=\r\n(X : C)\r\n(π : (const J C).obj X ⟹ F)\r\n```\r\n\r\n```\r\nstructure is_limit (t : cone F) :=\r\n(lift : ∀ (s : cone F), s.X ⟶ t.X)\r\n(fac'  : ∀ (s : cone F) (j : J), (lift s ≫ t.π.app j) = s.π.app j . obviously)\r\n(uniq' : ∀ (s : cone F) (m : s.X ⟶ t.X) (w : ∀ j : J, (m ≫ t.π.app j) = s.π.app j), \r\n  m = lift s . obviously)\r\n```\r\n\r\nand a typeclass bundling these together:\r\n\r\n```\r\nclass has_limit {J : Type v} [small_category J] (F : J ⥤ C) :=\r\n(cone : cone F)\r\n(is_limit : is_limit cone)\r\n```\r\n\r\nTheorems/constructions included so far:\r\n* `Type u` has all limits and colimits.\r\n* products, equalizers, pullbacks from limits\r\n* limits from products and equalizers\r\n* binary_products and terminal objects from products\r\n* if `has_limits_of_shape J C`, then `has_limits_of_shape J (K \\func C)`, and the evaluation function at `k` preserves limits\r\n* `F.cones` is the category `C^op \\func Type`, giving the collection of cones with a given cone point. We show `has_limit F` iff `representable F.cones`"},"comment":{"url":"https://api.github.com/repos/leanprover/mathlib/issues/comments/438471533","html_url":"https://github.com/leanprover/mathlib/pull/473#issuecomment-438471533","issue_url":"https://api.github.com/repos/leanprover/mathlib/issues/473","id":438471533,"node_id":"MDEyOklzc3VlQ29tbWVudDQzODQ3MTUzMw==","user":{"login":"semorrison","id":477956,"node_id":"MDQ6VXNlcjQ3Nzk1Ng==","avatar_url":"https://avatars1.githubusercontent.com/u/477956?v=4","gravatar_id":"","url":"https://api.github.com/users/semorrison","html_url":"https://github.com/semorrison","followers_url":"https://api.github.com/users/semorrison/followers","following_url":"https://api.github.com/users/semorrison/following{/other_user}","gists_url":"https://api.github.com/users/semorrison/gists{/gist_id}","starred_url":"https://api.github.com/users/semorrison/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/semorrison/subscriptions","organizations_url":"https://api.github.com/users/semorrison/orgs","repos_url":"https://api.github.com/users/semorrison/repos","events_url":"https://api.github.com/users/semorrison/events{/privacy}","received_events_url":"https://api.github.com/users/semorrison/received_events","type":"User","site_admin":false},"created_at":"2018-11-13T23:01:37Z","updated_at":"2018-11-13T23:01:37Z","author_association":"CONTRIBUTOR","body":"The outstanding issues raised in previous reviews were:\r\n\r\n* Is it okay to leave some comments in, suggesting additional theorems that could be added soon?\r\n* The construction of `has_equalizers CommRing` is really bad. It should either be:\r\n  * Cleaned up, with parts moved out of the `category_theory/` folder.\r\n  * Or removed for now.\r\n\r\n(The reason it's so bad is we don't have `simp` lemmas for `is_ring_hom`, it seems, not do we have a version of `ring` for playing with ring homomorphisms!)"}}
{"actor":{"display_login":"semorrison"}}