Documentation

CombinatorialGames.Game.Ordinal

Ordinals as games #

We define the canonical map NatOrdinal → IGame, where every ordinal is mapped to the game whose left set consists of all previous ordinals. We make use of the type alias NatOrdinal rather than Ordinal, as this map also preserves addition, and in the case of surreals, multiplication. The map to surreals is defined in CombinatorialGames.Surreal.Ordinal.

We also prove some properties about NatCast, which is related to the previous construction by toIGame (↑n) ≈ ↑n.

Main declarations #

Lemmas to upstream #

source
@[simp]
theorem OrderEmbedding.antisymmRel_iff_antisymmRel {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a b : α} (f : α ↪o β) :
f a ≈ f b ↔ a ≈ b
source
theorem OrderEmbedding.antisymmRel_iff_eq {α : Type u_1} {β : Type u_2} [Preorder α] [PartialOrder β] {a b : α} (f : α ↪o β) :
f a ≈ f b ↔ a = b

NatOrdinal to IGame #

source
def NatOrdinal.toIGame :
NatOrdinal ↪o IGame

The canonical map from NatOrdinal to IGame, sending o to {Iio o | ∅}.

Equations
Instances For
    source
    instance NatOrdinal.instCoeIGame :
    Coe NatOrdinal IGame
    Equations
    source
    theorem NatOrdinal.toIGame_def (o : NatOrdinal) :
    toIGame o = !{⇑toIGame '' Set.Iio o | ∅}
    source
    @[simp]
    theorem NatOrdinal.leftMoves_toIGame (o : NatOrdinal) :
    IGame.moves Player.left (toIGame o) = ⇑toIGame '' Set.Iio o
    source
    @[simp]
    theorem NatOrdinal.rightMoves_toIGame (o : NatOrdinal) :
    IGame.moves Player.right (toIGame o) = ∅
    source
    theorem NatOrdinal.forall_leftMoves_toIGame {P : IGame → Prop} {o : NatOrdinal} :
    (∀ x ∈ IGame.moves Player.left (toIGame o), P x) ↔ ∀ a < o, P (toIGame a)
    source
    theorem NatOrdinal.exists_leftMoves_toIGame {P : IGame → Prop} {o : NatOrdinal} :
    (∃ x ∈ IGame.moves Player.left (toIGame o), P x) ↔ ∃ a < o, P (toIGame a)
    source
    theorem NatOrdinal.forall_leftMoves_toIGame_natCast {P : IGame → Prop} {n : ℕ} :
    (∀ x ∈ IGame.moves Player.left (toIGame ↑n), P x) ↔ ∀ m < n, P (toIGame ↑m)
    source
    theorem NatOrdinal.exists_leftMoves_toIGame_natCast {P : IGame → Prop} {n : ℕ} :
    (∃ x ∈ IGame.moves Player.left (toIGame ↑n), P x) ↔ ∃ m < n, P (toIGame ↑m)
    source
    theorem NatOrdinal.forall_leftMoves_toIGame_ofNat {P : IGame → Prop} {n : ℕ} [n.AtLeastTwo] :
    (∀ x ∈ IGame.moves Player.left (toIGame (OfNat.ofNat n)), P x) ↔ ∀ m < n, P (toIGame ↑m)
    source
    theorem NatOrdinal.exists_leftMoves_toIGame_ofNat {P : IGame → Prop} {n : ℕ} [n.AtLeastTwo] :
    (∃ x ∈ IGame.moves Player.left (toIGame (OfNat.ofNat n)), P x) ↔ ∃ m < n, P (toIGame ↑m)
    source
    theorem NatOrdinal.mem_leftMoves_toIGame_of_lt {a b : NatOrdinal} (h : a < b) :
    toIGame a ∈ IGame.moves Player.left (toIGame b)
    source
    @[simp]
    theorem NatOrdinal.toIGame_zero :
    toIGame 0 = 0
    source
    @[simp]
    theorem NatOrdinal.toIGame_one :
    toIGame 1 = 1
    source
    @[simp]
    theorem NatOrdinal.not_toIGame_fuzzy (a b : NatOrdinal) :
    ¬toIGame a ‖ toIGame b
    source
    @[simp]
    theorem NatOrdinal.toIGame_nonneg (a : NatOrdinal) :
    0 ≤ toIGame a

    NatOrdinal to Game #

    source
    noncomputable def NatOrdinal.toGame :
    NatOrdinal ↪o Game

    Converts an ordinal into the corresponding game.

    Equations
    Instances For
      source
      instance NatOrdinal.instCoeGame :
      Coe NatOrdinal Game
      Equations
      source
      @[simp]
      theorem Game.mk_natOrdinal_toIGame (o : NatOrdinal) :
      mk (NatOrdinal.toIGame o) = NatOrdinal.toGame o
      source
      theorem NatOrdinal.toGame_def (o : NatOrdinal) :
      toGame o = !{⇑toGame '' Set.Iio o | ∅}
      source
      @[simp]
      theorem NatOrdinal.toGame_zero :
      toGame 0 = 0
      source
      @[simp]
      theorem NatOrdinal.toGame_one :
      toGame 1 = 1
      source
      @[simp]
      theorem NatOrdinal.not_toGame_fuzzy (a b : NatOrdinal) :
      ¬toGame a ‖ toGame b
      source
      @[simp]
      theorem NatOrdinal.toGame_nonneg (a : NatOrdinal) :
      0 ≤ toGame a
      source
      @[irreducible]
      theorem NatOrdinal.toIGame_add (a b : NatOrdinal) :
      toIGame (a + b) ≈ toIGame a + toIGame b

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

      source
      @[simp]
      theorem NatOrdinal.toGame_add (a b : NatOrdinal) :
      toGame (a + b) = toGame a + toGame b
      source
      @[irreducible]
      theorem NatOrdinal.toIGame_mul (a b : NatOrdinal) :
      toIGame (a * b) ≈ toIGame a * toIGame b

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

      source
      @[simp]
      theorem NatOrdinal.toGame_mul (a b : NatOrdinal) :
      toGame (a * b) = Game.mk (toIGame a * toIGame b)
      source
      def NatOrdinal.toGameAddHom :
      NatOrdinal →+o Game

      NatOrdinal.toGame as an OrderAddMonoidHom.

      Equations
      Instances For
        source
        @[simp]
        theorem NatOrdinal.toGameAddHom_apply (a : NatOrdinal) :
        toGameAddHom a = toGame a

        NatCast properties #

        source
        @[simp]
        theorem NatOrdinal.toGame_natCast (n : ℕ) :
        toGame ↑n = ↑n
        source
        theorem NatOrdinal.toIGame_natCast_equiv (n : ℕ) :
        toIGame ↑n ≈ ↑n

        Note that the equality doesn't hold, as e.g. ↑2 = {1 | }, while toIGame 2 = {0, 1 | }.

        source
        @[irreducible]
        theorem IGame.Short.exists_lt_natCast (x : IGame) [x.Short] :
        ∃ (n : ℕ), x < ↑n
        source
        theorem IGame.Short.exists_neg_natCast_lt (x : IGame) [x.Short] :
        ∃ (n : ℕ), -↑n < x
        source
        theorem IGame.Short.lt_omega0 (x : IGame) [x.Short] :
        x < NatOrdinal.toIGame (NatOrdinal.of Ordinal.omega0)
        source
        theorem IGame.Short.neg_omega0_lt (x : IGame) [x.Short] :
        -NatOrdinal.toIGame (NatOrdinal.of Ordinal.omega0) < x