Ordinals as games #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define the canonical map ordinal → 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.to_surreal.

Main declarations #

ordinal.to_pgame: The canonical map between ordinals and pre-games.
ordinal.to_pgame_embedding: The order embedding version of the previous map.

source

def ordinal.to_pgame :

ordinal → pgame

Converts an ordinal into the corresponding pre-game.

Equations

o.to_pgame = pgame.mk (quotient.out o).α pempty (λ (x : (quotient.out o).α), let hwf : ordinal.typein has_lt.lt x < o := _ in (ordinal.typein has_lt.lt x).to_pgame) pempty.elim

source

theorem ordinal.to_pgame_def (o : ordinal) :

o.to_pgame = pgame.mk (quotient.out o).α pempty (λ (x : (quotient.out o).α), (ordinal.typein has_lt.lt x).to_pgame) pempty.elim

source

@[simp]

theorem ordinal.to_pgame_left_moves (o : ordinal) :

o.to_pgame.left_moves = (quotient.out o).α

source

@[simp]

theorem ordinal.to_pgame_right_moves (o : ordinal) :

o.to_pgame.right_moves = pempty

source

@[protected, instance]

def ordinal.is_empty_zero_to_pgame_left_moves :

is_empty 0.to_pgame.left_moves

source

@[protected, instance]

def ordinal.is_empty_to_pgame_right_moves (o : ordinal) :

is_empty o.to_pgame.right_moves

source

noncomputable def ordinal.to_left_moves_to_pgame {o : ordinal} :

↥(set.Iio o) ≃ o.to_pgame.left_moves

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

Equations

ordinal.to_left_moves_to_pgame = o.enum_iso_out.to_equiv.trans (equiv.cast ordinal.to_left_moves_to_pgame._proof_1)

source

@[simp]

theorem ordinal.to_left_moves_to_pgame_symm_lt {o : ordinal} (i : o.to_pgame.left_moves) :

↑(⇑(ordinal.to_left_moves_to_pgame.symm) i) < o

source

theorem ordinal.to_pgame_move_left_heq {o : ordinal} :

o.to_pgame.move_left == λ (x : (quotient.out o).α), (ordinal.typein has_lt.lt x).to_pgame

source

@[simp]

theorem ordinal.to_pgame_move_left' {o : ordinal} (i : o.to_pgame.left_moves) :

o.to_pgame.move_left i = (⇑(ordinal.to_left_moves_to_pgame.symm) i).val.to_pgame

source

theorem ordinal.to_pgame_move_left {o : ordinal} (i : ↥(set.Iio o)) :

o.to_pgame.move_left (⇑ordinal.to_left_moves_to_pgame i) = i.val.to_pgame

source

noncomputable def ordinal.zero_to_pgame_relabelling :

0.to_pgame.relabelling 0

0.to_pgame has the same moves as 0.

Equations

ordinal.zero_to_pgame_relabelling = pgame.relabelling.is_empty 0.to_pgame

source

@[protected, instance]

noncomputable def ordinal.unique_one_to_pgame_left_moves :

unique 1.to_pgame.left_moves

Equations

ordinal.unique_one_to_pgame_left_moves = (equiv.cast ordinal.unique_one_to_pgame_left_moves._proof_1).unique

source

@[simp]

theorem ordinal.one_to_pgame_left_moves_default_eq :

inhabited.default = ⇑ordinal.to_left_moves_to_pgame ⟨0, _⟩

source

@[simp]

theorem ordinal.to_left_moves_one_to_pgame_symm (i : 1.to_pgame.left_moves) :

⇑(ordinal.to_left_moves_to_pgame.symm) i = ⟨0, _⟩

source

theorem ordinal.one_to_pgame_move_left (x : 1.to_pgame.left_moves) :

1.to_pgame.move_left x = 0.to_pgame

source

noncomputable def ordinal.one_to_pgame_relabelling :

1.to_pgame.relabelling 1

1.to_pgame has the same moves as 1.

Equations

ordinal.one_to_pgame_relabelling = pgame.relabelling.mk (equiv.equiv_of_unique 1.to_pgame.left_moves 1.left_moves) (equiv.equiv_of_is_empty 1.to_pgame.right_moves 1.right_moves) (λ (i : 1.to_pgame.left_moves), _.mpr (ordinal.one_to_pgame_relabelling._proof_3.mp ordinal.zero_to_pgame_relabelling)) is_empty_elim

source

theorem ordinal.to_pgame_lf {a b : ordinal} (h : a < b) :

a.to_pgame.lf b.to_pgame

source

theorem ordinal.to_pgame_le {a b : ordinal} (h : a ≤ b) :

a.to_pgame ≤ b.to_pgame

source

theorem ordinal.to_pgame_lt {a b : ordinal} (h : a < b) :

a.to_pgame < b.to_pgame

source

theorem ordinal.to_pgame_nonneg (a : ordinal) :

0 ≤ a.to_pgame

source

@[simp]

theorem ordinal.to_pgame_lf_iff {a b : ordinal} :

a.to_pgame.lf b.to_pgame ↔ a < b

source

@[simp]

theorem ordinal.to_pgame_le_iff {a b : ordinal} :

a.to_pgame ≤ b.to_pgame ↔ a ≤ b

source

@[simp]

theorem ordinal.to_pgame_lt_iff {a b : ordinal} :

a.to_pgame < b.to_pgame ↔ a < b

source

@[simp]

theorem ordinal.to_pgame_equiv_iff {a b : ordinal} :

a.to_pgame.equiv b.to_pgame ↔ a = b

source

theorem ordinal.to_pgame_injective :

function.injective ordinal.to_pgame

source

@[simp]

theorem ordinal.to_pgame_eq_iff {a b : ordinal} :

a.to_pgame = b.to_pgame ↔ a = b

source

@[simp]

theorem ordinal.to_pgame_embedding_apply (ᾰ : ordinal) :

⇑ordinal.to_pgame_embedding ᾰ = ᾰ.to_pgame

source

noncomputable def ordinal.to_pgame_embedding :

ordinal ↪o pgame

The order embedding version of to_pgame.

Equations

ordinal.to_pgame_embedding = {to_embedding := {to_fun := ordinal.to_pgame, inj' := ordinal.to_pgame_injective}, map_rel_iff' := ordinal.to_pgame_le_iff}

source

theorem ordinal.to_pgame_add (a b : ordinal) :

(a.to_pgame + b.to_pgame).equiv (a.nadd b).to_pgame

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

source

@[simp]

theorem ordinal.to_pgame_add_mk (a b : ordinal) :

⟦a.to_pgame ⟧ + ⟦b.to_pgame ⟧ = ⟦(a.nadd b).to_pgame⟧