mathlib documentation

order.countable_dense_linear_order

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 isomorhpism α ≃ β.

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} [linear_order α] [densely_ordered α] [no_bot_order α] [no_top_order α] [nonem : nonempty α] (lo hi : finset α) (lo_lt_hi : ∀ (x : α), x lo∀ (y : α), y hix < y) :
∃ (m : α), (∀ (x : α), x lox < m) ∀ (y : α), y him < 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.

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
@[instance]
def order.partial_iso.inhabited (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] :
Equations
@[instance]
def order.partial_iso.preorder (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] :
Equations
theorem order.partial_iso.exists_across {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] [densely_ordered β] [no_bot_order β] [no_top_order β] [nonempty β] (f : order.partial_iso α β) (a : α) :
∃ (b : β), ∀ (p : α × β), p f.valcmp 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.

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

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

Equations
def order.partial_iso.defined_at_left {α : Type u_1} (β : Type u_2) [linear_order α] [linear_order β] [densely_ordered β] [no_bot_order β] [no_top_order β] [nonempty β] (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
def order.partial_iso.defined_at_right (α : Type u_1) {β : Type u_2} [linear_order α] [linear_order β] [densely_ordered α] [no_bot_order α] [no_top_order α] [nonempty α] (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
def order.partial_iso.fun_of_ideal {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] [densely_ordered β] [no_bot_order β] [no_top_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 q : α × β), p fq fcmp 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
def order.partial_iso.inv_of_ideal {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] [densely_ordered α] [no_bot_order α] [no_top_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 q : α × β), p fq fcmp 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
def order.embedding_from_countable_to_dense (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] [encodable α] [densely_ordered β] [no_bot_order β] [no_top_order β] [nonempty β] :
α ↪o β

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

Equations
def order.iso_of_countable_dense (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] [encodable α] [densely_ordered α] [no_bot_order α] [no_top_order α] [nonempty α] [encodable β] [densely_ordered β] [no_bot_order β] [no_top_order β] [nonempty β] :
α ≃o β

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

Equations