Pi.Lex

Stream: mathlib4

[Violeta Hernández]

I think I've asked this before, but I'll ask again. Isn't the order on docs#Pi.Lex backwards?

[Violeta Hernández]

Specifically, docs#Finsupp.Lex.wellFoundedLT says that Lex (α →₀ N) is well-founded when N is well-founded, and α is... co-well-founded?

[Violeta Hernández]

Is this something that comes up often? I would imagine that the lexicographic ordering on functions is most useful when the domain is well-ordered, like ℕ or Ordinal.

[Violeta Hernández]

Having to write down Finsupp.equivMapDomain OrderDual.toDual just to get the correct ordering for my use-case is quite annoying

[Yaël Dillies]

@Weiyi Wang, what's your opinion?

[Bhavik Mehta]

I think this is the usual definition of Lex on functions, and swapping the order on the domain type would give us the colex order. See eg the colex section of https://en.m.wikipedia.org/wiki/Lexicographic_order

[Violeta Hernández]

Do note that strictly speaking, the Wikipedia article talks about the lex order on strings, rather than functions. And there is precedent to indexing strings from right to left, e.g. when talking about digit expansions.

[Violeta Hernández]

I also found this nlab article which seems to agree with me on the lex ordering: https://ncatlab.org/nlab/show/lexicographic+order

[Bhavik Mehta]

Violeta Hernández said:

Do note that strictly speaking, the Wikipedia article talks about the lex order on strings, rather than functions.

Indeed, that's why I specifically mentioned the colex section which talks about the order on functions!

[Bhavik Mehta]

I think nlab also disagrees with you, it's talking about the least place where they differ, which is what docs#Pi.Lex does

[Violeta Hernández]

Oh, you're right.

[Violeta Hernández]

It seems like the restriction to finsupps is the cause for this disparity. For Lex (α → β) to be linearly ordered, you need β to be linearly ordered and α to be well-ordered. Whereas for Lex (α →₀ β) you only need α and β to be linearly ordered, and you furthermore get a well-order when α is co-well-ordered.

[Violeta Hernández]

I think it's quite reasonable for both the lex orderings on ℕ → α and ℕ →₀ α to come up, so someone had to end up disappointed

[Bhavik Mehta]

I'm not sure there's any disparity at all, the non-well-foundedness of lex on finitely supported things is expected:

It is not true that the set of all finite words is well-ordered; for example, the infinite set of words {b, ab, aab, aaab, ... } has no lexicographically earliest element.

[Violeta Hernández]

Well, there's an asymmetry in the mathematics themselves, is my point

[Violeta Hernández]

Yeah, I think the ordering as-is is the correct one. Guess I'll have to get comfortable inserting order duals.

[Bhavik Mehta]

It might be reasonable to make Pi.Colex. Or more specifically to make a type synonym Colex analogous to docs#Lex, and put the right order on it; and also use this for docs#Finset.Colex. I'm interested to hear Yaël's thoughts on this. My impression was that Colex is only really useful for finsets, but last week I found an application for it for finitely supported order embeddings, and it sounds like you want it to work for Finsupps too

[Violeta Hernández]

Wait, what's the relationship between Finset.Colex and Pi.Colex? I don't see it at first glance.

[Bhavik Mehta]

It's certainly not clear, but I happened to prove a version of it last week:

lemma colex_orderEmb {α β : Type*} [LinearOrder α] [LinearOrder β] [Fintype α] {x y : α ↪o β} :
    toColex (univ.image x) < toColex (univ.image y) ↔ ∃ i, x i < y i ∧ ∀ j, i < j → x j = y j := by

[Bhavik Mehta]

(this probably generalises in some way, I haven't thought about it yet)

[Violeta Hernández]

Would this work if you replaced α ↪o β with α →₀ β?

[Bhavik Mehta]

No, since the functions could reorder the points randomly

[Bhavik Mehta]

The way to think about x, y here is that they're increasing enumerations of the finset

[Bhavik Mehta]

I could replace them with finitely supported strictly monotone functions, though; they're already finitely supported because [Fintype α]

[Violeta Hernández]

Well, a Colex alias would certainly save me from some hassle, though I do worry that it might take more work to set up than to simply insert some spurious OrderDuals here and there.

[Yaël Dillies]

Bhavik Mehta said:

It might be reasonable to make Pi.Colex. Or more specifically to make a type synonym Colex analogous to docs#Lex, and put the right order on it; and also use this for docs#Finset.Colex.

This was always on my mind, and the sole reason I didn't do it is because I didn't have an application! Looks like we do now :slight_smile:

[Bhavik Mehta]

Violeta Hernández said:

Wait, what's the relationship between Finset.Colex and Pi.Colex? I don't see it at first glance.

Just to make this completely explicit, this is true:

lemma colex_orderEmb_iff {α β : Type*}
    [LinearOrder α] [LinearOrder β] [Fintype α] {x y : α ↪o β} :
    toColex (univ.image x) < toColex (univ.image y) ↔
    Pi.Lex (· > ·) (· < ·) x y := by

(and univ.image · is a bijection between α ↪o β and finsets in β with size card α).

[Violeta Hernández]

Which types would have the Colex alias? Pi types, finsupps, finsets, anything else?

[Aaron Liu]

Is finset Colex is equivalent to the subtype of Pi lex where the codomain is Prop and the function is finitely supported

[Bhavik Mehta]

No:

import Mathlib

noncomputable def asFinsupp (s : Finset α) : Lex (α → Prop) := toLex (· ∈ s)

@[simp] lemma false_lt_true : False < True := by simp [lt_iff_le_and_ne]

example : asFinsupp {2, 3} < asFinsupp {1, 2} := ⟨1, by simp [asFinsupp]⟩

Finset lex and finset colex would have {1,2} < {2,3}, but taking the indicator functions on these give the opposite order

[Bhavik Mehta]

(aside: surely a single tactic should prove False < True)

[Aaron Liu]

oh

[Aaron Liu]

yeah that makes sense

[Violeta Hernández]

Violeta Hernández said:

Which types would have the Colex alias? Pi types, finsupps, finsets, anything else?

Also, all the material on docs#Finsupp.Colex is currently in the namesake namespace. Should that remain true after generalizing the alias?

[Violeta Hernández]

I've opened #29058 introducing a Colex type synonym, replacing the existing Finset.Colex one.

[Aaron Liu]

Bhavik Mehta said:

No:

import Mathlib

noncomputable def asFinsupp (s : Finset α) : Lex (α → Prop) := toLex (· ∈ s)

@[simp] lemma false_lt_true : False < True := by simp [lt_iff_le_and_ne]

example : asFinsupp {2, 3} < asFinsupp {1, 2} := ⟨1, by simp [asFinsupp]⟩

Finset lex and finset colex would have {1,2} < {2,3}, but taking the indicator functions on these give the opposite order

Wait so if it's the other way around is finset colex isomorphic to finsupp lex?

[Bhavik Mehta]

Sorry, I meant gives the opposite order on these specific places. I considered briefly if you get the opposite order entirely, but didn't have time to prove or disprove it

[Violeta Hernández]

Isn't colex ordering on finsets the same as the ordering on binary expansions, which is the colex ordering on finsupps?

[Violeta Hernández]

(if this is true, would it be a good idea to directly redefine Finsupp colex using this? It would at the very least make the proof that they're a linear order much more immediate)

[Bryan Gin-ge Chen]

@Bhavik Mehta I was assigned #29058 (feat: Colex type synonym), which I guess was discussed in this thread. Could you take a look when you have a chance?

[Antoine Chambert-Loir]

Bhavik Mehta said:

I think this is the usual definition of Lex on functions, and swapping the order on the domain type would give us the colex order. See eg the colex section of https://en.m.wikipedia.org/wiki/Lexicographic_order

Right, but both conventions exist and I found that having to swap the ordering on the domain was sometimes more painful than expected.

[Antoine Chambert-Loir]

This colex stuff is basically what blocked my definition of the degrevlex monomial order.

[Bhavik Mehta]

Is it really true that both conventions exist? I've only ever seen the mathlib one used for "lex". In any case, I think the above PR should make it less painful to use the colex/revlex order

[Violeta Hernández]

I've definitely seen people use "lexicographic" when referring to the colex ordering on ordinal finsupps. Here's a Wikipedia excerpt:
image.png

[Violeta Hernández]

I guess you could argue "lexicographically with the least significant position first" is just a long-winded way of saying "colexicographically"

[Bhavik Mehta]

Yeah this is quite literally saying, lex but with an order dual in there, which is what colex already is

[Violeta Hernández]

fair enough