feat: endow Simplicity with the Scott-Hausdorff topology

CombinatorialGames.lean

@@ -1,4 +1,4 @@
-module  -- shake: keep-all
+module  -- shake: keep-all --deprecated_module: ignore
 
 public import CombinatorialGames.Counterexamples.Multiplication
 public import CombinatorialGames.Game.Basic
@@ -28,6 +28,7 @@ public import CombinatorialGames.Mathlib.Small
 public import CombinatorialGames.Mathlib.WithTop
 public import CombinatorialGames.NatOrdinal.Basic
 public import CombinatorialGames.NatOrdinal.Pow
+public import CombinatorialGames.NatOrdinal.Topology
 public import CombinatorialGames.Nimber.Basic
 public import CombinatorialGames.Nimber.Field
 public import CombinatorialGames.Nimber.Nat
@@ -37,6 +38,7 @@ public import CombinatorialGames.Nimber.SimplestExtension.Closure
 public import CombinatorialGames.Nimber.SimplestExtension.Polynomial
 public import CombinatorialGames.SignExpansion.Basic
 public import CombinatorialGames.SignExpansion.Simplicity
+public import CombinatorialGames.SignExpansion.Topology
 public import CombinatorialGames.Surreal.Basic
 public import CombinatorialGames.Surreal.Birthday.Basic
 public import CombinatorialGames.Surreal.Birthday.Cut

CombinatorialGames/NatOrdinal/Topology.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2026 Violeta Hernández Palacios. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Violeta Hernández Palacios
+-/
+module
+
+public import CombinatorialGames.NatOrdinal.Basic
+public import Mathlib.Topology.Order.Basic
+
+/-!
+# Topology on ordinals
+
+We endow `NatOrdinal` and `WithTop NatOrdinal` with the order topology.
+-/
+
+public section
+
+instance : TopologicalSpace NatOrdinal := Preorder.topology _
+instance : OrderTopology NatOrdinal := ⟨rfl⟩
+instance : TopologicalSpace (WithTop NatOrdinal) := Preorder.topology _
+instance : OrderTopology (WithTop NatOrdinal) := ⟨rfl⟩
+
+end

CombinatorialGames/SignExpansion/Basic.lean

@@ -211,6 +211,15 @@ theorem small_iff_exists_eq_zero {x : SignExpansion} : Small x ↔ ∃ o, x o =
 instance : Neg SignExpansion where
   neg e := ⟨-e, by simpa using e.2⟩
 
+@[simp]
+theorem length_eq_zero {x : SignExpansion} : x.length = 0 ↔ x = 0 := by
+  refine ⟨fun hx ↦ ?_, ?_⟩
+  · ext i
+    rw [zero_apply, apply_eq_zero, hx]
+    exact zero_le
+  · rintro rfl
+    simp
+
 @[simp] theorem coe_neg (x : SignExpansion) : ⇑(-x : SignExpansion) = -⇑x := rfl
 theorem neg_apply (x : SignExpansion) (o : NatOrdinal) : (-x) o = -x o := rfl
 @[simp] theorem neg_mk (f h) : -mk f h = mk (-f) (by simpa) := rfl

CombinatorialGames/SignExpansion/Simplicity.lean

@@ -62,20 +62,26 @@ def Simplicity : Type _ := SignExpansion
 deriving Inhabited
 
 namespace Simplicity
+open Order Set
 
 /-- The identity function between `SignExpansion` and `Simplicity`. -/
 def of : SignExpansion ≃ Simplicity := Equiv.refl _
 
 /-- The identity function between `Simplicity` and `SignExpansion`. -/
 def val : Simplicity ≃ SignExpansion := Equiv.refl _
 
+@[simp, grind =] theorem symm_of : of.symm = val := rfl
+@[simp, grind =] theorem symm_val : val.symm = of := rfl
+
 @[simp, grind =] theorem of_val (x) : of (val x) = x := rfl
 @[simp, grind =] theorem val_of (x) : val (of x) = x := rfl
 
 instance : Bot Simplicity := ⟨of 0⟩
 
 @[simp, grind =] theorem of_zero : of 0 = ⊥ := rfl
 @[simp, grind =] theorem val_bot : val ⊥ = 0 := rfl
+@[simp] theorem val_eq_zero {x} : val x = 0 ↔ x = ⊥ := .rfl
+@[simp] theorem of_eq_bot {x} : of x = ⊥ ↔ x = 0 := .rfl
 
 instance : FunLike Simplicity NatOrdinal SignType where
   coe x := x.val
@@ -108,8 +114,27 @@ instance : Preorder Simplicity where
   le_trans x y z := by grind
 
 theorem le_def {x y : Simplicity} : x ≤ y ↔ y.val ↾ x.val.length = x.val := .rfl
+
 theorem of_le_of {x y} : of x ≤ of y ↔ y ↾ x.length = x := .rfl
 
+instance : OrderBot Simplicity where
+  bot_le := by simp [le_def]
+
+theorem eq_or_length_lt_of_le {x y : Simplicity} (h : x ≤ y) :
+    x = y ∨ x.val.length < y.val.length := by
+  rw [le_def] at h
+  have := lt_or_ge x.val.length y.val.length
+  aesop
+
+theorem length_strictMono : StrictMono fun x : Simplicity ↦ x.val.length :=
+  fun _ _ h ↦ (eq_or_length_lt_of_le h.le).resolve_left h.ne
+
+instance : PartialOrder Simplicity where
+  le_antisymm x y h₁ h₂ := by
+    have := eq_or_length_lt_of_le h₁
+    have := eq_or_length_lt_of_le h₂
+    grind
+
 theorem le_restrict_of_le_of_length_le {x y : Simplicity} {o : WithTop NatOrdinal}
     (h : x ≤ y) (h' : x.val.length ≤ o) : x ≤ of (val y ↾ o) := by
   simp_all [le_def]
@@ -136,31 +161,57 @@ theorem le_of_le_of_length_le {x y z : Simplicity} (hx : x ≤ z) (hy : y ≤ z)
   rw [← val_apply, apply_ne_zero] at ho ⊢
   exact ho.trans_le h
 
+theorem lt_of_le_of_length_lt {x y z : Simplicity} (hx : x ≤ z) (hy : y ≤ z)
+    (h : x.val.length < y.val.length) : x < y := by
+  apply (le_of_le_of_length_le hx hy h.le).lt_of_ne
+  apply_fun fun a ↦ a.val.length
+  exact h.ne
+
+theorem of_restrict_le (x : Simplicity) (o : WithTop NatOrdinal) : of (x.val ↾ o) ≤ x := by
+  rw [le_def, val_of, length_restrict, ← restrict_restrict_eq, restrict_of_length_le le_rfl]
+
+theorem of_restrict_lt {x : Simplicity} {o : WithTop NatOrdinal} (hx : o < x.val.length) :
+    of (x.val ↾ o) < x := by
+  apply (of_restrict_le x o).lt_of_ne
+  apply_fun fun y ↦ y.val.length
+  simpa
+
 theorem le_or_ge_of_le {x y z : Simplicity} (hx : x ≤ z) (hy : y ≤ z) : x ≤ y ∨ y ≤ x := by
   obtain h | h := le_total x.val.length y.val.length
   · exact .inl <| le_of_le_of_length_le hx hy h
   · exact .inr <| le_of_le_of_length_le hy hx h
 
-theorem of_restrict_le_of (x : SignExpansion) (o : WithTop NatOrdinal) : of (x ↾ o) ≤ of x := by
-  rw [of_le_of, length_restrict, ← restrict_restrict_eq, restrict_of_length_le le_rfl]
-
-theorem eq_or_length_lt_of_le {x y : Simplicity} (h : x ≤ y) :
-    x = y ∨ x.val.length < y.val.length := by
-  rw [le_def] at h
-  have := lt_or_ge x.val.length y.val.length
-  aesop
-
-theorem length_strictMono : StrictMono fun x : Simplicity ↦ x.val.length :=
-  fun _ _ h ↦ (eq_or_length_lt_of_le h.le).resolve_left h.ne
-
-instance : PartialOrder Simplicity where
-  le_antisymm x y h₁ h₂ := by
-    have := eq_or_length_lt_of_le h₁
-    have := eq_or_length_lt_of_le h₂
-    grind
-
-instance : OrderBot Simplicity where
-  bot_le := by simp [le_def]
+theorem lt_or_ge_of_le {x y z : Simplicity} (hx : x ≤ z) (hy : y ≤ z) : x < y ∨ y ≤ x := by
+  obtain rfl | hxy := eq_or_ne x y
+  · simp
+  · obtain h | h := le_or_ge_of_le hx hy
+    · exact .inl <| h.lt_of_ne hxy
+    · exact .inr h
+
+theorem le_or_gt_of_le {x y z : Simplicity} (hx : x ≤ z) (hy : y ≤ z) : x ≤ y ∨ y < x :=
+  (lt_or_ge_of_le hy hx).symm
+
+theorem Iic_sdiff_Iic {x y : Simplicity} (h : x ≤ y) : Iic y \ Iic x = Ioc x y := by
+  apply subset_antisymm
+  · exact fun z ⟨hzy, hzx⟩ ↦ ⟨(lt_or_ge_of_le h hzy).resolve_right hzx, hzy⟩
+  · grind
+
+theorem isSuccPrelimit_iff {x : Simplicity} : IsSuccPrelimit x ↔ IsSuccPrelimit x.val.length := by
+  constructor <;> intro hx y hy
+  · refine hx (of <| val x ↾ y) ⟨of_restrict_lt hy.lt, fun z hz hz' ↦ ?_⟩
+    apply @hy.2 z.val.length
+    · convert length_strictMono hz
+      simpa using hy.le
+    · exact length_strictMono hz'
+  · refine hx y.val.length ⟨length_strictMono hy.lt, fun i hi hi' ↦ ?_⟩
+    apply @hy.2 (of <| val x ↾ i)
+    · apply lt_of_le_of_length_lt hy.le (of_restrict_le ..)
+      convert hi
+      simpa using hi'.le
+    · exact of_restrict_lt hi'
+
+theorem isSuccLimit_iff {x : Simplicity} : IsSuccLimit x ↔ IsSuccLimit x.val.length := by
+  simp [Order.isSuccLimit_iff, isSuccPrelimit_iff, bot_eq_zero]
 
 /-! ### Infimum -/
 
@@ -192,7 +243,7 @@ private theorem sInf_eq_of_mem {s : Set Simplicity} {x : Simplicity} (hx : x ∈
 theorem isGLB_sInf_of_nonempty {s : Set Simplicity} (hs : s.Nonempty) : IsGLB s (sInf s) := by
   constructor <;> intro x hx
   · rw [sInf_eq_of_mem hx]
-    exact of_restrict_le_of ..
+    exact of_restrict_le ..
   · obtain ⟨y, hy⟩ := hs
     rw [sInf_eq_of_mem hy]
     apply le_restrict_of_le_of_length_le (hx hy)
@@ -219,7 +270,7 @@ instance : SupSet Simplicity where
     of ⟨fun i ↦ if h : ∃ x ∈ s, x i ≠ 0 then h.choose i else 0, ?_⟩ else ⊥
 where finally
   intro a b h
-  simp only [Set.mem_preimage, Set.mem_singleton_iff, dite_eq_right_iff,
+  simp only [mem_preimage, Set.mem_singleton_iff, dite_eq_right_iff,
     forall_exists_index, forall_and_index]
   refine fun H x hx hb ↦ isUpperSet_preimage_singleton_zero _ h ?_
   have := H x hx ?_
@@ -271,17 +322,58 @@ theorem isLUB_sSup_iff_bddAbove {s : Set Simplicity} : IsLUB s (sSup s) ↔ BddA
 
 alias ⟨_, isLUB_sSup_of_bddAbove⟩ := isLUB_sSup_iff_bddAbove
 
+protected theorem le_sSup {s : Set Simplicity} {x : Simplicity} (hx : x ∈ s) (hs : BddAbove s) :
+    x ≤ sSup s :=
+  (isLUB_sSup_of_bddAbove hs).1 hx
+
+protected theorem sSup_le {s : Set Simplicity} {x : Simplicity} (hx : x ∈ upperBounds s) :
+    sSup s ≤ x :=
+  (isLUB_sSup_of_bddAbove ⟨x, hx⟩).2 hx
+
 theorem sSup_of_not_bddAbove {s : Set Simplicity} (hs : ¬ BddAbove s) : sSup s = ⊥ := by
   apply dif_neg
   rwa [isChain_iff_bddAbove]
 
+theorem sSup_mono {s t : Set Simplicity} (hst : s ⊆ t) (ht : BddAbove t) : sSup s ≤ sSup t :=
+  Simplicity.sSup_le <| upperBounds_mono_set hst (isLUB_sSup_of_bddAbove ht).1
+
+theorem length_sSup {s : Set Simplicity} (hs : BddAbove s) :
+    (sSup s).val.length = sSup ((·.val.length) '' s) := by
+  apply le_antisymm
+  · apply le_of_forall_lt
+    simp only [WithTop.forall, not_top_lt, imp_self, true_and]
+    intro y hy
+    obtain ⟨z, hz, hz'⟩ :=
+      exists_of_sSup_apply_ne_zero (isChain_iff_bddAbove.2 hs) (apply_ne_zero.2 hy)
+    rw [← val_apply, apply_ne_zero] at hz'
+    apply hz'.trans_le (le_sSup _)
+    exact ⟨z, hz, rfl⟩
+  · rw [sSup_le_iff]
+    rintro _ ⟨x, hx, rfl⟩
+    exact length_strictMono.monotone (Simplicity.le_sSup hx hs)
+
+theorem sSup_Iic (x : Simplicity) : sSup (Iic x) = x :=
+  (isLUB_sSup_of_bddAbove bddAbove_Iic).unique isLUB_Iic
+
+theorem sSup_Iio_of_isSuccLimit {x : Simplicity} (hx : Order.IsSuccLimit x) :
+    sSup (Iio x) = x := by
+  have hx' := (sSup_mono Iio_subset_Iic_self bddAbove_Iic).trans_eq <| sSup_Iic x
+  apply hx'.antisymm (le_of_le_of_length_le le_rfl hx' _)
+  rw [length_sSup bddAbove_Iio]
+  refine le_of_forall_lt fun i hi ↦ ?_
+  rw [(isSuccLimit_iff.1 hx).lt_iff_exists_lt] at hi
+  obtain ⟨j, hj, hij⟩ := hi
+  apply hij.trans_le (le_sSup _)
+  refine ⟨_, of_restrict_lt hj, ?_⟩
+  simpa using hj.le
+
 instance : Max Simplicity where
   max x y := sSup {x, y}
 
 theorem sSup_pair (x y : Simplicity) : sSup {x, y} = x ⊔ y := rfl
 
 protected theorem sup_comm (x y : Simplicity) : x ⊔ y = y ⊔ x :=
-  congrArg sSup <| Set.pair_comm x y
+  congrArg sSup <| pair_comm x y
 
 protected theorem sup_of_le_right {x y : Simplicity} (h : x ≤ y) : x ⊔ y = y := by
   apply (isLUB_sSup_of_bddAbove ?_).unique