Ordinals as games

We define the canonical map Ordinal → SetTheory.PGame, where every ordinal is mapped to the game whose left set consists of all previous ordinals.

The map to surreals is defined in Ordinal.toSurreal.

Main declarations

• Ordinal.toPGame: The canonical map between ordinals and pre-games.
• Ordinal.toPGameEmbedding: The order embedding version of the previous map.

noncomputable def Ordinal.toPGame : Ordinal.{u} → SetTheory.PGame

Converts an ordinal into the corresponding pre-game.

Equations

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

theorem Ordinal.toPGame_def (o : Ordinal.{u_1}) : let_fun this := (_ : IsWellOrder (Quotient.out o).α fun (x x_1 : (Quotient.out o).α) => x < x_1); Ordinal.toPGame o = SetTheory.PGame.mk (Quotient.out o).α PEmpty.{u_1 + 1} (fun (x : (Quotient.out o).α) => Ordinal.toPGame (Ordinal.typein (fun (x x_1 : (Quotient.out o).α) => x < x_1) x)) PEmpty.elim

@[simp]

theorem Ordinal.toPGame_leftMoves (o : Ordinal.{u_1}) : SetTheory.PGame.LeftMoves (Ordinal.toPGame o) = (Quotient.out o).α

@[simp]

theorem Ordinal.toPGame_rightMoves (o : Ordinal.{u_1}) : SetTheory.PGame.RightMoves (Ordinal.toPGame o) = PEmpty.{u_1 + 1}

instance Ordinal.isEmpty_zero_toPGame_leftMoves : IsEmpty (SetTheory.PGame.LeftMoves (Ordinal.toPGame 0))

Equations

• Ordinal.isEmpty_zero_toPGame_leftMoves = (_ : IsEmpty (SetTheory.PGame.LeftMoves (Ordinal.toPGame 0)))

instance Ordinal.isEmpty_toPGame_rightMoves (o : Ordinal.{u_1}) : IsEmpty (SetTheory.PGame.RightMoves (Ordinal.toPGame o))

Equations

• (_ : IsEmpty (SetTheory.PGame.RightMoves (Ordinal.toPGame o))) = (_ : IsEmpty (SetTheory.PGame.RightMoves (Ordinal.toPGame o)))

noncomputable def Ordinal.toLeftMovesToPGame {o : Ordinal.{u_1}} : ↑(Set.Iio o) ≃ SetTheory.PGame.LeftMoves (Ordinal.toPGame o)

Converts an ordinal less than o into a move for the PGame corresponding to o, and vice versa.

Equations

• Ordinal.toLeftMovesToPGame = (Ordinal.enumIsoOut o).trans (Equiv.cast (_ : (Quotient.out o).α = SetTheory.PGame.LeftMoves (Ordinal.toPGame o)))

@[simp]

theorem Ordinal.toLeftMovesToPGame_symm_lt {o : Ordinal.{u_1}} (i : SetTheory.PGame.LeftMoves (Ordinal.toPGame o)) : ↑(Ordinal.toLeftMovesToPGame.symm i) < o

theorem Ordinal.toPGame_moveLeft_hEq {o : Ordinal.{u_1}} : let_fun this := (_ : IsWellOrder (Quotient.out o).α fun (x x_1 : (Quotient.out o).α) => x < x_1); HEq (SetTheory.PGame.moveLeft (Ordinal.toPGame o)) fun (x : (Quotient.out o).α) => Ordinal.toPGame (Ordinal.typein (fun (x x_1 : (Quotient.out o).α) => x < x_1) x)

@[simp]

theorem Ordinal.toPGame_moveLeft' {o : Ordinal.{u_1}} (i : SetTheory.PGame.LeftMoves (Ordinal.toPGame o)) : SetTheory.PGame.moveLeft (Ordinal.toPGame o) i = Ordinal.toPGame ↑(Ordinal.toLeftMovesToPGame.symm i)

theorem Ordinal.toPGame_moveLeft {o : Ordinal.{u_1}} (i : ↑(Set.Iio o)) : SetTheory.PGame.moveLeft (Ordinal.toPGame o) (Ordinal.toLeftMovesToPGame i) = Ordinal.toPGame ↑i

noncomputable def Ordinal.zeroToPGameRelabelling : SetTheory.PGame.Relabelling (Ordinal.toPGame 0) 0

0.toPGame has the same moves as 0.

Equations

• Ordinal.zeroToPGameRelabelling = SetTheory.PGame.Relabelling.isEmpty (Ordinal.toPGame 0)

noncomputable instance Ordinal.uniqueOneToPGameLeftMoves : Unique (SetTheory.PGame.LeftMoves (Ordinal.toPGame 1))

Equations

• Ordinal.uniqueOneToPGameLeftMoves = Equiv.unique (Equiv.cast Ordinal.uniqueOneToPGameLeftMoves.proof_1)

@[simp]

theorem Ordinal.one_toPGame_leftMoves_default_eq : default = Ordinal.toLeftMovesToPGame { val := 0, property := (_ : 0 ∈ Set.Iio 1) }

@[simp]

theorem Ordinal.to_leftMoves_one_toPGame_symm (i : SetTheory.PGame.LeftMoves (Ordinal.toPGame 1)) : Ordinal.toLeftMovesToPGame.symm i = { val := 0, property := (_ : 0 ∈ Set.Iio 1) }

theorem Ordinal.one_toPGame_moveLeft (x : SetTheory.PGame.LeftMoves (Ordinal.toPGame 1)) : SetTheory.PGame.moveLeft (Ordinal.toPGame 1) x = Ordinal.toPGame 0

noncomputable def Ordinal.oneToPGameRelabelling : SetTheory.PGame.Relabelling (Ordinal.toPGame 1) 1

1.toPGame has the same moves as 1.

Equations

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

theorem Ordinal.toPGame_lf {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (h : a < b) : SetTheory.PGame.LF (Ordinal.toPGame a) (Ordinal.toPGame b)

theorem Ordinal.toPGame_le {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (h : a ≤ b) : Ordinal.toPGame a ≤ Ordinal.toPGame b

theorem Ordinal.toPGame_lt {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (h : a < b) : Ordinal.toPGame a < Ordinal.toPGame b

theorem Ordinal.toPGame_nonneg (a : Ordinal.{u_1}) : 0 ≤ Ordinal.toPGame a

@[simp]

theorem Ordinal.toPGame_lf_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} : SetTheory.PGame.LF (Ordinal.toPGame a) (Ordinal.toPGame b) ↔ a < b

@[simp]

theorem Ordinal.toPGame_le_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} : Ordinal.toPGame a ≤ Ordinal.toPGame b ↔ a ≤ b

@[simp]

theorem Ordinal.toPGame_lt_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} : Ordinal.toPGame a < Ordinal.toPGame b ↔ a < b

@[simp]

theorem Ordinal.toPGame_equiv_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} : Ordinal.toPGame a ≈ Ordinal.toPGame b ↔ a = b

theorem Ordinal.toPGame_injective : Function.Injective Ordinal.toPGame

@[simp]

theorem Ordinal.toPGame_eq_iff {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} : Ordinal.toPGame a = Ordinal.toPGame b ↔ a = b

@[simp]

theorem Ordinal.toPGameEmbedding_apply : ∀ (a : Ordinal.{u}), Ordinal.toPGameEmbedding a = Ordinal.toPGame a

noncomputable def Ordinal.toPGameEmbedding : Ordinal.{u} ↪o SetTheory.PGame

The order embedding version of toPGame.

Equations

• Ordinal.toPGameEmbedding = { toEmbedding := { toFun := Ordinal.toPGame, inj' := Ordinal.toPGame_injective }, map_rel_iff' := @Ordinal.toPGame_le_iff }

theorem Ordinal.toPGame_add (a : Ordinal.{u}) (b : Ordinal.{u}) : Ordinal.toPGame a + Ordinal.toPGame b ≈ Ordinal.toPGame (Ordinal.nadd a b)

The sum of ordinals as games corresponds to natural addition of ordinals.

@[simp]

theorem Ordinal.toPGame_add_mk' (a : Ordinal.{u_1}) (b : Ordinal.{u_1}) : ⟦Ordinal.toPGame a⟧ + ⟦Ordinal.toPGame b⟧ = ⟦Ordinal.toPGame (Ordinal.nadd a b)⟧