Order-reversing maps

Stream: maths

[Wrenna Robson]

I find myself often wishing we had clear spellings for "order-reversing map" and "Galois connection but it reverses the order", without using OrderDual. I know that you can use the dual, of course. But I don't like this as an option myself. For one thing - is the natural type of order-reversing maps Aᵒᵈ →o B or A →o Bᵒᵈ?

Personally I would like to see a world where we have A →oᵒᵈ B to mean "order-reversing map from A to B", and then an appropriate equivalence between A →oᵒᵈ B and Aᵒᵈ →o B and A →o Bᵒᵈ. I'm not sure if there's any appetite for this amongst contributors or maintainers. I assume this was considered before in the past and discounted?

This would also mean that the type of OrderDual.toDualwould be α ≃ᵒᵈ αᵒᵈ, which I think is nicer, personally.

Given we want to, probably, move to a world in which OrderDual is defined as a one-element structure, it would be even nicer to have this stuff: A →oᵒᵈ B and Aᵒᵈ →o B and A →o Bᵒᵈ are in that case different types, albeit (order)-isomorphic ones.

[Aaron Liu]

I really dislike it when there's multiple options but no canonical or "best" choice

[Wrenna Robson]

I agree, which I think means you might be agreeing with me - certainly at the moment that is the case! (because we have Aᵒᵈ →o B and A →o Bᵒᵈ and these both mean the same thing but, IMO, neither is better than the other).

[Wrenna Robson]

Given we have Antitone as a perfectly well-supported predicate, I see no issue with a mostly identical definition to OrderHom but with antitone' instead of monotone'.

[Aaron Liu]

Order isos are a bit more tricky since they're an abbrev for docs#RelIso

[Wrenna Robson]

I think that's fine, right? OrderAntiIso or whatever would also be such an abbrev, but with ge instead of le on the RHS (or, yes, on the LHS, but I think in this case that's just an implementation detail).

[Wrenna Robson]

Really it's weird that OrderHom isn't an abbrev for RelHom. I don't see why there isn't a consistent approach there.

[Kevin Buzzard]

I once developed a theory of contravariant functors and it was great -- I proved that composite of covariant and contravariant was contravariant, and that composite of two contravariant was covariant. What I liked about this was that there is literally no way of spelling contravariant in the "add an op somewhere" manner which makes "if F : A -> B and G : B -> C are contravariant functors, then GF is a covariant functor" typecheck -- you need both conventions in one statement. On the other hand Lean has got this far without contravariant functors and we have an absolute ton of stuff, so presumably our conventions are working great so far.

[Aaron Liu]

The reason I don't like them is if I'm stating a theorem or a def, which one should I use? There's nothing about them that makes one better than the other and there don't seem to be any conventions either.

[Wrenna Robson]

I wonder how much it's the case that people just fudge it. I agree with you precisely that that GF theorem would be good, Kevin - as you say you need both conventions to make it make sense!

[Wrenna Robson]

I think you can Just Fudge it (but we shouldn't), I think is my opinion.

[Wrenna Robson]

But I also think Monotone shouldn't require preorder, but the bottom of the order hierarchy is full of sharks and I am sure YD has good thoughts as to why this is wrong.

[Wrenna Robson]

(It is so weird that OrderHom requires Preorder but OrderEmbedding and OrderIso don't.)

[Wrenna Robson]

@Yaël Dillies why, by the way, is that?

[Wrenna Robson]

Like why is OrderHom not defined as @RelHom α β (· ≤ ·) (· ≤ ·)?