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

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.

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
@[protected, instance]
Equations
@[protected, instance]
Equations
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.

@[protected]
noncomputable 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

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

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
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
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

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

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