Zulip Chat Archive

Stream: Is there code for X?

Topic: category of POSet

Simon Hudon (Aug 17 2020 at 15:43):

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

Kenny Lau (Aug 17 2020 at 15:45):

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

Simon Hudon (Aug 17 2020 at 15:48):

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

Reid Barton (Aug 17 2020 at 15:49):

@Johan Commelin :this:

Reid Barton (Aug 17 2020 at 15:50):

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

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

Johan Commelin (Aug 17 2020 at 16:43):

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

Simon Hudon (Aug 17 2020 at 16:44):

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

Johan Commelin (Aug 17 2020 at 16:49):

#3841

Johan Commelin (Aug 17 2020 at 16:49):

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

Simon Hudon (Aug 17 2020 at 16:51):

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

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: Dec 20 2023 at 11:08 UTC