Multiplication of pre-games can't be lifted to the quotient #
We show that there exist equivalent pregames 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.
The game {-1, 0 | 0, 1}, which is equivalent but not identical to *.
Equations
- Counterexample.PGame.star' = SetTheory.PGame.ofLists [0, -1] [0, 1]
Instances For
*' is its own negative.
*' is equivalent to *.
The equation ** = * is an identity, though not a relabelling.
*'* ⧏ * implies *'* ≉ *.
theorem
Counterexample.PGame.mul_not_lift :
∃ (x₁ : SetTheory.PGame) (x₂ : SetTheory.PGame) (y : SetTheory.PGame), x₁ ≈ x₂ ∧ ¬x₁ * y ≈ x₂ * y
Pre-game multiplication cannot be lifted to games.