Multiplication of pre-games can't be lifted to the quotient

We show that there exist equivalent pre-games x₁ ≈ x₂ and y such that x₁ * y ≉ x₂ * y. In particular, we cannot define the multiplication of games in general.

The specific counterexample we use is x₁ = y = {0 | 0} and x₂ = {-1, 0 | 0, 1}. The first game is colloquially known as star, so we use the name star' for the second. We prove that star ≈ star' and star * star ≈ star, but star' * star ≉ star.

def IGame.star' : IGame

The game ⋆' = {-1, 0 | 0, 1}, which is equivalent but not identical to ⋆.

Equations

• IGame.star' = !{{0, -1} | {0, 1}}

theorem IGame.star'_equiv_star : star' ≈ ⋆

⋆' is equivalent to ⋆.

theorem IGame.star'_mul_star_not_equiv : ¬star' * ⋆ ≈ ⋆

⋆' * ⋆ is not equivalent to *.

theorem IGame.mul_not_lift : ∃ (x₁ : IGame) (x₂ : IGame) (y : IGame), x₁ ≈ x₂ ∧ ¬x₁ * y ≈ x₂ * y

Pre-game multiplication cannot be lifted to games.