Surreal division

In this file, we prove that if x is a positive numeric game, then x⁻¹ (defined in Mathlib.SetTheory.Game.IGame) is a number and is a multiplicative inverse for x. We use that to define the field structure on Surreal.

This is Theorem 1.10 in ONAG, and we follow the broad strokes of the proof. We prove by simultaneous induction that if x is positive and numeric, then (ii) x⁻¹ is numeric, and (iv) x * x⁻¹ ≈ 1. We do this by showing the inductive hypothesis implies that (i) x * y < 1 for y ∈ x⁻¹.leftMoves and 1 < x * y for y ∈ x⁻¹.rightMoves, and that (iv) y < 1 for y ∈ (x * x⁻¹).leftMoves and 1 < y for y ∈ (x * x⁻¹.rightMoves).

An important difference is that Conway assumes that x has no negative left options, while we don't make use of this assumption. This is because our definition of the inverse is tweaked to ensure that only positive left options of x generate the options for x⁻¹. To make sure the induction checks out, we require two small extra arithmetic lemmas mulOption_le and le_mulOption.

Once we have defined the inverse for positive x, it is extended in the obvious way to negative numbers.

Arithmetic lemmas

theorem Surreal.Division.mulOption_le (x y : IGame) {a b : IGame} [x.Numeric] [y.Numeric] [a.Numeric] [b.Numeric] (ha : a ≤ 0) (hb : b ≤ y) : IGame.mulOption x y a b ≤ x * b

theorem Surreal.Division.le_mulOption (x y : IGame) {a b : IGame} [x.Numeric] [y.Numeric] [a.Numeric] [b.Numeric] (ha : a ≤ 0) (hb : y ≤ b) : x * b ≤ IGame.mulOption x y a b

Inductive proof

theorem Surreal.Division.numeric_option_inv {x : IGame} [x.Numeric] (hx : 0 < x) (hl : ∀ y ∈ x.leftMoves, 0 < y → y⁻¹.Numeric) (hr : ∀ y ∈ x.rightMoves, y⁻¹.Numeric) : (∀ y ∈ x⁻¹.leftMoves, y.Numeric) ∧ ∀ y ∈ x⁻¹.rightMoves, y.Numeric

theorem Surreal.Division.mul_inv_option_mem {x : IGame} [x.Numeric] (hx : 0 < x) (hl : ∀ y ∈ x.leftMoves, 0 < y → y⁻¹.Numeric) (hr : ∀ y ∈ x.rightMoves, y⁻¹.Numeric) (hl' : ∀ y ∈ x.leftMoves, 0 < y → y * y⁻¹ ≈ 1) (hr' : ∀ y ∈ x.rightMoves, y * y⁻¹ ≈ 1) : (∀ y ∈ x⁻¹.leftMoves, x * y < 1) ∧ ∀ y ∈ x⁻¹.rightMoves, 1 < x * y

theorem Surreal.Division.numeric_inv {x : IGame} [x.Numeric] (hx : 0 < x) (hl : ∀ y ∈ x.leftMoves, 0 < y → y⁻¹.Numeric) (hr : ∀ y ∈ x.rightMoves, y⁻¹.Numeric) (hl' : ∀ y ∈ x.leftMoves, 0 < y → y * y⁻¹ ≈ 1) (hr' : ∀ y ∈ x.rightMoves, y * y⁻¹ ≈ 1) : x⁻¹.Numeric

theorem Surreal.Division.option_mul_inv_lt {x : IGame} [x.Numeric] (hx : 0 < x) (hl : ∀ y ∈ x.leftMoves, 0 < y → y⁻¹.Numeric) (hr : ∀ y ∈ x.rightMoves, y⁻¹.Numeric) (hl' : ∀ y ∈ x.leftMoves, 0 < y → y * y⁻¹ ≈ 1) (hr' : ∀ y ∈ x.rightMoves, y * y⁻¹ ≈ 1) : (∀ y ∈ (x * x⁻¹).leftMoves, y < 1) ∧ ∀ y ∈ (x * x⁻¹).rightMoves, 1 < y

theorem Surreal.Division.mul_inv_self {x : IGame} [x.Numeric] (hx : 0 < x) (hl : ∀ y ∈ x.leftMoves, 0 < y → y⁻¹.Numeric) (hr : ∀ y ∈ x.rightMoves, y⁻¹.Numeric) (hl' : ∀ y ∈ x.leftMoves, 0 < y → y * y⁻¹ ≈ 1) (hr' : ∀ y ∈ x.rightMoves, y * y⁻¹ ≈ 1) : x * x⁻¹ ≈ 1

@[irreducible]

theorem Surreal.Division.main {x : IGame} [x.Numeric] (hx : 0 < x) : x⁻¹.Numeric ∧ x * x⁻¹ ≈ 1

Instances and corollaries

instance IGame.Numeric.inv (x : IGame) [x.Numeric] : x⁻¹.Numeric

instance IGame.Numeric.div (x y : IGame) [x.Numeric] [y.Numeric] : (x / y).Numeric

instance IGame.Numeric.ratCast (q : ℚ) : (↑q).Numeric

instance IGame.Numeric.invOption (x y a : IGame) [x.Numeric] [y.Numeric] [a.Numeric] : (invOption x y a).Numeric

theorem IGame.Numeric.mul_inv_cancel {x : IGame} [x.Numeric] (hx : ¬x ≈ 0) : x * x⁻¹ ≈ 1

theorem IGame.Numeric.inv_mul_cancel {x : IGame} [x.Numeric] (hx : ¬x ≈ 0) : x⁻¹ * x ≈ 1

noncomputable instance Surreal.instField : Field Surreal

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Surreal.mk_inv (x : IGame) [x.Numeric] : mk x⁻¹ = (mk x)⁻¹

@[simp]

theorem Surreal.mk_div (x y : IGame) [x.Numeric] [y.Numeric] : mk (x / y) = mk x / mk y

@[simp]

theorem Surreal.mk_ratCast (q : ℚ) : mk ↑q = ↑q

@[simp]

theorem Surreal.toGame_ratCast (q : ℚ) : toGame ↑q = ↑q

@[simp]

theorem IGame.Numeric.inv_pos {x : IGame} [x.Numeric] : 0 < x⁻¹ ↔ 0 < x

@[simp]

theorem IGame.Numeric.inv_neg {x : IGame} [x.Numeric] : x⁻¹ < 0 ↔ x < 0

@[simp]

theorem IGame.Numeric.inv_nonneg {x : IGame} [x.Numeric] : 0 ≤ x⁻¹ ↔ 0 ≤ x

@[simp]

theorem IGame.Numeric.inv_nonpos {x : IGame} [x.Numeric] : x⁻¹ ≤ 0 ↔ x ≤ 0

theorem IGame.Numeric.lt_div_iff {x y z : IGame} [x.Numeric] [y.Numeric] [z.Numeric] (hz : 0 < z) : x < y / z ↔ x * z < y

theorem IGame.Numeric.div_lt_iff {x y z : IGame} [x.Numeric] [y.Numeric] [z.Numeric] (hy : 0 < y) : x / y < z ↔ x < z * y

theorem IGame.Numeric.lt_div_iff_of_neg {x y z : IGame} [x.Numeric] [y.Numeric] [z.Numeric] (hz : z < 0) : x < y / z ↔ y < x * z

theorem IGame.Numeric.div_lt_iff_of_neg {x y z : IGame} [x.Numeric] [y.Numeric] [z.Numeric] (hy : y < 0) : x / y < z ↔ z * y < x

@[simp]

theorem IGame.ratCast_le {m n : ℚ} : ↑m ≤ ↑n ↔ m ≤ n

@[simp]

theorem IGame.ratCast_lt {m n : ℚ} : ↑m < ↑n ↔ m < n

theorem IGame.ratCast_strictMono : StrictMono Rat.cast

@[simp]

theorem IGame.ratCast_inj {m n : ℚ} : ↑m = ↑n ↔ m = n

@[simp]

theorem IGame.ratCast_equiv {m n : ℚ} : ↑m ≈ ↑n ↔ m = n

theorem IGame.ratCast_natCast_equiv (n : ℕ) : ↑↑n ≈ ↑n

theorem IGame.ratCast_intCast_equiv (n : ℤ) : ↑↑n ≈ ↑n

theorem IGame.ratCast_add_equiv (m n : ℚ) : ↑(m + n) ≈ ↑m + ↑n

theorem IGame.ratCast_sub_equiv (m n : ℚ) : ↑(m - n) ≈ ↑m - ↑n

theorem IGame.ratCast_mul_equiv (m n : ℚ) : ↑(m * n) ≈ ↑m * ↑n

theorem IGame.ratCast_inv_equiv (m : ℚ) : ↑m⁻¹ ≈ (↑m)⁻¹

theorem IGame.ratCast_div_equiv (m n : ℚ) : ↑(m / n) ≈ ↑m / ↑n

@[simp]

theorem IGame.zero_lt_ratCast {q : ℚ} : 0 < ↑q ↔ 0 < q

@[simp]

theorem IGame.ratCast_lt_zero {q : ℚ} : ↑q < 0 ↔ q < 0

@[simp]

theorem IGame.zero_le_ratCast {q : ℚ} : 0 ≤ ↑q ↔ 0 ≤ q

@[simp]

theorem IGame.ratCast_le_zero {q : ℚ} : ↑q ≤ 0 ↔ q ≤ 0

theorem IGame.equiv_ratCast_of_mem_leftMoves_ratCast {q : ℚ} {x : IGame} (hx : x ∈ (↑q).leftMoves) : ∃ r < q, x ≈ ↑r

Every left option of a rational number is equivalent to a smaller rational number.

theorem IGame.equiv_ratCast_of_mem_rightMoves_ratCast {q : ℚ} {x : IGame} (hx : x ∈ (↑q).rightMoves) : ∃ (r : ℚ), q < r ∧ x ≈ ↑r

Every right option of a rational number is equivalent to a larger rational number.

@[simp]

theorem Game.ratCast_le {m n : ℚ} : ↑m ≤ ↑n ↔ m ≤ n

@[simp]

theorem Game.ratCast_lt {m n : ℚ} : ↑m < ↑n ↔ m < n

theorem Game.ratCast_strictMono : StrictMono Rat.cast

@[simp]

theorem Game.ratCast_inj {m n : ℚ} : ↑m = ↑n ↔ m = n

@[simp]

theorem Game.ratCast_natCast (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem Game.ratCast_intCast (n : ℤ) : ↑↑n = ↑n

@[simp]

theorem Game.ratCast_add (m n : ℚ) : ↑(m + n) = ↑m + ↑n

@[simp]

theorem Game.ratCast_sub (m n : ℚ) : ↑(m - n) = ↑m - ↑n

@[simp]

theorem Game.zero_lt_ratCast {q : ℚ} : 0 < ↑q ↔ 0 < q

@[simp]

theorem Game.ratCast_lt_zero {q : ℚ} : ↑q < 0 ↔ q < 0

@[simp]

theorem Game.zero_le_ratCast {q : ℚ} : 0 ≤ ↑q ↔ 0 ≤ q

@[simp]

theorem Game.ratCast_le_zero {q : ℚ} : ↑q ≤ 0 ↔ q ≤ 0