StrictMono for partial order

Stream: maths

[Yury G. Kudryashov]

Is docs#StrictMono the right notion for a map between partial orders, or is ∀ x y, f x ≤ f y ↔ x ≤ y better? They're equivalent if the domain is a linear order.

[Yury G. Kudryashov]

#xy: @Eric Wieser 's comment in #22426.

[Yury G. Kudryashov]

Note: in any case, I would prefer to have that PR merged before we decide whether to refactor StrictMono.

[Jireh Loreaux]

Isn't that docs#OrderEmbedding ?

[Yury G. Kudryashov]

Yes, this is a bundled version.

[Yury G. Kudryashov]

My question is: should we use the same predicate for StrictMono?

[Jireh Loreaux]

I don't understand. ∀ x y, f x ≤ f y ↔ x ≤ y means f is an order embedding, which is equivalent to strict monotonicity for linear orders, but in general they are different.

What's the question?

[Yury G. Kudryashov]

The question is: which one is more useful if the domain isn't a linear order?

[Violeta Hernández]

Why can't both be useful?

[Yury G. Kudryashov]

That's one of the possible answers.

[Yury G. Kudryashov]

AFAIR, I never needed StrictMono for partial orders, that's why I've decided to ask the question.

[Violeta Hernández]

I admit I can't come up with any (mathematically relevant) strict monotonic relations on partial orders that don't also satisfy the stronger condition...

[Eric Wieser]

Maybe something like commit date on a git graph?

[Eric Wieser]

I guess there the current definition is the right one, since otherwise the only strictly monotone graphs are linear

[Aaron Liu]

Violeta Hernández said:

I admit I can't come up with any (mathematically relevant) strict monotonic relations on partial orders that don't also satisfy the stronger condition...

Embed ℕ+ with divisibility into ℕ with the standard order

[Patrick Massot]

This has been discussed in the past. I think the docstring of StrictMono should have a big warning telling people that it is almost surely not what they want for partial orders, and link to OrderEmbedding.

[Aaron Liu]

Patrick Massot said:

This has been discussed in the past. I think the docstring of StrictMono should have a big warning telling people that it is almost surely not what they want for partial orders, and link to OrderEmbedding.

Is this how other people think about strictly monotone functions? As order embeddings? I've always thought of them as just that: functions which preserve the < relation, and also as essentially injective monotone functions monotone functions which are essentially injective on chains.

[Yury G. Kudryashov]

But if you want to generalize a fact about strictly monotone functions from linear orders to preorders, then quite probably the generalization will use order embeddings, not StrictMono functions.

[Patrick Massot]

Aaron Liu said:

Patrick Massot said:

This has been discussed in the past. I think the docstring of StrictMono should have a big warning telling people that it is almost surely not what they want for partial orders, and link to OrderEmbedding.

Is this how other people think about strictly monotone functions? As order embeddings? I've always thought of them as just that: functions which preserve the < relation, and also as essentially injective monotone functions.

See? This is why we need that big warning. It’s really really natural to think StrictMono implies injective if you don’t make the effort to specifically think about it.

[Junyan Xu]

I admit I can't come up with any (mathematically relevant) strict monotonic relations on partial orders that don't also satisfy the stronger condition...

strictMono_inf_prod_sup is an example that is not even injective in general.