monotonic isomorphism between finite sets

Stream: maths

[Chris Hughes]

I'm looking for a lexicographic total order on fin a × fin b and a proof that's it's isomorphic to the lexicographic total order on fin b × fin a. Is this easy in lean?

[Chris Hughes]

No longer needed

[Chris Hughes]

Turns out I do need it after all. I need a linear order isomorphism between any two totally ordered types of the same size. Is that anywhere in lean? Seems like the sort of thing that might have come up doing ordinals.

[Johan Commelin]

I have no idea whether this is in Lean. Also, I'm not a master of finsets, like you are. But my initial attempt would be to prove this by induction. Construct a map to fin n. If the cardinality is 0, then it's easy. If it is k+1 construct a map to fin k+1 by sending the largest element to k.

[Johan Commelin]

Do you in fact also want to prove that the linear order isom is unique?

[Chris Hughes]

I don't care if it's unique I don't think.

[Mario Carneiro]

I need a linear order isomorphism between any two totally ordered types of the same size

This isn't true for all types, e.g. nat and int are not order isomorphic

[Mario Carneiro]

This fact for finite linear orders is a special case of the uniqueness of well orders in the finite case

[Kevin Buzzard]

He's only interested in finite types surely

[Chris Hughes]

I do mean finite

[Kevin Buzzard]

So the question is "is existence and uniqueness (up to permutation) of a total order on a finite type in Lean"?

[Mario Carneiro]

ord n essentially imposes a well order on any set (or the well order theorem directly), which gives you the existence part

[Chris Hughes]

The uniqueness is what I care about.

[Mario Carneiro]

A linear order of a finite set is a well order, so you get an embedding of each order into ordinal; the cardinals for these orders is equal so you have uniqueness by ord_nat and hence an order isomorphism

[Mario Carneiro]

(this is probably an excessively high powered proof)

[Kenny Lau]

I'm still struggling with something like

noncomputable def something : @order_iso (α) (fin $ fintype.card α) (<) (<) :=
classical.choice $ ordinal.type_eq.1 $ (ordinal.fintype_card (<)).trans (ordinal.lift_type_fin $ fintype.card α).symm

[Kenny Lau]

(I hadn't read the messages by Mario)

[Kenny Lau]

oh and my incomplete code (posting here because I don't want to work with it now):

[Kenny Lau]

import set_theory.ordinal

universes u v w

variables (α : Type u) [fintype α] [linear_order α]
variables (β : Type v) [has_lt β] [is_well_order β (<)]
variables (γ : Type w)

instance is_well_order_of_fintype : is_well_order α (<) :=
{ wf := sorry }

@[simp] lemma ulift_up_eq (x y : γ) : ulift.up x = ulift.up y ↔ x = y :=
⟨ulift.up.inj, congr_arg _⟩

instance ulift.is_well_order : is_well_order (ulift.{u v} β) (equiv.ulift.to_fun ⁻¹'o has_lt.lt) :=
{ trans := λ ⟨x⟩ ⟨y⟩ ⟨z⟩ Hxy Hyz, @is_trans.trans β (<) _ x y z Hxy Hyz,
  irrefl := λ ⟨x⟩ H, is_irrefl.irrefl (<) x H,
  trichotomous := λ ⟨x⟩ ⟨y⟩, by simpa using is_trichotomous.trichotomous (<) x y,
  wf := inv_image.wf _ $ is_well_order.wf _ }

noncomputable def something : @order_iso (α) (fin $ fintype.card α) (<) (<) :=
classical.choice $ ordinal.type_eq.1 $ (ordinal.fintype_card (<)).trans (ordinal.lift_type_fin $ fintype.card α).symm
#check cardinal.ord_nat
#check something