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
- [Conway, On numbers and games][conway2001]
Multiplicative operations can be defined at the level of pre-games, but as they are only useful on surreal numbers, we define them here.
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 : Π (a : xl), (λ (x : pgame), pgame → pgame) (xL a)) (IHxr : Π (a : xr), (λ (x : pgame), pgame → pgame) (xR a)) (y : pgame), pgame.rec (λ (yl yr : Type u_2) (yL : yl → pgame) (yR : yr → pgame) (IHyl : Π (a : yl), (λ (y : pgame), pgame) (yL a)) (IHyr : Π (a : yr), (λ (y : pgame), pgame) (yR a)), pgame.mk (xl × yl ⊕ xr × yr) (xl × yr ⊕ xr × yl) (λ (a : xl × yl ⊕ xr × yr), a.cases_on (λ (a : xl × yl), a.cases_on (λ (i : xl) (j : yl), IHxl i (pgame.mk yl yr yL yR) + IHyl j - IHxl i (yL j))) (λ (a : xr × yr), a.cases_on (λ (i : xr) (j : yr), IHxr i (pgame.mk yl yr yL yR) + IHyr j - IHxr i (yR j)))) (λ (a : xl × yr ⊕ xr × yl), a.cases_on (λ (a : xl × yr), a.cases_on (λ (i : xl) (j : yr), IHxl i (pgame.mk yl yr yL yR) + IHyr j - IHxl i (yR j))) (λ (a : xr × yl), a.cases_on (λ (i : xr) (j : yl), IHxr i (pgame.mk yl yr yL yR) + IHyl j - IHxr i (yL j))))) y) x y
- zero : Π (l r : Type u), pgame.inv_ty l r bool.ff
- left₁ : Π (l r : Type u), r → pgame.inv_ty l r bool.ff → pgame.inv_ty l r bool.ff
- left₂ : Π (l r : Type u), l → pgame.inv_ty l r bool.tt → pgame.inv_ty l r bool.ff
- right₁ : Π (l r : Type u), l → pgame.inv_ty l r bool.ff → pgame.inv_ty l r bool.tt
- right₂ : Π (l r : Type u), r → pgame.inv_ty l r bool.tt → pgame.inv_ty l r bool.tt
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.
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
- pgame.inv_val L R IHl IHr (pgame.inv_ty.right₂ i j) = (1 + (R i - pgame.mk l r L R) * pgame.inv_val L R IHl IHr j) * IHr i
- pgame.inv_val L R IHl IHr (pgame.inv_ty.right₁ i j) = (1 + (L i - pgame.mk l r L R) * pgame.inv_val L R IHl IHr j) * IHl i
- pgame.inv_val L R IHl IHr (pgame.inv_ty.left₂ i j) = (1 + (L i - pgame.mk l r L R) * pgame.inv_val L R IHl IHr j) * IHl i
- pgame.inv_val L R IHl IHr (pgame.inv_ty.left₁ i j) = (1 + (R i - pgame.mk l r L R) * pgame.inv_val L R IHl IHr j) * IHr i
- pgame.inv_val L R IHl IHr pgame.inv_ty.zero = 0
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
- (pgame.mk l r L R).inv' = let l' : Type u_1 := {i // 0 < L i}, L' : l' → pgame := λ (i : l'), L i.val, IHl' : l' → pgame := λ (i : l'), (L i.val).inv', IHr : r → pgame := λ (i : r), (R i).inv' in pgame.mk (pgame.inv_ty l' r bool.ff) (pgame.inv_ty l' r bool.tt) (pgame.inv_val L' R IHl' IHr) (pgame.inv_val L' R IHl' IHr)
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.
The equivalence on numeric pre-games.
Equations
- surreal.equiv x y = x.val.equiv y.val
Construct a surreal number from a numeric pre-game.
Equations
- surreal.mk x h = ⟦⟨x, h⟩⟧
Equations
- surreal.has_zero = {zero := ⟦⟨0, pgame.numeric_zero⟩⟧}
Equations
- surreal.has_one = {one := ⟦⟨1, pgame.numeric_one⟩⟧}
Equations
- surreal.inhabited = {default := 0}
Lift an equivalence-respecting function on pre-games to surreals.
Equations
- surreal.lift f H = quotient.lift (λ (x : {x // x.numeric}), f x.val _) _
Lift a binary equivalence-respecting function on pre-games to surreals.
Equations
- surreal.lift₂ f H = surreal.lift (λ (x : pgame) (ox : x.numeric), surreal.lift (λ (y : pgame) (oy : y.numeric), f x y ox oy) _) _
The relation x ≤ y on surreals.
Equations
- surreal.le = surreal.lift₂ (λ (x y : pgame) (_x : x.numeric) (_x : y.numeric), x ≤ y) surreal.le._proof_1
The relation x < y on surreals.
Equations
- surreal.lt = surreal.lift₂ (λ (x y : pgame) (_x : x.numeric) (_x : y.numeric), x < y) surreal.lt._proof_1
Equations
- surreal.preorder = {le := surreal.le, lt := surreal.lt, le_refl := surreal.preorder._proof_1, le_trans := surreal.preorder._proof_2, lt_iff_le_not_le := surreal.preorder._proof_3}
Equations
- surreal.partial_order = {le := preorder.le surreal.preorder, lt := preorder.lt surreal.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := surreal.partial_order._proof_1}
Equations
- surreal.linear_order = {le := partial_order.le surreal.partial_order, lt := partial_order.lt surreal.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := surreal.linear_order._proof_1}
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
- surreal.add = surreal.lift₂ (λ (x y : pgame) (ox : x.numeric) (oy : y.numeric), ⟦⟨x + y, _⟩⟧) surreal.add._proof_1