Documentation

Mathlib.SetTheory.Surreal.Basic

Surreal numbers #

The basic theory of surreal numbers, built on top of the theory of combinatorial (pre-)games.

A pregame is Numeric if all the Left options are strictly smaller than all the Right options, and all those options are themselves numeric. In terms of combinatorial games, the numeric games have "frozen"; you can only make your position worse by playing, and Left is some definite "number" of moves ahead (or behind) Right.

A surreal number is an equivalence class of numeric pregames.

In fact, the surreals form a complete ordered field, containing a copy of the reals (and much else besides!) but we do not yet have a complete development.

Order properties #

Surreal numbers inherit the relations and < from games (Surreal.instLE and Surreal.instLT), and these relations satisfy the axioms of a partial order.

Algebraic operations #

We show that the surreals form a linear ordered commutative group.

One can also map all the ordinals into the surreals!

Multiplication of surreal numbers #

The proof that multiplication lifts to surreal numbers is surprisingly difficult and is currently missing in the library. A sample proof can be found in Theorem 3.8 in the second reference below. The difficulty lies in the length of the proof and the number of theorems that need to proven simultaneously. This will make for a fun and challenging project.

The branch surreal_mul contains some progress on this proof.

Todo #

References #

A pre-game is numeric if everything in the L set is less than everything in the R set, and all the elements of L and R are also numeric.

Equations
  • (SetTheory.PGame.mk α β L R).Numeric = ((∀ (i : α) (j : β), L i < R j) (∀ (i : α), (L i).Numeric) ∀ (j : β), (R j).Numeric)
Instances For
    theorem SetTheory.PGame.numeric_def {x : SetTheory.PGame} :
    x.Numeric (∀ (i : x.LeftMoves) (j : x.RightMoves), x.moveLeft i < x.moveRight j) (∀ (i : x.LeftMoves), (x.moveLeft i).Numeric) ∀ (j : x.RightMoves), (x.moveRight j).Numeric
    theorem SetTheory.PGame.Numeric.mk {x : SetTheory.PGame} (h₁ : ∀ (i : x.LeftMoves) (j : x.RightMoves), x.moveLeft i < x.moveRight j) (h₂ : ∀ (i : x.LeftMoves), (x.moveLeft i).Numeric) (h₃ : ∀ (j : x.RightMoves), (x.moveRight j).Numeric) :
    x.Numeric
    theorem SetTheory.PGame.Numeric.left_lt_right {x : SetTheory.PGame} (o : x.Numeric) (i : x.LeftMoves) (j : x.RightMoves) :
    x.moveLeft i < x.moveRight j
    theorem SetTheory.PGame.Numeric.moveLeft {x : SetTheory.PGame} (o : x.Numeric) (i : x.LeftMoves) :
    (x.moveLeft i).Numeric
    theorem SetTheory.PGame.Numeric.moveRight {x : SetTheory.PGame} (o : x.Numeric) (j : x.RightMoves) :
    (x.moveRight j).Numeric
    theorem SetTheory.PGame.numeric_rec {C : SetTheory.PGameProp} (H : ∀ (l r : Type u_1) (L : lSetTheory.PGame) (R : rSetTheory.PGame), (∀ (i : l) (j : r), L i < R j)(∀ (i : l), (L i).Numeric)(∀ (i : r), (R i).Numeric)(∀ (i : l), C (L i))(∀ (i : r), C (R i))C (SetTheory.PGame.mk l r L R)) (x : SetTheory.PGame) :
    x.NumericC x
    theorem SetTheory.PGame.Relabelling.numeric_imp {x : SetTheory.PGame} {y : SetTheory.PGame} (r : x.Relabelling y) (ox : x.Numeric) :
    y.Numeric
    theorem SetTheory.PGame.Relabelling.numeric_congr {x : SetTheory.PGame} {y : SetTheory.PGame} (r : x.Relabelling y) :
    x.Numeric y.Numeric

    Relabellings preserve being numeric.

    theorem SetTheory.PGame.lf_asymm {x : SetTheory.PGame} {y : SetTheory.PGame} (ox : x.Numeric) (oy : y.Numeric) :
    x.LF y¬y.LF x
    theorem SetTheory.PGame.le_of_lf {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x.LF y) (ox : x.Numeric) (oy : y.Numeric) :
    x y
    theorem SetTheory.PGame.LF.le {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x.LF y) (ox : x.Numeric) (oy : y.Numeric) :
    x y

    Alias of SetTheory.PGame.le_of_lf.

    theorem SetTheory.PGame.lt_of_lf {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x.LF y) (ox : x.Numeric) (oy : y.Numeric) :
    x < y
    theorem SetTheory.PGame.LF.lt {x : SetTheory.PGame} {y : SetTheory.PGame} (h : x.LF y) (ox : x.Numeric) (oy : y.Numeric) :
    x < y

    Alias of SetTheory.PGame.lt_of_lf.

    theorem SetTheory.PGame.lf_iff_lt {x : SetTheory.PGame} {y : SetTheory.PGame} (ox : x.Numeric) (oy : y.Numeric) :
    x.LF y x < y
    theorem SetTheory.PGame.le_iff_forall_lt {x : SetTheory.PGame} {y : SetTheory.PGame} (ox : x.Numeric) (oy : y.Numeric) :
    x y (∀ (i : x.LeftMoves), x.moveLeft i < y) ∀ (j : y.RightMoves), x < y.moveRight j

    Definition of x ≤ y on numeric pre-games, in terms of <

    theorem SetTheory.PGame.lt_iff_exists_le {x : SetTheory.PGame} {y : SetTheory.PGame} (ox : x.Numeric) (oy : y.Numeric) :
    x < y (∃ (i : y.LeftMoves), x y.moveLeft i) ∃ (j : x.RightMoves), x.moveRight j y

    Definition of x < y on numeric pre-games, in terms of

    theorem SetTheory.PGame.lt_of_exists_le {x : SetTheory.PGame} {y : SetTheory.PGame} (ox : x.Numeric) (oy : y.Numeric) :
    ((∃ (i : y.LeftMoves), x y.moveLeft i) ∃ (j : x.RightMoves), x.moveRight j y)x < y
    theorem SetTheory.PGame.lt_def {x : SetTheory.PGame} {y : SetTheory.PGame} (ox : x.Numeric) (oy : y.Numeric) :
    x < y (∃ (i : y.LeftMoves), (∀ (i' : x.LeftMoves), x.moveLeft i' < y.moveLeft i) ∀ (j : (y.moveLeft i).RightMoves), x < (y.moveLeft i).moveRight j) ∃ (j : x.RightMoves), (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i < y) ∀ (j' : y.RightMoves), x.moveRight j < y.moveRight j'

    The definition of x < y on numeric pre-games, in terms of < two moves later.

    theorem SetTheory.PGame.not_fuzzy {x : SetTheory.PGame} {y : SetTheory.PGame} (ox : x.Numeric) (oy : y.Numeric) :
    ¬x.Fuzzy y
    theorem SetTheory.PGame.lt_or_equiv_or_gt {x : SetTheory.PGame} {y : SetTheory.PGame} (ox : x.Numeric) (oy : y.Numeric) :
    x < y x y y < x
    theorem SetTheory.PGame.numeric_of_isEmpty (x : SetTheory.PGame) [IsEmpty x.LeftMoves] [IsEmpty x.RightMoves] :
    x.Numeric
    theorem SetTheory.PGame.numeric_of_isEmpty_leftMoves (x : SetTheory.PGame) [IsEmpty x.LeftMoves] :
    (∀ (j : x.RightMoves), (x.moveRight j).Numeric)x.Numeric
    theorem SetTheory.PGame.numeric_of_isEmpty_rightMoves (x : SetTheory.PGame) [IsEmpty x.RightMoves] (H : ∀ (i : x.LeftMoves), (x.moveLeft i).Numeric) :
    x.Numeric
    theorem SetTheory.PGame.Numeric.neg {x : SetTheory.PGame} :
    x.Numeric(-x).Numeric
    theorem SetTheory.PGame.Numeric.moveLeft_lt {x : SetTheory.PGame} (o : x.Numeric) (i : x.LeftMoves) :
    x.moveLeft i < x
    theorem SetTheory.PGame.Numeric.moveLeft_le {x : SetTheory.PGame} (o : x.Numeric) (i : x.LeftMoves) :
    x.moveLeft i x
    theorem SetTheory.PGame.Numeric.lt_moveRight {x : SetTheory.PGame} (o : x.Numeric) (j : x.RightMoves) :
    x < x.moveRight j
    theorem SetTheory.PGame.Numeric.le_moveRight {x : SetTheory.PGame} (o : x.Numeric) (j : x.RightMoves) :
    x x.moveRight j
    theorem SetTheory.PGame.Numeric.add {x : SetTheory.PGame} {y : SetTheory.PGame} :
    x.Numericy.Numeric(x + y).Numeric
    theorem SetTheory.PGame.Numeric.sub {x : SetTheory.PGame} {y : SetTheory.PGame} (ox : x.Numeric) (oy : y.Numeric) :
    (x - y).Numeric
    theorem SetTheory.PGame.numeric_nat (n : ) :
    (n).Numeric

    Pre-games defined by natural numbers are numeric.

    theorem SetTheory.PGame.numeric_toPGame (o : Ordinal.{u_1}) :
    o.toPGame.Numeric

    Ordinal games are numeric.

    def Surreal :
    Type (u_1 + 1)

    The type of surreal numbers. These are the numeric pre-games quotiented by the equivalence relation x ≈ y ↔ x ≤ y ∧ y ≤ x. In the quotient, the order becomes a total order.

    Equations
    Instances For
      def Surreal.mk (x : SetTheory.PGame) (h : x.Numeric) :

      Construct a surreal number from a numeric pre-game.

      Equations
      Instances For
        def Surreal.lift {α : Sort u_1} (f : (x : SetTheory.PGame) → x.Numericα) (H : ∀ {x y : SetTheory.PGame} (hx : x.Numeric) (hy : y.Numeric), x.Equiv yf x hx = f y hy) :
        Surrealα

        Lift an equivalence-respecting function on pre-games to surreals.

        Equations
        Instances For
          def Surreal.lift₂ {α : Sort u_1} (f : (x : SetTheory.PGame) → (y : SetTheory.PGame) → x.Numericy.Numericα) (H : ∀ {x₁ : SetTheory.PGame} {y₁ : SetTheory.PGame} {x₂ : SetTheory.PGame} {y₂ : SetTheory.PGame} (ox₁ : x₁.Numeric) (oy₁ : y₁.Numeric) (ox₂ : x₂.Numeric) (oy₂ : y₂.Numeric), x₁.Equiv x₂y₁.Equiv y₂f x₁ y₁ ox₁ oy₁ = f x₂ y₂ ox₂ oy₂) :
          SurrealSurrealα

          Lift a binary equivalence-respecting function on pre-games to surreals.

          Equations
          Instances For
            Equations
            @[simp]
            theorem Surreal.mk_le_mk {x : SetTheory.PGame} {y : SetTheory.PGame} {hx : x.Numeric} {hy : y.Numeric} :
            Equations

            Addition on surreals is inherited from pre-game addition: the sum of x = {xL | xR} and y = {yL | yR} is {xL + y, x + yL | xR + y, x + yR}.

            Equations

            Negation for surreal numbers is inherited from pre-game negation: the negation of {L | R} is {-R | -L}.

            Equations
            Equations
            • One or more equations did not get rendered due to their size.

            Casts a Surreal number into a Game.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem Surreal.zero_toGame :
              Surreal.toGame 0 = 0
              @[simp]
              theorem Surreal.one_toGame :
              Surreal.toGame 1 = 1
              @[simp]
              theorem Surreal.nat_toGame (n : ) :
              Surreal.toGame n = n

              A small family of surreals is bounded above.

              A small set of surreals is bounded above.

              A small family of surreals is bounded below.

              A small set of surreals is bounded below.

              Converts an ordinal into the corresponding surreal.

              Equations
              Instances For