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} [LinearOrder α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] [nonem : Nonempty α] (lo hi : Finset α) (lo_lt_hi : ∀ x ∈ lo, ∀ y ∈ hi, x < y) : ∃ (m : α), (∀ x ∈ lo, x < m) ∧ ∀ y ∈ hi, 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.

theorem Order.exists_orderEmbedding_insert {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] [DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β] [nonem : Nonempty β] (S : Finset α) (f : { x : α // x ∈ S } ↪o β) (a : α) : ∃ (g : { x : α // x ∈ insert a S } ↪o β), ⇑g ∘ Set.inclusion ⋯ = ⇑f

def Order.PartialIso (α : Type u_1) (β : Type u_2) [LinearOrder α] [LinearOrder β] : 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.PartialIso α β = { f : Finset (α × β) // ∀ p ∈ f, ∀ q ∈ f, cmp p.1 q.1 = cmp p.2 q.2 }

instance Order.PartialIso.instInhabited (α : Type u_1) (β : Type u_2) [LinearOrder α] [LinearOrder β] : Inhabited (Order.PartialIso α β)

Equations

• Order.PartialIso.instInhabited α β = { default := ⟨∅, ⋯⟩ }

instance Order.PartialIso.instPreorder (α : Type u_1) (β : Type u_2) [LinearOrder α] [LinearOrder β] : Preorder (Order.PartialIso α β)

Equations

• Order.PartialIso.instPreorder α β = Subtype.preorder fun (f : Finset (α × β)) => ∀ p ∈ f, ∀ q ∈ f, cmp p.1 q.1 = cmp p.2 q.2

theorem Order.PartialIso.exists_across {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] [DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β] [Nonempty β] (f : Order.PartialIso α β) (a : α) : ∃ (b : β), ∀ p ∈ ↑f, 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} [LinearOrder α] [LinearOrder β] : Order.PartialIso α β → Order.PartialIso β α

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

Equations

• Order.PartialIso.comm = Subtype.map (Finset.image ⇑(Equiv.prodComm α β)) ⋯

def Order.PartialIso.definedAtLeft {α : Type u_1} (β : Type u_2) [LinearOrder α] [LinearOrder β] [DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β] [Nonempty β] (a : α) : Order.Cofinal (Order.PartialIso α β)

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.PartialIso.definedAtLeft β a = { carrier := {f : Order.PartialIso α β | ∃ (b : β), (a, b) ∈ ↑f}, mem_gt := ⋯ }

def Order.PartialIso.definedAtRight (α : Type u_1) {β : Type u_2} [LinearOrder α] [LinearOrder β] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] [Nonempty α] (b : β) : Order.Cofinal (Order.PartialIso α β)

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.PartialIso.definedAtRight α b = { carrier := {f : Order.PartialIso α β | ∃ (a : α), (a, b) ∈ ↑f}, mem_gt := ⋯ }

def Order.PartialIso.funOfIdeal {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] [DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β] [Nonempty β] (a : α) (I : Order.Ideal (Order.PartialIso α β)) : (∃ f ∈ Order.PartialIso.definedAtLeft β a, f ∈ I) → { b : β // ∃ f ∈ I, (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

• Order.PartialIso.funOfIdeal a I = (Classical.indefiniteDescription fun (b : β) => ∃ f ∈ I, (a, b) ∈ ↑f) ∘ ⋯

def Order.PartialIso.invOfIdeal {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] [Nonempty α] (b : β) (I : Order.Ideal (Order.PartialIso α β)) : (∃ f ∈ Order.PartialIso.definedAtRight α b, f ∈ I) → { a : α // ∃ f ∈ I, (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

• Order.PartialIso.invOfIdeal b I = (Classical.indefiniteDescription fun (a : α) => ∃ f ∈ I, (a, b) ∈ ↑f) ∘ ⋯

theorem Order.embedding_from_countable_to_dense (α : Type u_1) (β : Type u_2) [LinearOrder α] [LinearOrder β] [Countable α] [DenselyOrdered β] [Nontrivial β] : 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) [LinearOrder α] [LinearOrder β] [Countable α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] [Nonempty α] [Countable β] [DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β] [Nonempty β] : Nonempty (α ≃o β)

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