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.

@[irreducible]

noncomputable def Ordinal.toPGame (o : Ordinal.{u}) : SetTheory.PGame

Converts an ordinal into the corresponding pre-game.

Equations

• o.toPGame = SetTheory.PGame.mk o.toType PEmpty.{?u.2 + 1} (fun (x : o.toType) => (↑(o.enumIsoToType.symm x)).toPGame) PEmpty.elim

@[simp]

theorem Ordinal.toPGame_leftMoves (o : Ordinal.{u_1}) : o.toPGame.LeftMoves = o.toType

@[simp]

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

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

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

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

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

Equations

• Ordinal.toLeftMovesToPGame = o.enumIsoToType.trans (Equiv.cast ⋯)

@[simp]

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

theorem Ordinal.toPGame_moveLeft_hEq {o : Ordinal.{u_1}} : o.toPGame.moveLeft ≍ fun (x : o.toType) => (↑(o.enumIsoToType.symm x)).toPGame

@[simp]

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

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

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

0.toPGame has the same moves as 0.

Equations

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

theorem Ordinal.toPGame_zero : toPGame 0 ≈ 0

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

Equations

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

@[simp]

theorem Ordinal.one_toPGame_leftMoves_default_eq : default = toLeftMovesToPGame ⟨0, ⋯⟩

@[simp]

theorem Ordinal.to_leftMoves_one_toPGame_symm (i : (toPGame 1).LeftMoves) : toLeftMovesToPGame.symm i = ⟨0, ⋯⟩

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

noncomputable def Ordinal.oneToPGameRelabelling : (toPGame 1).Relabelling 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_one : toPGame 1 ≈ 1

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Ordinal.toPGame_injective : Function.Injective toPGame

@[simp]

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

@[deprecated Ordinal.toPGame_inj (since := "2024-12-29")]

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

Alias of Ordinal.toPGame_inj.

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

The order embedding version of toPGame.

Equations

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

@[simp]

theorem Ordinal.toPGameEmbedding_apply (o : Ordinal.{u}) : toPGameEmbedding o = o.toPGame

noncomputable def Ordinal.toGame : Ordinal.{u} ↪o SetTheory.Game

Converts an ordinal into the corresponding game.

Equations

• Ordinal.toGame = { toFun := fun (o : Ordinal.{?u.9}) => ⟦o.toPGame⟧, inj' := Ordinal.toGame._proof_1, map_rel_iff' := ⋯ }

@[simp]

theorem Ordinal.mk_toPGame (o : Ordinal.{u_1}) : ⟦o.toPGame⟧ = toGame o

@[deprecated Ordinal.toGame (since := "2024-11-23")]

def Ordinal.toGameEmbedding : Ordinal.{u} ↪o SetTheory.Game

Alias of Ordinal.toGame.

---

Converts an ordinal into the corresponding game.

Equations

• Ordinal.toGameEmbedding = Ordinal.toGame

@[simp]

theorem Ordinal.toGame_zero : toGame 0 = 0

@[simp]

theorem Ordinal.toGame_one : toGame 1 = 1

theorem Ordinal.toGame_injective : Function.Injective ⇑toGame

@[simp]

theorem Ordinal.toGame_lf_iff {a b : Ordinal.{u_1}} : (toGame a).LF (toGame b) ↔ a < b

theorem Ordinal.toGame_le_iff {a b : Ordinal.{u_1}} : toGame a ≤ toGame b ↔ a ≤ b

theorem Ordinal.toGame_lt_iff {a b : Ordinal.{u_1}} : toGame a < toGame b ↔ a < b

theorem Ordinal.toGame_inj {a b : Ordinal.{u_1}} : toGame a = toGame b ↔ a = b

@[deprecated Ordinal.toGame_inj (since := "2024-12-29")]

theorem Ordinal.toGame_eq_iff {a b : Ordinal.{u_1}} : toGame a = toGame b ↔ a = b

Alias of Ordinal.toGame_inj.

@[irreducible]

theorem Ordinal.toPGame_nadd (a b : Ordinal.{u_1}) : (a.nadd b).toPGame ≈ a.toPGame + b.toPGame

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

theorem Ordinal.toGame_nadd (a b : Ordinal.{u_1}) : toGame (a.nadd b) = toGame a + toGame b

@[irreducible]

theorem Ordinal.toPGame_nmul (a b : Ordinal.{u_1}) : (a.nmul b).toPGame ≈ a.toPGame * b.toPGame

The natural multiplication of ordinals corresponds to their product as pre-games.

theorem Ordinal.toGame_nmul (a b : Ordinal.{u_1}) : toGame (a.nmul b) = ⟦a.toPGame * b.toPGame⟧

@[simp]

theorem Ordinal.toGame_natCast (n : ℕ) : toGame ↑n = ↑n

theorem Ordinal.toPGame_natCast (n : ℕ) : (↑n).toPGame ≈ ↑n