Zulip Chat Archive

Stream: Is there code for X?

Topic: category of POSet


view this post on Zulip Simon Hudon (Aug 17 2020 at 15:43):

Do we have a category of partial orders (or preorders) with monotone functions as morphisms?

view this post on Zulip Kenny Lau (Aug 17 2020 at 15:45):

@Simon Hudon mathlib:sset/src/order/category/PartialOrder.lean

view this post on Zulip Simon Hudon (Aug 17 2020 at 15:48):

Nice thanks! Is that a PR about to be merged?

view this post on Zulip Reid Barton (Aug 17 2020 at 15:49):

@Johan Commelin :this:

view this post on Zulip Reid Barton (Aug 17 2020 at 15:50):

It's not already a PR, if that's what you mean.

view this post on Zulip Simon Hudon (Aug 17 2020 at 15:52):

Too bad, I could use that in my PR. I'm bundling monotone functions and I find myself reinventing binary products again

view this post on Zulip Johan Commelin (Aug 17 2020 at 16:43):

@Simon Hudon I can PR those three files on categories of orders

view this post on Zulip Simon Hudon (Aug 17 2020 at 16:44):

That'd be great! Thank you! Do you intend to define the limits of those categories?

view this post on Zulip Johan Commelin (Aug 17 2020 at 16:49):

#3841

view this post on Zulip Johan Commelin (Aug 17 2020 at 16:49):

@Simon Hudon No, I didn't have any plans on defining limits

view this post on Zulip Simon Hudon (Aug 17 2020 at 16:51):

Ok, I'll take care of it. Thanks for the PR!

view this post on Zulip Aaron Anderson (Aug 17 2020 at 17:27):

FWIW, this this notion of bundled monotone map is pretty similar to the notions of rel_embedding and the order_embedding that I'm redefining. I see no reason not to PR it now, but I might try to generalize it soon to rel_hom for arbitrary relations, with order_hom as a special case.


Last updated: May 07 2021 at 21:10 UTC