[Merged by Bors] - feat(set_theory/surreal): add dyadic surreals

docs/references.bib

@@ -355,6 +355,12 @@ @Book{            conway2001
   mrnumber      = {1803095}
 }
 
+@Misc{            schleicher_stoll,
+  author        = {Dierk Schleicher and Michael Stoll},
+  title         = {An introduction to {C}onway's games and numbers},
+  url           = {http://www.cs.cmu.edu/afs/cs/academic/class/15859-s05/www/lecture-notes/comb-games-notes.pdf}
+}
+
 @InProceedings{   deligne_formulaire,
   author        = {Deligne, P.},
   title         = {Courbes elliptiques: formulaire d'apr\`es {J}. {T}ate},

src/set_theory/pgame.lean

@@ -420,9 +420,13 @@ local infix ` ≈ ` := pgame.equiv
 @[trans] theorem equiv_trans {x y z} : x ≈ y → y ≈ z → x ≈ z
 | ⟨xy, yx⟩ ⟨yz, zy⟩ := ⟨le_trans xy yz, le_trans zy yx⟩
 
+@[trans]
 theorem lt_of_lt_of_equiv {x y z} (h₁ : x < y) (h₂ : y ≈ z) : x < z := lt_of_lt_of_le h₁ h₂.1
+@[trans]
 theorem le_of_le_of_equiv {x y z} (h₁ : x ≤ y) (h₂ : y ≈ z) : x ≤ z := le_trans h₁ h₂.1
+@[trans]
 theorem lt_of_equiv_of_lt {x y z} (h₁ : x ≈ y) (h₂ : y < z) : x < z := lt_of_le_of_lt h₁.1 h₂
+@[trans]
 theorem le_of_equiv_of_le {x y z} (h₁ : x ≈ y) (h₂ : y ≤ z) : x ≤ z := le_trans h₁.1 h₂
 
 theorem le_congr {x₁ y₁ x₂ y₂} : x₁ ≈ x₂ → y₁ ≈ y₂ → (x₁ ≤ y₁ ↔ x₂ ≤ y₂)
@@ -1021,4 +1025,35 @@ or.inl ⟨⟨0, zero_lt_one⟩, (by split; rintros ⟨⟩)⟩
 /-- The pre-game `ω`. (In fact all ordinals have game and surreal representatives.) -/
 def omega : pgame := ⟨ulift ℕ, pempty, λ n, ↑n.1, pempty.elim⟩
 
+theorem zero_lt_one : (0 : pgame) < 1 :=
+begin
+  rw lt_def,
+  left,
+  use ⟨punit.star, by split; rintro ⟨ ⟩⟩,
+end
+
+/-- The pre-game `half` is defined as `{0 | 1}`. -/
+def half : pgame := ⟨punit, punit, 0, 1⟩
+
+@[simp] lemma half_move_left : half.move_left punit.star = 0 := rfl
+
+@[simp] lemma half_move_right : half.move_right punit.star = 1 := rfl
+
+theorem zero_lt_half : 0 < half :=
+begin
+  rw lt_def,
+  left,
+  use punit.star,
+  split; rintro ⟨ ⟩,
+end
+
+theorem half_lt_one : half < 1 :=
+begin
+  rw lt_def,
+  right,
+  use punit.star,
+  split; rintro ⟨ ⟩,
+  exact zero_lt_one,
+end
+
 end pgame

src/set_theory/surreal.lean → src/set_theory/surreal/basic.lean

@@ -25,19 +25,19 @@ Surreal numbers inherit the relations `≤` and `<` from games, and these relati
 of a partial order (recall that `x < y ↔ x ≤ y ∧ ¬ y ≤ x` did not hold for games).
 
 ## Algebraic operations
-At this point, we have defined addition and negation (from pregames), and shown that surreals form
-an additive semigroup. It would be very little work to finish showing that the surreals form an
-ordered commutative group.
-
-## Embeddings
-It would be nice projects to define the group homomorphism `surreal → game`, and also `ℤ → surreal`,
-and then the homomorphic inclusion of the dyadic rationals into surreals, and finally
-via dyadic Dedekind cuts the homomorphic inclusion of the reals into the surreals.
+We show that the surreals form a linear ordered commutative group.
 
 One can also map all the ordinals into the surreals!
 
+### Multiplication of surreal numbers
+The definition of multiplication for surreal numbers is surprisingly difficult and is currently
+missing in the library. A sample proof can be found in Theorem 3.8 in the second reference below.
+The difficulty lies in the length of the proof and the number of theorems that need to proven
+simultaneously. This will make for a fun and challenging project.
+
 ## References
 * [Conway, *On numbers and games*][conway2001]
+* [Schleicher, Stoll, *An introduction to Conway's games and numbers*][schleicher_stoll]
 -/
 
 universes u
@@ -198,6 +198,47 @@ theorem numeric_nat : Π (n : ℕ), numeric n
 theorem numeric_omega : numeric omega :=
 ⟨by rintros ⟨⟩ ⟨⟩, λ i, numeric_nat i.down, by rintros ⟨⟩⟩
 
+/-- The pre-game `half` is numeric. -/
+theorem numeric_half : numeric half :=
+begin
+  split,
+  { rintros ⟨ ⟩ ⟨ ⟩,
+    exact zero_lt_one },
+  split; rintro ⟨ ⟩,
+  { exact numeric_zero },
+  { exact numeric_one }
+end
+
+theorem half_add_half_equiv_one : half + half ≈ 1 :=
+begin
+  split; rw le_def; split,
+  { rintro (⟨⟨ ⟩⟩ | ⟨⟨ ⟩⟩),
+    { right,
+      use (sum.inr punit.star),
+      calc ((half + half).move_left (sum.inl punit.star)).move_right (sum.inr punit.star)
+          = (half.move_left punit.star + half).move_right (sum.inr punit.star) : by fsplit
+      ... = (0 + half).move_right (sum.inr punit.star) : by fsplit
+      ... ≈ 1 : zero_add_equiv 1
+      ... ≤ 1 : pgame.le_refl 1 },
+    { right,
+      use (sum.inl punit.star),
+      calc ((half + half).move_left (sum.inr punit.star)).move_right (sum.inl punit.star)
+          = (half + half.move_left punit.star).move_right (sum.inl punit.star) : by fsplit
+      ... = (half + 0).move_right (sum.inl punit.star) : by fsplit
+      ... ≈ 1 : add_zero_equiv 1
+      ... ≤ 1 : pgame.le_refl 1 } },
+  { rintro ⟨ ⟩ },
+  { rintro ⟨ ⟩,
+    left,
+    use (sum.inl punit.star),
+    calc 0 ≤ half : le_of_lt numeric_zero numeric_half zero_lt_half
+    ... ≈ 0 + half : (zero_add_equiv half).symm
+    ... = (half + half).move_left (sum.inl punit.star) : by fsplit },
+  { rintro (⟨⟨ ⟩⟩ | ⟨⟨ ⟩⟩); left,
+    { exact ⟨sum.inr punit.star, le_of_le_of_equiv (pgame.le_refl _) (add_zero_equiv _).symm⟩ },
+    { exact ⟨sum.inl punit.star, le_of_le_of_equiv (pgame.le_refl _) (zero_add_equiv _).symm⟩ } }
+end
+
 end pgame
 
 /-- The equivalence on numeric pre-games. -/
@@ -295,16 +336,6 @@ noncomputable instance : linear_ordered_add_comm_group surreal :=
 -- We conclude with some ideas for further work on surreals; these would make fun projects.
 
 -- TODO define the inclusion of groups `surreal → game`
-
--- TODO define the dyadic rationals, and show they map into the surreals via the formula
---   m / 2^n ↦ { (m-1) / 2^n | (m+1) / 2^n }
--- TODO show this is a group homomorphism, and injective
-
--- TODO map the reals into the surreals, using dyadic Dedekind cuts
--- TODO show this is a group homomorphism, and injective
-
 -- TODO define the field structure on the surreals
--- TODO show the maps from the dyadic rationals and from the reals
--- into the surreals are multiplicative
 
 end surreal

src/set_theory/surreal/dyadic.lean

@@ -0,0 +1,214 @@
+/-
+Copyright (c) 2021 Apurva Nakade. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Apurva Nakade
+-/
+import set_theory.surreal.basic
+import ring_theory.localization
+
+/-!
+# Dyadic numbers
+Dyadic numbers are obtained by localizing ℤ away from 2. They are the initial object in the category
+of rings with no 2-torsion.
+
+## Dyadic surreal numbers
+We construct dyadic surreal numbers using the canonical map from ℤ[2 ^ {-1}] to surreals.
+As we currently do not have a ring structure on `surreal` we construct this map explicitly. Once we
+have the ring structure, this map can be constructed directly by sending `2 ^ {-1}` to `half`.
+
+## Embeddings
+The above construction gives us an abelian group embedding of ℤ into `surreal`. The goal is to
+extend this to an embedding of dyadic rationals into `surreal` and use Cauchy sequences of dyadic
+rational numbers to construct an ordered field embedding of ℝ into `surreal`.
+-/
+
+universes u
+
+local infix ` ≈ ` := pgame.equiv
+
+namespace pgame
+
+/-- For a natural number `n`, the pre-game `pow_half (n + 1)` is recursively defined as
+`{ 0 | pow_half n }`. These are the explicit expressions of powers of `half`. By definition, we have
+ `pow_half 0 = 0` and `pow_half 1 = half` and we prove later on that
+`pow_half (n + 1) + pow_half (n + 1) ≈ pow_half n`.-/
+def pow_half : ℕ → pgame
+| 0       := mk punit pempty 0 pempty.elim
+| (n + 1) := mk punit punit 0 (λ _, pow_half n)
+
+@[simp] lemma pow_half_left_moves {n} : (pow_half n).left_moves = punit :=
+by cases n; refl
+
+@[simp] lemma pow_half_right_moves {n} : (pow_half (n + 1)).right_moves = punit :=
+by cases n; refl
+
+@[simp] lemma pow_half_move_left {n i} : (pow_half n).move_left i = 0 :=
+by cases n; cases i; refl
+
+@[simp] lemma pow_half_move_right {n i} : (pow_half (n + 1)).move_right i = pow_half n :=
+by cases n; cases i; refl
+
+lemma pow_half_move_left' (n) :
+  (pow_half n).move_left (equiv.cast (pow_half_left_moves.symm) punit.star) = 0 :=
+by simp only [eq_self_iff_true, pow_half_move_left]
+
+lemma pow_half_move_right' (n) :
+  (pow_half (n + 1)).move_right (equiv.cast (pow_half_right_moves.symm) punit.star) = pow_half n :=
+by simp only [pow_half_move_right, eq_self_iff_true]
+
+/-- For all natural numbers `n`, the pre-games `pow_half n` are numeric. -/
+theorem numeric_pow_half {n} : (pow_half n).numeric :=
+begin
+  induction n with n hn,
+  { exact numeric_one },
+  { split,
+    { rintro ⟨ ⟩ ⟨ ⟩,
+      dsimp only [pi.zero_apply],
+      rw ← pow_half_move_left' n,
+      apply hn.move_left_lt },
+    { exact ⟨λ _, numeric_zero, λ _, hn⟩ } }
+end
+
+theorem pow_half_succ_lt_pow_half {n : ℕ} : pow_half (n + 1) < pow_half n :=
+(@numeric_pow_half (n + 1)).lt_move_right punit.star
+
+theorem pow_half_succ_le_pow_half {n : ℕ} : pow_half (n + 1) ≤ pow_half n :=
+le_of_lt numeric_pow_half numeric_pow_half pow_half_succ_lt_pow_half
+
+theorem zero_lt_pow_half {n : ℕ} : 0 < pow_half n :=
+by cases n; rw lt_def_le; use ⟨punit.star, pgame.le_refl 0⟩
+
+theorem zero_le_pow_half {n : ℕ} : 0 ≤ pow_half n :=
+le_of_lt numeric_zero numeric_pow_half zero_lt_pow_half
+
+theorem add_pow_half_succ_self_eq_pow_half {n} : pow_half (n + 1) + pow_half (n + 1) ≈ pow_half n :=
+begin
+  induction n with n hn,
+  { exact half_add_half_equiv_one },
+  { split; rw le_def_lt; split,
+    { rintro (⟨⟨ ⟩⟩ | ⟨⟨ ⟩⟩),
+      { calc 0 + pow_half (n.succ + 1) ≈ pow_half (n.succ + 1) : zero_add_equiv _
+                                   ... < pow_half n.succ       : pow_half_succ_lt_pow_half },
+      { calc pow_half (n.succ + 1) + 0 ≈ pow_half (n.succ + 1) : add_zero_equiv _
+                                   ... < pow_half n.succ       : pow_half_succ_lt_pow_half } },
+    { rintro ⟨ ⟩,
+      rw lt_def_le,
+      right,
+      use sum.inl punit.star,
+      calc pow_half (n.succ) + pow_half (n.succ + 1)
+          ≤ pow_half (n.succ) + pow_half (n.succ) : add_le_add_left pow_half_succ_le_pow_half
+      ... ≈ pow_half n                            : hn },
+    { rintro ⟨ ⟩,
+      calc 0 ≈ 0 + 0                                        : (add_zero_equiv _).symm
+        ... ≤ pow_half (n.succ + 1) + 0                     : add_le_add_right zero_le_pow_half
+        ... < pow_half (n.succ + 1) + pow_half (n.succ + 1) : add_lt_add_left zero_lt_pow_half },
+    { rintro (⟨⟨ ⟩⟩ | ⟨⟨ ⟩⟩),
+      { calc pow_half n.succ
+            ≈ pow_half n.succ + 0                           : (add_zero_equiv _).symm
+        ... < pow_half (n.succ) + pow_half (n.succ + 1)     : add_lt_add_left zero_lt_pow_half },
+      { calc pow_half n.succ
+            ≈ 0 + pow_half n.succ                           : (zero_add_equiv _).symm
+        ... < pow_half (n.succ + 1) + pow_half (n.succ)     : add_lt_add_right zero_lt_pow_half }}}
+end
+
+end pgame
+
+namespace surreal
+open pgame
+
+/-- The surreal number `half`. -/
+def half : surreal := ⟦⟨pgame.half, pgame.numeric_half⟩⟧
+
+/-- Powers of the surreal number `half`. -/
+def pow_half (n : ℕ) : surreal := ⟦⟨pgame.pow_half n, pgame.numeric_pow_half⟩⟧
+
+@[simp] lemma pow_half_zero : pow_half 0 = 1 := rfl
+
+@[simp] lemma pow_half_one : pow_half 1 = half := rfl
+
+@[simp] theorem add_half_self_eq_one : half + half = 1 :=
+quotient.sound pgame.half_add_half_equiv_one
+
+lemma double_pow_half_succ_eq_pow_half (n : ℕ) : 2 • pow_half n.succ = pow_half n :=
+begin
+  rw two_nsmul,
+  apply quotient.sound,
+  exact pgame.add_pow_half_succ_self_eq_pow_half,
+end
+
+lemma nsmul_pow_two_pow_half (n : ℕ) : 2 ^ n • pow_half n = 1 :=
+begin
+  induction n with n hn,
+  { simp only [nsmul_one, pow_half_zero, nat.cast_one, pow_zero] },
+  { rw [← hn, ← double_pow_half_succ_eq_pow_half n, smul_smul (2^n) 2 (pow_half n.succ),
+        mul_comm, pow_succ] }
+end
+
+lemma nsmul_pow_two_pow_half' (n k : ℕ) : 2 ^ n • pow_half (n + k) = pow_half k :=
+begin
+  induction k with k hk,
+  { simp only [add_zero, surreal.nsmul_pow_two_pow_half, nat.nat_zero_eq_zero, eq_self_iff_true,
+               surreal.pow_half_zero] },
+  { rw [← double_pow_half_succ_eq_pow_half (n + k), ← double_pow_half_succ_eq_pow_half k,
+        smul_algebra_smul_comm] at hk,
+    rwa ← (gsmul_eq_gsmul_iff' two_ne_zero) }
+end
+
+lemma nsmul_int_pow_two_pow_half (m : ℤ) (n k : ℕ) :
+  (m * 2 ^ n) • pow_half (n + k) = m • pow_half k :=
+begin
+  rw mul_gsmul,
+  congr,
+  norm_cast,
+  exact nsmul_pow_two_pow_half' n k,
+end
+
+lemma dyadic_aux {m₁ m₂ : ℤ} {y₁ y₂ : ℕ} (h₂ : m₁ * (2 ^ y₁) = m₂ * (2 ^ y₂)) :
+  m₁ • pow_half y₂ = m₂ • pow_half y₁ :=
+begin
+  revert m₁ m₂,
+  wlog h : y₁ ≤ y₂,
+  intros m₁ m₂ h₂,
+  obtain ⟨c, rfl⟩ := le_iff_exists_add.mp h,
+  rw [add_comm, pow_add, ← mul_assoc, mul_eq_mul_right_iff] at h₂,
+  cases h₂,
+  { rw [h₂, add_comm, nsmul_int_pow_two_pow_half m₂ c y₁] },
+  { have := nat.one_le_pow y₁ 2 nat.succ_pos',
+    linarith },
+end
+
+/-- The map `dyadic_map` sends ⟦⟨m, 2^n⟩⟧ to m • half ^ n. -/
+def dyadic_map (x : localization (submonoid.powers (2 : ℤ))) : surreal :=
+quotient.lift_on' x (λ x : _ × _, x.1 • pow_half (submonoid.log x.2)) $
+begin
+  rintros ⟨m₁, n₁⟩ ⟨m₂, n₂⟩ h₁,
+  obtain ⟨⟨n₃, y₃, hn₃⟩, h₂⟩ := localization.r_iff_exists.mp h₁,
+  simp only [subtype.coe_mk, mul_eq_mul_right_iff] at h₂,
+  cases h₂,
+  { simp only,
+    obtain ⟨a₁, ha₁⟩ := n₁.prop,
+    obtain ⟨a₂, ha₂⟩ := n₂.prop,
+    have hn₁ : n₁ = submonoid.pow 2 a₁ := subtype.ext ha₁.symm,
+    have hn₂ : n₂ = submonoid.pow 2 a₂ := subtype.ext ha₂.symm,
+    have h₂ : 1 < (2 : ℤ).nat_abs, from dec_trivial,
+    rw [hn₁, hn₂, submonoid.log_pow_int_eq_self h₂, submonoid.log_pow_int_eq_self h₂],
+    apply dyadic_aux,
+    rwa [ha₁, ha₂] },
+  { have := nat.one_le_pow y₃ 2 nat.succ_pos',
+    linarith }
+end
+
+/-- We define dyadic surreals as the range of the map `dyadic_map`. -/
+def dyadic : set surreal := set.range dyadic_map
+
+-- We conclude with some ideas for further work on surreals; these would make fun projects.
+
+-- TODO show that the map from dyadic rationals to surreals is a group homomorphism, and injective
+
+-- TODO map the reals into the surreals, using dyadic Dedekind cuts
+-- TODO show this is a group homomorphism, and injective
+
+-- TODO show the maps from the dyadic rationals and from the reals
+-- into the surreals are multiplicative
+
+end surreal