The back and forth method and countable dense linear orders #

Results #

Suppose α β are linear orders, with α countable and β dense, nonempty, without endpoints. Then there is an order embedding α ↪ β. If in addition α is dense, nonempty, without endpoints and β is countable, then we can upgrade this to an order isomorphism α ≃ β.

The idea for both results is to consider "partial isomorphisms", which identify a finite subset of α with a finite subset of β, and prove that for any such partial isomorphism f and a : α, we can extend f to include a in its domain.

References #

https://en.wikipedia.org/wiki/Back-and-forth_method

Tags #

back and forth, dense, countable, order

source

theorem order.exists_between_finsets {α : Type u_1} [linear_order α] [densely_ordered α] [no_min_order α] [no_max_order α] [nonem : nonempty α] (lo hi : finset α) (lo_lt_hi : ∀ (x : α), x ∈ lo → ∀ (y : α), y ∈ hi → x < y) :

∃ (m : α), (∀ (x : α), x ∈ lo → x < m) ∧ ∀ (y : α), y ∈ hi → m < y

Suppose α is a nonempty dense linear order without endpoints, and suppose lo, hi, are finite subssets with all of lo strictly before hi. Then there is an element of α strictly between lo and hi.

source

def order.partial_iso (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] :

Type (max u_1 u_2)

The type of partial order isomorphisms between α and β defined on finite subsets. A partial order isomorphism is encoded as a finite subset of α × β, consisting of pairs which should be identified.

Equations

order.partial_iso α β = {f // ∀ (p : α × β), p ∈ f → ∀ (q : α × β), q ∈ f → cmp p.fst q.fst = cmp p.snd q.snd}

source

@[protected, instance]

def order.partial_iso.inhabited (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] :

inhabited (order.partial_iso α β)

Equations

order.partial_iso.inhabited α β = {default := ⟨∅, _⟩}

source

@[protected, instance]

def order.partial_iso.preorder (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] :

preorder (order.partial_iso α β)

Equations

order.partial_iso.preorder α β = subtype.preorder (λ (f : finset (α × β)), ∀ (p : α × β), p ∈ f → ∀ (q : α × β), q ∈ f → cmp p.fst q.fst = cmp p.snd q.snd)

source

theorem order.partial_iso.exists_across {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] [densely_ordered β] [no_min_order β] [no_max_order β] [nonempty β] (f : order.partial_iso α β) (a : α) :

∃ (b : β), ∀ (p : α × β), p ∈ f.val → cmp p.fst a = cmp p.snd b

For each a, we can find a b in the codomain, such that a's relation to the domain of f is b's relation to the image of f.

Thus, if a is not already in f, then we can extend f by sending a to b.

source

@[protected]

noncomputable def order.partial_iso.comm {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] :

order.partial_iso α β → order.partial_iso β α

A partial isomorphism between α and β is also a partial isomorphism between β and α.

Equations

order.partial_iso.comm = subtype.map (finset.image ⇑(equiv.prod_comm α β)) order.partial_iso.comm._proof_1

source

def order.partial_iso.defined_at_left {α : Type u_1} (β : Type u_2) [linear_order α] [linear_order β] [densely_ordered β] [no_min_order β] [no_max_order β] [nonempty β] (a : α) :

order.cofinal (order.partial_iso α β)

The set of partial isomorphisms defined at a : α, together with a proof that any partial isomorphism can be extended to one defined at a.

Equations

order.partial_iso.defined_at_left β a = {carrier := λ (f : order.partial_iso α β), ∃ (b : β), (a, b) ∈ f.val, mem_gt := _}

source

def order.partial_iso.defined_at_right (α : Type u_1) {β : Type u_2} [linear_order α] [linear_order β] [densely_ordered α] [no_min_order α] [no_max_order α] [nonempty α] (b : β) :

order.cofinal (order.partial_iso α β)

The set of partial isomorphisms defined at b : β, together with a proof that any partial isomorphism can be extended to include b. We prove this by symmetry.

Equations

order.partial_iso.defined_at_right α b = {carrier := λ (f : order.partial_iso α β), ∃ (a : α), (a, b) ∈ f.val, mem_gt := _}

source

noncomputable def order.partial_iso.fun_of_ideal {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] [densely_ordered β] [no_min_order β] [no_max_order β] [nonempty β] (a : α) (I : order.ideal (order.partial_iso α β)) :

(∃ (f : order.partial_iso α β), f ∈ order.partial_iso.defined_at_left β a ∧ f ∈ I) → {b // ∃ (f : {f // ∀ (p : α × β), p ∈ f → ∀ (q : α × β), q ∈ f → cmp p.fst q.fst = cmp p.snd q.snd}) (H : f ∈ I), (a, b) ∈ f.val}

Given an ideal which intersects defined_at_left β a, pick b : β such that some partial function in the ideal maps a to b.

Equations

order.partial_iso.fun_of_ideal a I = classical.indefinite_description (λ (b : β), ∃ (f : {f // ∀ (p : α × β), p ∈ f → ∀ (q : α × β), q ∈ f → cmp p.fst q.fst = cmp p.snd q.snd}) (H : f ∈ I), (a, b) ∈ f.val) ∘ _

source

noncomputable def order.partial_iso.inv_of_ideal {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] [densely_ordered α] [no_min_order α] [no_max_order α] [nonempty α] (b : β) (I : order.ideal (order.partial_iso α β)) :

(∃ (f : order.partial_iso α β), f ∈ order.partial_iso.defined_at_right α b ∧ f ∈ I) → {a // ∃ (f : {f // ∀ (p : α × β), p ∈ f → ∀ (q : α × β), q ∈ f → cmp p.fst q.fst = cmp p.snd q.snd}) (H : f ∈ I), (a, b) ∈ f.val}

Given an ideal which intersects defined_at_right α b, pick a : α such that some partial function in the ideal maps a to b.

Equations

order.partial_iso.inv_of_ideal b I = classical.indefinite_description (λ (a : α), ∃ (f : {f // ∀ (p : α × β), p ∈ f → ∀ (q : α × β), q ∈ f → cmp p.fst q.fst = cmp p.snd q.snd}) (H : f ∈ I), (a, b) ∈ f.val) ∘ _

source

noncomputable def order.embedding_from_countable_to_dense (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] [encodable α] [densely_ordered β] [no_min_order β] [no_max_order β] [nonempty β] :

α ↪o β

Any countable linear order embeds in any nonempty dense linear order without endpoints.

Equations

order.embedding_from_countable_to_dense α β = let our_ideal : order.ideal (order.partial_iso α β) := order.ideal_of_cofinals default (order.partial_iso.defined_at_left β), F : Π (a : α), {b // ∃ (f : {f // ∀ (p : α × β), p ∈ f → ∀ (q : α × β), q ∈ f → cmp p.fst q.fst = cmp p.snd q.snd}) (H : f ∈ our_ideal), (a, b) ∈ f.val} := λ (a : α), order.partial_iso.fun_of_ideal a our_ideal _ in order_embedding.of_strict_mono (λ (a : α), (F a).val) _

source

noncomputable def order.iso_of_countable_dense (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] [encodable α] [densely_ordered α] [no_min_order α] [no_max_order α] [nonempty α] [encodable β] [densely_ordered β] [no_min_order β] [no_max_order β] [nonempty β] :

α ≃o β

Any two countable dense, nonempty linear orders without endpoints are order isomorphic.

Equations

order.iso_of_countable_dense α β = let to_cofinal : α ⊕ β → order.cofinal (order.partial_iso α β) := λ (p : α ⊕ β), p.rec_on (order.partial_iso.defined_at_left β) (order.partial_iso.defined_at_right α), our_ideal : order.ideal (order.partial_iso α β) := order.ideal_of_cofinals default to_cofinal, F : Π (a : α), {b // ∃ (f : {f // ∀ (p : α × β), p ∈ f → ∀ (q : α × β), q ∈ f → cmp p.fst q.fst = cmp p.snd q.snd}) (H : f ∈ our_ideal), (a, b) ∈ f.val} := λ (a : α), order.partial_iso.fun_of_ideal a our_ideal _, G : Π (b : β), {a // ∃ (f : {f // ∀ (p : α × β), p ∈ f → ∀ (q : α × β), q ∈ f → cmp p.fst q.fst = cmp p.snd q.snd}) (H : f ∈ our_ideal), (a, b) ∈ f.val} := λ (b : β), order.partial_iso.inv_of_ideal b our_ideal _ in order_iso.of_cmp_eq_cmp (λ (a : α), (F a).val) (λ (b : β), (G b).val) _