Documentation

Mathlib.Order.CountableDenseLinearOrder

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 : Finset α) (hi : Finset α) (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) [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
Instances For
    Equations
    instance Order.PartialIso.instPreorder (α : Type u_1) (β : Type u_2) [LinearOrder α] [LinearOrder β] :
    Equations
    theorem Order.PartialIso.exists_across {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] [DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β] [Nonempty β] (f : Order.PartialIso α β) (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} [LinearOrder α] [LinearOrder β] :

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

    Equations
    Instances For

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

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

              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.