# The back and forth method and countable dense linear orders #

## Results #

Suppose α β are linear orders, with α countable and β dense, nontrivial. Then there is an order embedding α ↪ β. If in addition α is dense, nonempty, without endpoints and β is countable, without endpoints, 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

theorem Order.exists_between_finsets {α : Type u_1} [] [] [] [] [nonem : ] (lo : ) (hi : ) (lo_lt_hi : xlo, yhi, x < y) :
∃ (m : α), (xlo, x < m) yhi, m < y

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

def Order.PartialIso (α : Type u_1) (β : Type u_2) [] [] :
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
• = { f : Finset (α × β) // pf, qf, cmp p.1 q.1 = cmp p.2 q.2 }
Instances For
instance Order.PartialIso.instInhabited (α : Type u_1) (β : Type u_2) [] [] :
Equations
• = { default := , }
instance Order.PartialIso.instPreorder (α : Type u_1) (β : Type u_2) [] [] :
Equations
theorem Order.PartialIso.exists_across {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] (f : ) (a : α) :
∃ (b : β), pf, cmp p.1 a = cmp p.2 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.

def Order.PartialIso.comm {α : Type u_1} {β : Type u_2} [] [] :

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

Equations
Instances For
def Order.PartialIso.definedAtLeft {α : Type u_1} (β : Type u_2) [] [] [] [] [] [] (a : α) :

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
• = { carrier := {f : | ∃ (b : β), (a, b) f}, mem_gt := }
Instances For
def Order.PartialIso.definedAtRight (α : Type u_1) {β : Type u_2} [] [] [] [] [] [] (b : β) :

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
• = { carrier := {f : | ∃ (a : α), (a, b) f}, mem_gt := }
Instances For
def Order.PartialIso.funOfIdeal {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] (a : α) (I : ) :
(f, f I){ b : β // fI, (a, b) f }

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

Equations
Instances For
def Order.PartialIso.invOfIdeal {α : Type u_1} {β : Type u_2} [] [] [] [] [] [] (b : β) (I : ) :
(f, f I){ a : α // fI, (a, b) f }

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

Equations
Instances For
theorem Order.embedding_from_countable_to_dense (α : Type u_1) (β : Type u_2) [] [] [] [] [] :
Nonempty (α ↪o β)

Any countable linear order embeds in any nontrivial dense linear order.

theorem Order.iso_of_countable_dense (α : Type u_1) (β : Type u_2) [] [] [] [] [] [] [] [] [] [] [] [] :
Nonempty (α ≃o β)

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