order_iso

Stream: maths

[Yury G. Kudryashov]

Currently order_iso takes two relations as arguments. I have an impression that most of the time (at least outside of set_theory/ordinal) these relations are le and le. What do you think about hardcoding this, i.e. define

structure order_iso (α β : Type*) [has_le α] [has_le β] extends α ≃ β :=
(map_le_iff' : ∀ x y, to_fun x ≤ to_fun y ↔ x ≤ y)

How much will it break in set_theory?

[Yury G. Kudryashov]

The main gain for the rest of the library is that α ≃o β looks better than (≤) ≃o (≤) in output and much better than ((≤) : α → α → Prop) ≃o ... in input.

[Yury G. Kudryashov]

@Mario Carneiro You're the author of order_iso.lean, so probably you have an opinion about this :up:.

[Mario Carneiro]

I think there is a need for the general relation version when doing actual order theory, but I also see the use for an equiv for ordered types

[Mario Carneiro]

I think in set_theory.ordinal the relation isn't even <=-like, it is <-like

[Mario Carneiro]

order_iso is meant to play nice with the "explicit relation" versions of order classes, like is_irreflexive, is_transitive and so on

[Mario Carneiro]

I think you should probably just define a separate type for the le-hardcoded version when working in partial_order, linear_order and descendents

[Aaron Anderson]

order_iso is also the definition of isomorphism for every other kind of (first-order) structure consisting of a single binary relation, and order_embedding seems similarly general. Could we rename it to rel_iso and then make order_iso a rel_iso between two instances of has_le.le?

[Aaron Anderson]

Hopefully one wouldn't have to add too many extra instances and coercions, and then you get to use it to define graph embeddings and isomorphisms too

[Aaron Anderson]

I've started doing this at mathlib:rel_iso. My plan is roughly to make the following PRs:

• Change the notation for order_iso to use rel_iso (will PR today once it builds)
• Add abbreviations for le_iso (and embedding) and lt_iso, which should be the new definition of order_iso we were talking about.
• As many PRs as it takes to swap over existing rel_isos to using le_iso and lt_iso where relevant, with any new required lemmas
• Add rel_hom, to denote a map such that r x y -> s (f x) (f y), without the iff, and connect that to monotone

[Kevin Buzzard]

It's about time we had stuff like this

[Aaron Anderson]

By then hopefully we'll have a definition simple_graph, and can use this to define graph homomorphisms, and it'll play really nicely with first-order structures if I make any headway porting flypitch

[Yury G. Kudryashov]

Note that le_iso (resp., le_embedding) is automatically an lt_iso (resp., lt_embedding), and for a partial_order the reversed implication is true as well.

[Aaron Anderson]

I think there are some lemmas to that effect in order_iso.lean, although without the new notation

[Yury G. Kudryashov]

I think that we should choose one of le/lt as the standard interface for partial_order and up.

[Aaron Anderson]

le makes more sense to me, but @Mario Carneiro indicated that the ordinal library usually prefers lt, possibly for good reasons

[Mario Carneiro]

le is the default for most order classes

[Mario Carneiro]

the ordinal library builds on unbundled order classes though, which have both le and lt friendly predicates

[Aaron Anderson]

Assuming there's no easy way to convert the ordinal library to only use le_embedding, should I make two abbreviations, with a note that le_embedding is preferred elsewhere, or just leave lt_embedding unabbreviated?

[Yury G. Kudryashov]

As far as I understand, the ordinal library doesn't use has_lt.lt. It uses an explicit argument r instead; this r is a strict order, so we can't just drop the current order_embedding and use le_embedding everywhere.

[Aaron Anderson]

What I mean by leaving lt_embedding unabbreviated is to rename order_embedding to rel_embedding (working on that right now) and otherwise leave the ordinal library the same, except any places it uses has_le.le.

[Aaron Anderson]

The ordinal library does sometimes use @order_embedding a b (<) (<)

[Aaron Anderson]

So I would have created a name for that, but you're right that it's probably inviting trouble to have two reasonable definitions that could each be thought of as order embeddings.

[Aaron Anderson]

#3750 is just the renaming of order_embedding/iso to rel_embedding/iso

[Aaron Anderson]

That PR merged, so I'm moving on. I'm finding that the rest of mathlib also uses <-embeddings pretty often, often constructing a <=-embedding and then a <-embedding consecutively, even in algebra.

[Aaron Anderson]

I think this means it's not inviting any more trouble than we're already in to define two abbreviations: ↪≤ and ↪<?

[Aaron Anderson]

It seems that the library for proving orders to be well-founded at least is better developed for <, so ↪< is what's useful for proving well-foundedness (e.g. for Noetherian), although for preorders they're equivalent

[Aaron Anderson]

I'll keep looking. If it's really just well-foundedness that's using ↪< on actual preorders, then I can just add a few lemmas to order/order_iso_nat to make it compatible with ↪≤, otherwise I think I'll add both

[Kevin Buzzard]

Scott would say that instead of all these new symbols you should just make them categories and then use functor notation.

[Aaron Anderson]

I've already given myself enough trouble elsewhere with the fact that category notation needs type synonyms to switch between different categories with the same objects

[Aaron Anderson]

Ok. I could confidently remove all of the lt_embeddings outside of order theory, and call le_embedding the real order_embedding, if I prove a few lemmas relating well-foundedness of lt and le in preorders

[Aaron Anderson]

But I’m not sure if those lemmas are true yet...

[Aaron Anderson]

They’re probably actually just true in partial orders

[Yury G. Kudryashov]

Kevin Buzzard said:

Scott would say that instead of all these new symbols you should just make them categories and then use functor notation.

Category morphism notation works only for objects in the same universe.

[Aaron Anderson]

#3838

[Aaron Anderson]

still has a few errors to catch it seems, but should be fixed soon