Zulip Chat Archive

Stream: general

Topic: unifying `order_dual` and `opposite`


Scott Morrison (Apr 13 2019 at 09:32):

I would really like to unify order_dual in order/basic.lean with opposite in category_theory/opposites.lean.

Scott Morrison (Apr 13 2019 at 09:34):

They are talking about exactly the same thing, and to do presheafs and sheafs nicely I think we'll want to reflect a lot of the order structure on open sets up in category theoretic language. On the category theory side we'll be talking about (opens X)\op, and it's very sad at the moment there isn't just a complete_lattice immediately available, precisely because order_dual and opposite are not identical.

Scott Morrison (Apr 13 2019 at 09:35):

@Mario Carneiro, @Reid Barton, @Johannes Hölzl, any ideas about how to proceed?

Mario Carneiro (Apr 13 2019 at 09:36):

That sounds difficult... You would have to have preorder be the same thing as category

Scott Morrison (Apr 13 2019 at 09:36):

Why is that?

Scott Morrison (Apr 13 2019 at 09:37):

I was just thinking to move the definition def opposite (C : Sort u₁) : Sort u₁ := C (but nothing else) way down the import tree, and then search and replace order_dual for opposite.

Mario Carneiro (Apr 13 2019 at 09:37):

You could equip opposite with a preorder separate from its category, although you then have a diamond

Scott Morrison (Apr 13 2019 at 09:37):

oh, I see, a diamond

Scott Morrison (Apr 13 2019 at 09:38):

there would be two ways to get category (opens X)\op

Scott Morrison (Apr 13 2019 at 09:38):

either make the opposite preorder, then build a category from that

Scott Morrison (Apr 13 2019 at 09:38):

or make the category from the preorder, and take the opposite category

Scott Morrison (Apr 13 2019 at 09:38):

... tedious

Mario Carneiro (Apr 13 2019 at 09:38):

if you are lucky it might be defeq

Kevin Buzzard (Apr 13 2019 at 11:47):

Rather bizarrely I was experimenting with this stuff on the way home from AITP yesterday -- I decided that I could try to prove that the categories built in these two ways were equivalent -- it certainly didn't occur to me to try and make them defeq :-)


Last updated: Dec 20 2023 at 11:08 UTC