Long line & ordinals

[Columbus240]

I’d like to add some examples of (pathological) topological spaces to the library. For the long line I need the following:

• Order Topology (already in the library)
• Lexicographic order on the product of two orders (haven’t found it yet, if it’s already formalised)
• The first uncountable ordinal ω_1.

I’m currently struggling with the definition of ω_1. Wikipedia gives Hartog numbers as slight hint. But my problem is not conceptual, in understanding the mathematics, but in the formalisation in Coq.
I’d like to use the Ordinal and well_founded definitions from Ordinals.v and WellOrders.v, but well_founded demands forall a b, a < b \/ a = b \/ a > b, while we can only prove forall a b : Ordinal, a < b \/ a == b \/ a > b. So the theorems of WellOrders.v remain unavailable for the Ordinal type. Interestingly, == isn’t extensional for Ordinal; for it is possible to prove ~ forall a b : Ordinal, a == b -> a = b.
I see three possible ways to continue:

• Redefine the Ordinal type, so a == b -> a = b holds. That actually looks rather difficult, since we can’t easily take quotients. Maybe Induction-Induction would lead to a suitable definition, but currently that needs axioms, which isn’t very satisfying.
• Redefine the well_founded definition (specifically total_strict_order) so it is only up-to-equivalence. I.e. use Setoids. But since the rest of the library avoids using Setoids, I don’t want to introduce them here.
• Do the work I wanted to do with the Ordinal type, on the type of well_founded relations. Using a bundled structure (i.e. a Record WF_Type := { carrier : T; R : relation T; wf : well_founded R }.) might simplify the work, because always carrying T and R around is a bit annoying. It would be necessary to show that WF_Type is itself a well_founded type, then we could (probably) carry out the construction of ω_1. And the layered universes will probably make sure that no paradox arises.

We might want to add more theory about ordinals, like ordinal arithmetic. But hopefully with an ordinal type where a <= b -> a => b -> a = b.

P.S.: The proof that == is not extensional. We might want to add this to the library, as a reminder that == isn’t nice enough. The trick of the proof is to notice, that ord_sup isn’t injective with respect to ==. The term ord_sup (fun H:False => match H return Ordinal with end) corresponds to the ordinal zero.

Lemma ord_eq_not_extensional :
  ~ forall a b : Ordinal, a == b -> a = b.
Proof.
  intro.
  pose (a := (ord_sup (fun H:False => match H return Ordinal with end))).
  pose (b := (ord_sup (fun _:True=> (ord_sup (fun H:False => match H return Ordinal with end))))).
  assert (a == b).
  { unfold a, b.
    repeat constructor; intros; contradiction.
  }
  specialize (H a b H0).
  unfold a, b in *.
  inversion H.
  pose proof I.
  destruct H2.
  assumption.
Qed.

[Columbus240]

I haven’t yet looked at other libraries and how they formalise ordinals. Might be worth it.

[palmskog]

For reference, here are some formalizations of topology/ordinals in proof assistants, which might be useful since you already assume classical logic:

• Coq+MathComp
• HOL Light
• Isabelle/HOL
• Lean

[Columbus240]

Thanks for the reading material.

I noticed today, that the file Quotients.v exists. Well, that might be useful.

[Columbus240]

I came up with an easier way to describe the long line. I can introduce the first uncountable ordinal as a hypothesis, without giving an explicit construction. This way we can avoid intricate constructions and universe incompatibilities.
The following snippet is a starting point:

From ZornsLemma Require Import CountableTypes WellOrders.

From Coq Require Import Relation_Operators.

From Topology Require Import RTopology.

Definition ho_unit_interval :=
  [z : RTop | 0 <= z < 1].

(* It is a bit clunky to work with the construction of the long line.
   Can we work with it axiomatically? Would that be easier?
   (i.e. list some properties such that every space satisfying these
   properties is homeomorphic to some canonical construction of the
   long line.)
*)

Section LongLine.
  (* Assume, that [Omega] is the first uncountable
  ordinal. Independent of its actual construction, we are only
  interested in this property. *)
  Variable Omega : Type.
  Variable lt :
    relation Omega.
  Variable Omega_well_ordered :
    well_order lt.
  Hypothesis Omega_Uncountable : ~CountableT Omega.
  (* [Omega] is the least uncountable ordinal. I.e. it can be order-embedded into all other uncountable ordinals. *)
  Hypothesis Omega_minimal :
    forall (X : Type) (R : relation X),
      well_order R ->
      ~CountableT X ->
      exists f : Omega -> X,
        forall x y,
          lt x y <->
          R (f x) (f y).

  Definition clr_le : relation _ :=
      (lexprod
         (SubspaceTopology ho_unit_interval)
         (fun _ => Omega)
         (fun x y =>
            Rle (proj1_sig x)
                (proj1_sig y))
         (fun _ x y =>
            x = y \/
            lt x y)).

  Definition closed_long_ray :=
    OrderTopology clr_le.
End LongLine.