## Stream: maths

### Topic: order_iso

#### Yury G. Kudryashov (Jul 23 2020 at 04:51):

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 (Jul 23 2020 at 05:15):

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 (Jul 23 2020 at 05:41):

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

#### Mario Carneiro (Jul 23 2020 at 05:43):

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 (Jul 23 2020 at 05:44):

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

#### Mario Carneiro (Jul 23 2020 at 05:45):

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 (Jul 23 2020 at 05:46):

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 (Jul 23 2020 at 06:24):

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 (Jul 23 2020 at 06:40):

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 (Aug 12 2020 at 19:17):

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

#### Aaron Anderson (Aug 12 2020 at 19:26):

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 (Aug 12 2020 at 20:02):

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 (Aug 12 2020 at 20:03):

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

#### Yury G. Kudryashov (Aug 12 2020 at 20:04):

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

#### Aaron Anderson (Aug 12 2020 at 20:07):

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

#### Mario Carneiro (Aug 12 2020 at 20:08):

le is the default for most order classes

#### Mario Carneiro (Aug 12 2020 at 20:09):

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

#### Aaron Anderson (Aug 12 2020 at 20:11):

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 (Aug 12 2020 at 20:47):

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 (Aug 12 2020 at 20:49):

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 (Aug 12 2020 at 20:51):

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

#### Aaron Anderson (Aug 12 2020 at 20:52):

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 (Aug 12 2020 at 21:26):

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

#### Aaron Anderson (Aug 16 2020 at 17:32):

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 (Aug 16 2020 at 17:33):

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

#### Aaron Anderson (Aug 16 2020 at 17:36):

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 (Aug 16 2020 at 17:47):

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 (Aug 16 2020 at 17:48):

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

#### Aaron Anderson (Aug 16 2020 at 17:51):

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 (Aug 16 2020 at 22:15):

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 (Aug 16 2020 at 22:16):

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

#### Aaron Anderson (Aug 16 2020 at 22:18):

They’re probably actually just true in partial orders

#### Yury G. Kudryashov (Aug 17 2020 at 03:15):

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.

#3838

#### Aaron Anderson (Aug 17 2020 at 06:03):

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

Last updated: May 12 2021 at 06:14 UTC