mathlib documentation

set_theory.surreal

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, and these relations satisfy the axioms of a partial order (recall that x < y ↔ x ≤ y ∧ ¬ y ≤ x did not hold for games).

Algebraic operations #

At this point, we have defined addition and negation (from pregames), and shown that surreals form an additive semigroup. It would be very little work to finish showing that the surreals form an ordered commutative group.

We define the operations of multiplication and inverse on surreals, but do not yet establish any of the necessary properties to show the surreals form an ordered field.

Embeddings #

It would be nice projects to define the group homomorphism surreal → game, and also ℤ → surreal, and then the homomorphic inclusion of the dyadic rationals into surreals, and finally via dyadic Dedekind cuts the homomorphic inclusion of the reals into the surreals.

One can also map all the ordinals into the surreals!

References #

Multiplicative operations can be defined at the level of pre-games, but as they are only useful on surreal numbers, we define them here.

source
def pgame.mul (x : pgame) (y : pgame) :
pgame

The product of x = {xL | xR} and y = {yL | yR} is {xL*y + x*yL - xL*yL, xR*y + x*yR - xR*yR | xL*y + x*yR - xL*yR, x*yL + xR*y - xR*yL }.

Equations
  • x.mul y = pgame.rec (λ (xl xr : Type u_1) (xL : xl → pgame) (xR : xr → pgame) (IHxl : Π (ᾰ : xl), (λ (x : pgame), pgame → pgame) (xL ᾰ)) (IHxr : Π (ᾰ : xr), (λ (x : pgame), pgame → pgame) (xR ᾰ)) (y : pgame), pgame.rec (λ (yl yr : Type u_2) (yL : yl → pgame) (yR : yr → pgame) (IHyl : Π (ᾰ : yl), (λ (y : pgame), pgame) (yL ᾰ)) (IHyr : Π (ᾰ : yr), (λ (y : pgame), pgame) (yR ᾰ)), pgame.mk (xl × yl ⊕ xr × yr) (xl × yr ⊕ xr × yl) (λ (ᾰ : xl × yl ⊕ xr × yr), ᾰ.cases_on (λ (ᾰ : xl × yl), ᾰ.cases_on (λ (i : xl) (j : yl), IHxl i (pgame.mk yl yr yL yR) + IHyl j - IHxl i (yL j))) (λ (ᾰ : xr × yr), ᾰ.cases_on (λ (i : xr) (j : yr), IHxr i (pgame.mk yl yr yL yR) + IHyr j - IHxr i (yR j)))) (λ (ᾰ : xl × yr ⊕ xr × yl), ᾰ.cases_on (λ (ᾰ : xl × yr), ᾰ.cases_on (λ (i : xl) (j : yr), IHxl i (pgame.mk yl yr yL yR) + IHyr j - IHxl i (yR j))) (λ (ᾰ : xr × yl), ᾰ.cases_on (λ (i : xr) (j : yl), IHxr i (pgame.mk yl yr yL yR) + IHyl j - IHxr i (yL j))))) y) x y
source
@[protected, instance]
def pgame.has_mul  :
has_mul pgame
Equations
source
def pgame.left_moves_mul (x y : pgame) :
(x * y).left_moves ≃ x.left_moves × y.left_moves ⊕ x.right_moves × y.right_moves

An explicit description of the moves for Left in x * y.

Equations
source
def pgame.right_moves_mul (x y : pgame) :
(x * y).right_moves ≃ x.left_moves × y.right_moves ⊕ x.right_moves × y.left_moves

An explicit description of the moves for Right in x * y.

Equations
source
@[simp]
theorem pgame.mk_mul_move_left_inl {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xl} {j : yl} :
((pgame.mk xl xr xL xR) * pgame.mk yl yr yL yR).move_left (sum.inl (i, j)) = (xL i) * pgame.mk yl yr yL yR + (pgame.mk xl xr xL xR) * yL j - (xL i) * yL j
source
@[simp]
theorem pgame.mul_move_left_inl {x y : pgame} {i : x.left_moves} {j : y.left_moves} :
(x * y).move_left (⇑((x.left_moves_mul y).symm) (sum.inl (i, j))) = (x.move_left i) * y + x * y.move_left j - (x.move_left i) * y.move_left j
source
@[simp]
theorem pgame.mk_mul_move_left_inr {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xr} {j : yr} :
((pgame.mk xl xr xL xR) * pgame.mk yl yr yL yR).move_left (sum.inr (i, j)) = (xR i) * pgame.mk yl yr yL yR + (pgame.mk xl xr xL xR) * yR j - (xR i) * yR j
source
@[simp]
theorem pgame.mul_move_left_inr {x y : pgame} {i : x.right_moves} {j : y.right_moves} :
(x * y).move_left (⇑((x.left_moves_mul y).symm) (sum.inr (i, j))) = (x.move_right i) * y + x * y.move_right j - (x.move_right i) * y.move_right j
source
@[simp]
theorem pgame.mk_mul_move_right_inl {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xl} {j : yr} :
((pgame.mk xl xr xL xR) * pgame.mk yl yr yL yR).move_right (sum.inl (i, j)) = (xL i) * pgame.mk yl yr yL yR + (pgame.mk xl xr xL xR) * yR j - (xL i) * yR j
source
@[simp]
theorem pgame.mul_move_right_inl {x y : pgame} {i : x.left_moves} {j : y.right_moves} :
(x * y).move_right (⇑((x.right_moves_mul y).symm) (sum.inl (i, j))) = (x.move_left i) * y + x * y.move_right j - (x.move_left i) * y.move_right j
source
@[simp]
theorem pgame.mk_mul_move_right_inr {xl xr yl yr : Type u_1} {xL : xl → pgame} {xR : xr → pgame} {yL : yl → pgame} {yR : yr → pgame} {i : xr} {j : yl} :
((pgame.mk xl xr xL xR) * pgame.mk yl yr yL yR).move_right (sum.inr (i, j)) = (xR i) * pgame.mk yl yr yL yR + (pgame.mk xl xr xL xR) * yL j - (xR i) * yL j
source
@[simp]
theorem pgame.mul_move_right_inr {x y : pgame} {i : x.right_moves} {j : y.left_moves} :
(x * y).move_right (⇑((x.right_moves_mul y).symm) (sum.inr (i, j))) = (x.move_right i) * y + x * y.move_left j - (x.move_right i) * y.move_left j
source
def pgame.add_sub_relabelling {a b c x y z : pgame} (h₁ : a.relabelling x) (h₂ : b.relabelling y) (h₃ : c.relabelling z) :
(a + b - c).relabelling (x + y - z)

If a has the same moves as x, b has the same moves as y, and c has the same moves as z, then a + b - c has the same moves as x + y - z. This lemma is repeatedly used for simplifying multiplication of surreal numbers.

Equations
source
def pgame.add_comm_sub_relabelling {a b c x y z : pgame} (h₁ : a.relabelling x) (h₂ : b.relabelling y) (h₃ : c.relabelling z) :
(a + b - c).relabelling (y + x - z)

If a has the same moves as x, b has the same moves as y, and c has the same moves as z, then a + b - c has the same moves as y + x - z. This lemma is repeatedly used for simplifying multiplication of surreal numbers.

Equations
source
def pgame.mul_comm_relabelling (x y : pgame) :
(x * y).relabelling (y * x)

x * y has exactly the same moves as y * x.

Equations
source
theorem pgame.mul_comm_equiv (x y : pgame) :
(x * y).equiv (y * x)

x * y is equivalent to y * x.

source
def pgame.mul_zero_relabelling (x : pgame) :
(x * 0).relabelling 0

x * 0 has exactly the same moves as 0.

Equations
source
theorem pgame.mul_zero_equiv (x : pgame) :
(x * 0).equiv 0

x * 0 is equivalent to 0.

source
def pgame.zero_mul_relabelling (x : pgame) :
(0 * x).relabelling 0

0 * x has exactly the same moves as 0.

Equations
source
theorem pgame.zero_mul_equiv (x : pgame) :
(0 * x).equiv 0

0 * x is equivalent to 0.

source
inductive pgame.inv_ty (l r : Type u) :
bool → Type u

Because the two halves of the definition of inv produce more elements of each side, we have to define the two families inductively. This is the indexing set for the function, and inv_val is the function part.

source
def pgame.inv_val {l r : Type u_1} (L : l → pgame) (R : r → pgame) (IHl : l → pgame) (IHr : r → pgame) {b : bool} :
pgame.inv_ty l r b → pgame

Because the two halves of the definition of inv produce more elements of each side, we have to define the two families inductively. This is the function part, defined by recursion on inv_ty.

Equations
source
def pgame.inv'  :
pgame → pgame

The inverse of a positive surreal number x = {L | R} is given by x⁻¹ = {0, (1 + (R - x) * x⁻¹L) * R, (1 + (L - x) * x⁻¹R) * L | (1 + (L - x) * x⁻¹L) * L, (1 + (R - x) * x⁻¹R) * R}. Because the two halves x⁻¹L, x⁻¹R of x⁻¹ are used in their own definition, the sets and elements are inductively generated.

Equations
source
def pgame.inv (x : pgame) :
pgame

The inverse of a surreal number in terms of the inverse on positive surreals.

Equations
source
@[protected, instance]
def pgame.has_inv  :
has_inv pgame
Equations
source
@[protected, instance]
def pgame.has_div  :
has_div pgame
Equations
source
def pgame.numeric  :
pgame → Prop

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
source
theorem pgame.numeric.move_left {x : pgame} (o : x.numeric) (i : x.left_moves) :
(x.move_left i).numeric
source
theorem pgame.numeric.move_right {x : pgame} (o : x.numeric) (j : x.right_moves) :
(x.move_right j).numeric
source
theorem pgame.numeric_rec {C : pgame → Prop} (H : ∀ (l r : Type u_1) (L : l → pgame) (R : r → 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 (pgame.mk l r L R)) (x : pgame) :
x.numeric → C x
source
theorem pgame.lt_asymm {x y : pgame} (ox : x.numeric) (oy : y.numeric) :
x < y → ¬y < x
source
theorem pgame.le_of_lt {x y : pgame} (ox : x.numeric) (oy : y.numeric) (h : x < y) :
x ≤ y
source
theorem pgame.lt_iff_le_not_le {x y : pgame} (ox : x.numeric) (oy : y.numeric) :
x < y ↔ x ≤ y ∧ ¬y ≤ x

On numeric pre-games, < and ≤ satisfy the axioms of a partial order (even though they don't on all pre-games).

source
theorem pgame.numeric_zero  :
0.numeric
source
theorem pgame.numeric_one  :
1.numeric
source
theorem pgame.numeric_neg {x : pgame} (o : x.numeric) :
(-x).numeric
source
theorem pgame.numeric.move_left_lt {x : pgame} (o : x.numeric) (i : x.left_moves) :
x.move_left i < x
source
theorem pgame.numeric.move_left_le {x : pgame} (o : x.numeric) (i : x.left_moves) :
x.move_left i ≤ x
source
theorem pgame.numeric.lt_move_right {x : pgame} (o : x.numeric) (j : x.right_moves) :
x < x.move_right j
source
theorem pgame.numeric.le_move_right {x : pgame} (o : x.numeric) (j : x.right_moves) :
x ≤ x.move_right j
source
theorem pgame.add_lt_add {w x y z : pgame} (ow : w.numeric) (ox : x.numeric) (oy : y.numeric) (oz : z.numeric) (hwx : w < x) (hyz : y < z) :
w + y < x + z
source
theorem pgame.numeric_add {x y : pgame} (ox : x.numeric) (oy : y.numeric) :
(x + y).numeric
source
theorem pgame.numeric_nat (n : ℕ) :
↑n.numeric

Pre-games defined by natural numbers are numeric.

source
theorem pgame.numeric_omega  :
pgame.omega.numeric

The pre-game omega is numeric.

source
def surreal.equiv (x y : {x // x.numeric}) :
Prop

The equivalence on numeric pre-games.

Equations
source
@[protected, instance]
def surreal.setoid  :
setoid {x // x.numeric}
Equations
source
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
source
def surreal.mk (x : pgame) (h : x.numeric) :
surreal

Construct a surreal number from a numeric pre-game.

Equations
source
@[protected, instance]
def surreal.has_zero  :
has_zero surreal
Equations
source
@[protected, instance]
def surreal.has_one  :
has_one surreal
Equations
source
@[protected, instance]
def surreal.inhabited  :
inhabited surreal
Equations
source
def surreal.lift {α : Sort u_1} (f : Π (x : pgame), x.numeric → α) (H : ∀ {x y : pgame} (hx : x.numeric) (hy : y.numeric), x.equiv y → f x hx = f y hy) :
surreal → α

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

Equations
source
def surreal.lift₂ {α : Sort u_1} (f : Π (x : pgame) (y : pgame), x.numeric → y.numeric → α) (H : ∀ {x₁ : pgame} {y₁ : pgame} {x₂ : pgame} {y₂ : 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₂) :
surreal → surreal → α

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

Equations
source
def surreal.le  :
surreal → surreal → Prop

The relation x ≤ y on surreals.

Equations
source
def surreal.lt  :
surreal → surreal → Prop

The relation x < y on surreals.

Equations
source
theorem surreal.not_le {x y : surreal} :
¬x.le y ↔ y.lt x
source
def surreal.add  :
surreal → surreal → surreal

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
source
def surreal.neg  :
surreal → surreal

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

Equations
source
@[protected, instance]
def surreal.has_le  :
has_le surreal
Equations
source
@[protected, instance]
def surreal.has_lt  :
has_lt surreal
Equations
source
@[protected, instance]
def surreal.has_add  :
has_add surreal
Equations
source
@[protected, instance]
def surreal.has_neg  :
has_neg surreal
Equations
source
@[protected, instance]
def surreal.ordered_add_comm_group  :
ordered_add_comm_group surreal
Equations
source
@[protected, instance]
def surreal.linear_ordered_add_comm_group  :
linear_ordered_add_comm_group surreal
Equations