Sorting by function value

Stream: Is there code for X?

[Peter Nelson]

Is there a way to prove this already in mathlib?

import data.set.finite

lemma foo {α β : Type*} [finite α] [linear_order α] [linear_order β] (f : α ↪ β) :
  ∃ (e : β ≃ β), monotone (e ∘ f) := sorry

[Kevin Buzzard]

As it stands, doesn't that just say the false statement "some random injection from a finite linear order to an arbitrary linear order preserves the order"? Or am I missing something? For example alpha=beta={0,1}, f=identity, e=x\mapsto 1-x?

[Peter Nelson]

I don't think so; it's saying that after composing with an appropriate permutation, the random injection preserves the order.

[Damiano Testa]

There is docs#linear_extension. So you could probably define a partial order on β by saying that the elements that come from α have their order from α, everything else is bigger and then linearly extend. Not sure how pleasant this would be, though.

[Damiano Testa]

Possibly inducing a partial order from mapping β to with_top α might help with some of the steps.

[Kyle Miller]

Maybe what's in https://leanprover-community.github.io/mathlib_docs/data/fin/tuple/sort.html could be generalized to linear orders? This one is for permuting a finite domain rather than permuting the codomain.

[Alex J. Best]

import data.set.finite
import data.fintype.sort
import logic.equiv.fintype
import group_theory.perm.fin

open equiv

lemma foo {α β : Type*} [finite α] [linear_order α] [linear_order β] (f : α ↪ β) :
  ∃ (e : β ≃ β), monotone (e ∘ f) :=
begin
  casesI nonempty_fintype α,
  use perm.extend_domain (((mono_equiv_of_fin α rfl).to_equiv.trans (f.to_equiv_range.trans ((mono_equiv_of_fin (set.range f) (fintype.card_range _)).symm.to_equiv))).symm) (mono_equiv_of_fin (set.range f) (fintype.card_range _)).to_equiv,
  intros x y hxy,
  simpa [perm.extend_domain_apply_subtype],
end

-- un-obfuscated
lemma foo' {α β : Type*} [finite α] [linear_order α] [linear_order β] (f : α ↪ β) :
  ∃ (e : β ≃ β), monotone (e ∘ f) :=
begin
  casesI nonempty_fintype α,
  let a := (mono_equiv_of_fin (set.range f) (fintype.card_range _)).symm.to_equiv,
  let b := f.to_equiv_range,
  let c := (mono_equiv_of_fin α rfl).to_equiv,
  let : perm (fin _) := (c.trans (b.trans a)).symm,
  let e : perm β := this.extend_domain (mono_equiv_of_fin (set.range f) (fintype.card_range _)).to_equiv,
  use e,
  simp [e, this, a, b, c],
  intros x y hxy,
  simpa [perm.extend_domain_apply_subtype],
end

[Damiano Testa]

docs#equiv.perm.extend_domain: very nice!

[Peter Nelson]

Thank you!

[Patrick Johnson]

Is it true for infinite α?

[Junyan Xu]

No, you can't reorder permute N to get its dual order ...

[Kyle Miller]

@Junyan Xu How do you mean? Can't e flip N back over?

[Eric Wieser]

I think the scenario in question is when f = order_dual.to_dual.to_embedding

[Kyle Miller]

For infinite α, I think it might be true at least when it's countable. In the general case, I'd think the fact that there are different order types with the same cardinality would be an obstruction.

[Eric Wieser]

I thought we concluded it's not even true when α = nat (f = order_dual.to_dual.to_embedding, β = order_dual nat)?

[Kyle Miller]

Oh right, not sure how you'd flip N over...

[Eric Wieser]

Proof goes something like "if there was one, e 0 would have to be greater than all other nats, but then nat would be finite"