Zulip Chat Archive
Stream: general
Topic: Notation for order_dual
Yaël Dillies (Apr 29 2022 at 12:56):
It looks like it is time to give docs#order_dual some notation. Here are a few suggestions:
Yaël Dillies (Apr 29 2022 at 13:03):
/poll What should the notation for order_dual α be?
αᵒᵈ
αᵈᵘᵃˡ
α⤩
α﹥⇄﹤
Johan Commelin (Apr 29 2022 at 13:05):
Can we reuse ^{op} from category_theory?
Yaël Dillies (Apr 29 2022 at 13:07):
That would make sense because, considering orders as categories, the dual order corresponds to the opposite category.
Eric Wieser (Apr 29 2022 at 13:07):
With open_locale order_dual I assume?
Johan Commelin (Apr 29 2022 at 13:08):
Something like that?
Yaël Dillies (Apr 29 2022 at 13:08):
I would like the notation to not be localized because order_dual is used very widely.
Johan Commelin (Apr 29 2022 at 13:11):
Hmm. So maybe we shouldn't try to merge order_dual and opposite.
Johan Commelin (Apr 29 2022 at 13:11):
And so they shouldn't get the same notation either.
Yaël Dillies (Apr 29 2022 at 13:14):
In the context of docs#preorder.small_category, the correspondance of order_dual and opposite is very neat: αᵒᵈ ≌ αᵒᵖ.
Johan Commelin (Apr 29 2022 at 13:15):
Yeah, but it's certainly not a defeq.
Reid Barton (Apr 29 2022 at 13:15):
α﹥⇄﹤
This would have been a good name for what it was like to use the opposite category before it was made irreducible :confounded:
Reid Barton (Apr 29 2022 at 13:16):
I don't have a strong opinion but αᵒᵈ is cute and seems as good as anything else
Yaël Dillies (Apr 29 2022 at 13:17):
Johan Commelin said:
Yeah, but it's certainly not a defeq.
Was before opposite was reducible, I believe.
Yaël Dillies (Apr 29 2022 at 13:20):
Actually, I believe we could merge order_dual and opposite, were it not for the defeq abuse happening all over the order theory library to dualize results.
Yaël Dillies (Apr 29 2022 at 13:21):
By that I mean that we never seem to put an incompatible category structure on an order.
Yaël Dillies (Apr 29 2022 at 13:25):
It is probably saner to keep them separate for now, as merging them does not seem to buy us anything except one notation to learn, two "identity" coercions, and having to construct αᵒᵈ ≌ αᵒᵖ by hand.
Yaël Dillies (Apr 29 2022 at 15:55):
#13798 (warning, huge!)
Yaël Dillies (Apr 30 2022 at 13:34):
Okay, #13798 compiles! Could it be merged quick?
Eric Wieser (May 02 2022 at 10:23):
That PR is so big that it's painful to even write comments in the github UI. So it would have been really helpful if you had made there be nothing to comment on, rather than slipping in some unrelated tidy ups!
Yaël Dillies (May 02 2022 at 10:24):
Sorry... fixing it now
Last updated: Dec 20 2023 at 11:08 UTC