Documentation

CombinatorialGames.Surreal.Basic

Surreal numbers #

The basic theory of surreal numbers, built on top of the theory of combinatorial (pre-)games. A surreal number is defined as an equivalence class of numeric games.

Surreal numbers inherit the relations ≤ and < from games, and these relations satisfy the axioms of a linear order. In fact, the surreals form a complete ordered field, containing a copy of the reals, and much else besides!

Algebraic operations #

In this file, we show that the surreals form a linear ordered commutative group.

In CombinatorialGames.Surreal.Multiplication, we define multiplication and show that the surreals form a linear ordered commutative ring. In CombinatorialGames.Surreal.Division we further show the surreals are a field.

Simplicity theorem #

def IGame.Fits (x y : IGame) :

x fits within y when z ⧏ x for every z ∈ yᴸ, and x ⧏ z for every z ∈ yᴿ.

The simplicity theorem states that if a game fits a numeric game, but none of its options do, then the games are equivalent. In particular, a numeric game is equivalent to the game of the least birthday that fits in it

Equations

x.Fits y = ((∀ z ∈ IGame.moves Player.left y, ¬x ≤ z) ∧ ∀ z ∈ IGame.moves Player.right y, ¬z ≤ x)

Instances For

theorem IGame.fits_of_equiv {x y : IGame} (h : x ≈ y) :

x.Fits y

theorem IGame.AntisymmRel.Fits {x y : IGame} (h : x ≈ y) :

x.Fits y

Alias of IGame.fits_of_equiv.

theorem IGame.Fits.refl (x : IGame) :

x.Fits x

instance IGame.instReflFits :

theorem IGame.Fits.antisymm {x y : IGame} (h₁ : x.Fits y) (h₂ : y.Fits x) :

x ≈ y

@[simp]

theorem IGame.fits_neg_iff {x y : IGame} :

(-x).Fits (-y) ↔ x.Fits y

theorem IGame.Fits.neg {x y : IGame} :

x.Fits y → (-x).Fits (-y)

Alias of the reverse direction of IGame.fits_neg_iff.

theorem IGame.not_fits_iff {x y : IGame} :

¬x.Fits y ↔ (∃ z ∈ moves left y, x ≤ z) ∨ ∃ z ∈ moves right y, z ≤ x

theorem IGame.Fits.congr {x y z : IGame} (h : x ≈ y) (hx : x.Fits z) :

y.Fits z

theorem IGame.fits_congr {x y z : IGame} (h : x ≈ y) :

x.Fits z ↔ y.Fits z

theorem IGame.Fits.equiv_of_forall_moves {x y : IGame} (hx : x.Fits y) (hl : ∀ z ∈ moves left x, ∃ w ∈ moves left y, z ≤ w) (hr : ∀ z ∈ moves right x, ∃ w ∈ moves right y, w ≤ z) :

x ≈ y

A variant of the simplicity theorem with hypotheses that are easier to show.

theorem IGame.Fits.equiv_of_forall_not_fits {x y : IGame} [x.Numeric] (hx : x.Fits y) (h : ∀ (p : Player), ∀ z ∈ moves p x, ¬z.Fits y) :

x ≈ y

A variant of the simplicity theorem: if a numeric game x fits within a game y, but none of its options do, then x ≈ y.

Note that under most circumstances, Fits.equiv_of_forall_moves is easier to use.

theorem IGame.Fits.equiv_of_forall_birthday_le {x y : IGame} [x.Numeric] (hx : x.Fits y) (H : ∀ (z : IGame), z.Numeric → z.Fits y → x.birthday ≤ z.birthday) :

x ≈ y

A variant of the simplicity theorem: if x is the numeric game with the least birthday that fits within y, then x ≈ y.

@[simp]

theorem IGame.fits_zero_iff_equiv {x : IGame} :

Fits 0 x ↔ x ≈ 0

A specialization of the simplicity theorem to 0.

theorem IGame.equiv_one_of_fits {x : IGame} (hx : Fits 1 x) (h : ¬x ≈ 0) :

x ≈ 1

A specialization of the simplicity theorem to 1.

Surreal numbers #

Type (u + 1)

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

Equations

Surreal = Antisymmetrization (Subtype IGame.Numeric) fun (x1 x2 : Subtype IGame.Numeric) => x1 ≤ x2

Instances For

def Surreal.mk (x : IGame) [h : x.Numeric] :

The quotient map from the subtype of numeric IGames into Game.

Equations

Surreal.mk x = ⟦⟨x, h⟩⟧

Instances For

theorem Surreal.mk_eq_mk {x y : IGame} [x.Numeric] [y.Numeric] :

mk x = mk y ↔ x ≈ y

theorem Surreal.mk_eq {x y : IGame} [x.Numeric] [y.Numeric] :

x ≈ y → mk x = mk y

Alias of the reverse direction of Surreal.mk_eq_mk.

theorem Surreal.ind {motive : Surreal → Prop} (mk : ∀ (y : IGame) [inst : y.Numeric], motive (mk y)) (x : Surreal) :

motive x

def Surreal.out (x : Surreal) :

Choose an element of the equivalence class using the axiom of choice.

Equations

x.out = ↑(Quotient.out x)

Instances For

@[simp]

instance Surreal.instNumericOut (x : Surreal) :

@[simp]

theorem Surreal.out_eq (x : Surreal) :

mk x.out = x

theorem Surreal.mk_out_equiv (x : IGame) [h : x.Numeric] :

(mk x).out ≈ x

theorem Surreal.equiv_mk_out (x : IGame) [x.Numeric] :

x ≈ (mk x).out

instance Surreal.instZero :

Equations

Surreal.instZero = { zero := Surreal.mk 0 }

instance Surreal.instOne :

Equations

Surreal.instOne = { one := Surreal.mk 1 }

instance Surreal.instInhabited :

Inhabited Surreal

Equations

Surreal.instInhabited = { default := 0 }

instance Surreal.instAdd :

Equations

Surreal.instAdd = { add := Quotient.map₂ (fun (a b : Subtype IGame.Numeric) => ⟨↑a + ↑b, ⋯⟩) Surreal.instAdd._proof_2 }

instance Surreal.instNeg :

Equations

Surreal.instNeg = { neg := Quotient.map (fun (a : Subtype IGame.Numeric) => ⟨-↑a, ⋯⟩) Surreal.instNeg._proof_2 }

instance Surreal.instPartialOrder :

PartialOrder Surreal

Equations

Surreal.instPartialOrder = inferInstanceAs (PartialOrder (Antisymmetrization (Subtype IGame.Numeric) fun (x1 x2 : Subtype IGame.Numeric) => x1 ≤ x2))

instance Surreal.instLinearOrder :

LinearOrder Surreal

Equations

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

instance Surreal.instAddCommGroup :

AddCommGroup Surreal

Equations

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

instance Surreal.instAddGroupWithOne :

AddGroupWithOne Surreal

Equations

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

instance Surreal.instIsOrderedAddMonoid :

IsOrderedAddMonoid Surreal

@[simp]

theorem Surreal.mk_zero :

mk 0 = 0

@[simp]

theorem Surreal.mk_one :

mk 1 = 1

@[simp]

theorem Surreal.mk_add (x y : IGame) [x.Numeric] [y.Numeric] :

mk (x + y) = mk x + mk y

@[simp]

theorem Surreal.mk_neg (x : IGame) [x.Numeric] :

mk (-x) = -mk x

@[simp]

theorem Surreal.mk_sub (x y : IGame) [x.Numeric] [y.Numeric] :

mk (x - y) = mk x - mk y

@[simp]

theorem Surreal.mk_le_mk {x y : IGame} [x.Numeric] [y.Numeric] :

mk x ≤ mk y ↔ x ≤ y

@[simp]

theorem Surreal.mk_lt_mk {x y : IGame} [x.Numeric] [y.Numeric] :

mk x < mk y ↔ x < y

@[simp]

theorem Surreal.mk_natCast (n : ℕ) :

mk ↑n = ↑n

@[simp]

theorem Surreal.mk_intCast (n : ℤ) :

mk ↑n = ↑n

instance Surreal.instZeroLEOneClass :

ZeroLEOneClass Surreal

instance Surreal.instNeZeroOfNat :

instance Surreal.instNontrivial :

Nontrivial Surreal

def Surreal.toGame :

Surreal ↪o Game

Casts a Surreal number into a Game.

Equations

Surreal.toGame = { toFun := Quotient.lift (fun (x : Subtype IGame.Numeric) => Game.mk ↑x) Surreal.toGame._proof_1, inj' := Surreal.toGame._proof_2, map_rel_iff' := @Surreal.toGame._proof_3 }

Instances For

@[simp]

theorem Surreal.toGame_mk (x : IGame) [x.Numeric] :

toGame (mk x) = Game.mk x

@[simp]

theorem Surreal.toGame_zero :

@[simp]

theorem Surreal.toGame_one :

theorem Surreal.toGame_le_iff {a b : Surreal} :

toGame a ≤ toGame b ↔ a ≤ b

theorem Surreal.toGame_lt_iff {a b : Surreal} :

toGame a < toGame b ↔ a < b

theorem Surreal.toGame_inj {a b : Surreal} :

toGame a = toGame b ↔ a = b

def Surreal.toGameAddHom :

Surreal →+o Game

Surreal.toGame as an OrderAddMonoidHom

Equations

Surreal.toGameAddHom = { toFun := ⇑Surreal.toGame, map_zero' := Surreal.toGameAddHom._proof_1, map_add' := Surreal.toGameAddHom._proof_2, monotone' := Surreal.toGameAddHom._proof_3 }

Instances For

@[simp]

theorem Surreal.toGameAddHom_apply (a : Surreal) :

toGameAddHom a = toGame a

@[simp]

theorem Surreal.toGame_add (x y : Surreal) :

toGame (x + y) = toGame x + toGame y

@[simp]

theorem Surreal.toGame_neg (x : Surreal) :

toGame (-x) = -toGame x

@[simp]

theorem Surreal.toGame_sub (x y : Surreal) :

toGame (x - y) = toGame x - toGame y

@[simp]

theorem Surreal.toGame_natCast (n : ℕ) :

toGame ↑n = ↑n

@[simp]

theorem Surreal.toGame_intCast (n : ℤ) :

toGame ↑n = ↑n

@[simp]

theorem Surreal.game_out_eq (x : Surreal) :

Game.mk x.out = toGame x

instance Surreal.instOfSetsForallForallMemSetLeftForallForallRightLt :

OfSets Surreal fun (st : Player → Set Surreal) => ∀ x ∈ st Player.left, ∀ y ∈ st Player.right, x < y

Construct a Surreal from its left and right sets, and a proof that all elements from the left set are less than all the elements of the right set.

Note that although this function is well-defined, this function isn't injective, nor do equivalence classes in Surreal have a canonical representative. (Note however that every short numeric game has a unique "canonical" form!)

Equations

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

theorem Surreal.toGame_ofSets' (st : Player → Set Surreal) [Small.{u, u + 1} ↑(st Player.left)] [Small.{u, u + 1} ↑(st Player.right)] {H : ∀ x ∈ st Player.left, ∀ y ∈ st Player.right, x < y} :

toGame !{st} = !{fun (p : Player) => ⇑toGame '' st p}

@[simp]

theorem Surreal.toGame_ofSets (s t : Set Surreal) [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] {H : ∀ x ∈ s, ∀ y ∈ t, x < y} :

toGame !{s | t} = !{⇑toGame '' s | ⇑toGame '' t}

theorem Surreal.mk_ofSets' {st : Player → Set IGame} [Small.{u, u + 1} ↑(st Player.left)] [Small.{u, u + 1} ↑(st Player.right)] {H : !{st}.Numeric} :

mk !{st} = !{fun (p : Player) => Set.range fun (x : ↑(st p)) => mk ↑x}

theorem Surreal.mk_ofSets {s t : Set IGame} [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] {H : !{s | t}.Numeric} :

mk !{s | t} = !{Set.range fun (x : ↑s) => mk ↑x | Set.range fun (x : ↑t) => mk ↑x}

theorem Surreal.lt_ofSets_of_mem_left {s t : Set Surreal} [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] {H : ∀ x ∈ s, ∀ y ∈ t, x < y} {x : Surreal} (hx : x ∈ s) :

x < !{s | t}

theorem Surreal.ofSets_lt_of_mem_right {s t : Set Surreal} [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] {H : ∀ x ∈ s, ∀ y ∈ t, x < y} {x : Surreal} (hx : x ∈ t) :

!{s | t} < x

theorem Surreal.zero_def :

0 = !{fun (x : Player) => ∅}

theorem Surreal.one_def :

1 = !{{0} | ∅}

instance Surreal.instDenselyOrdered :

DenselyOrdered Surreal