mathlib3 documentation

order.countable_dense_linear_order

The back and forth method and countable dense linear orders #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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
Instances for order.partial_iso
source
@[protected, instance]
def order.partial_iso.inhabited (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] :
inhabited (order.partial_iso α β)
Equations
source
@[protected, instance]
def order.partial_iso.preorder (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] :
preorder (order.partial_iso α β)
Equations
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
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
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
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
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
source
theorem order.embedding_from_countable_to_dense (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] [encodable α] [densely_ordered β] [nontrivial β] :
nonempty (α ↪o β)

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

source
theorem 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 β] :
nonempty (α ≃o β)

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