Zulip Chat Archive

Stream: maths

Topic: monotonic isomorphism between finite sets


view this post on Zulip Chris Hughes (Aug 18 2018 at 18:32):

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?

view this post on Zulip Chris Hughes (Aug 18 2018 at 19:14):

No longer needed

view this post on Zulip Chris Hughes (Aug 21 2018 at 10:01):

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.

view this post on Zulip Johan Commelin (Aug 21 2018 at 10:09):

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.

view this post on Zulip Johan Commelin (Aug 21 2018 at 10:16):

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

view this post on Zulip Chris Hughes (Aug 21 2018 at 10:20):

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

view this post on Zulip Mario Carneiro (Aug 21 2018 at 11:40):

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

view this post on Zulip Mario Carneiro (Aug 21 2018 at 11:41):

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

view this post on Zulip Kevin Buzzard (Aug 21 2018 at 11:47):

He's only interested in finite types surely

view this post on Zulip Chris Hughes (Aug 21 2018 at 11:54):

I do mean finite

view this post on Zulip Kevin Buzzard (Aug 21 2018 at 11:59):

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

view this post on Zulip Mario Carneiro (Aug 21 2018 at 12:01):

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

view this post on Zulip Chris Hughes (Aug 21 2018 at 12:02):

The uniqueness is what I care about.

view this post on Zulip Mario Carneiro (Aug 21 2018 at 12:11):

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

view this post on Zulip Mario Carneiro (Aug 21 2018 at 12:11):

(this is probably an excessively high powered proof)

view this post on Zulip Kenny Lau (Aug 21 2018 at 12:30):

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

view this post on Zulip Kenny Lau (Aug 21 2018 at 12:30):

(I hadn't read the messages by Mario)

view this post on Zulip Kenny Lau (Aug 21 2018 at 12:39):

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

view this post on Zulip Kenny Lau (Aug 21 2018 at 12:39):

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

Last updated: May 11 2021 at 16:22 UTC