feat(set_theory/surreal/dyadic): define add_monoid_hom structure on d…

…yadic map (#11052)

The proof is mechanical and mostly requires unraveling definitions.

The above map cannot be extended to ring morphism as so far there's not multiplication structure on surreal numbers.

src/group_theory/submonoid/membership.lean

@@ -223,6 +223,8 @@ lemma powers_subset {n : M} {P : submonoid M} (h : n ∈ P) : powers n ≤ P :=
 @[simps] def pow (n : M) (m : ℕ) : powers n :=
 (powers_hom M n).mrange_restrict (multiplicative.of_add m)
 
+lemma pow_apply (n : M) (m : ℕ) : submonoid.pow n m = ⟨n ^ m, m, rfl⟩ := rfl
+
 /-- Logarithms from powers to natural numbers. -/
 def log [decidable_eq M] {n : M} (p : powers n) : ℕ :=
 nat.find $ (mem_powers_iff p.val n).mp p.prop
@@ -234,8 +236,8 @@ lemma pow_right_injective_iff_pow_injective {n : M} :
   function.injective (λ m : ℕ, n ^ m) ↔ function.injective (pow n) :=
 subtype.coe_injective.of_comp_iff (pow n)
 
-theorem log_pow_eq_self [decidable_eq M] {n : M} (h : function.injective (λ m : ℕ, n ^ m)) (m : ℕ) :
-  log (pow n m) = m :=
+@[simp] theorem log_pow_eq_self [decidable_eq M] {n : M} (h : function.injective (λ m : ℕ, n ^ m))
+  (m : ℕ) : log (pow n m) = m :=
 pow_right_injective_iff_pow_injective.mp h $ pow_log_eq_self _
 
 /-- The exponentiation map is an isomorphism from the additive monoid on natural numbers to powers
@@ -249,6 +251,9 @@ def pow_log_equiv [decidable_eq M] {n : M} (h : function.injective (λ m : ℕ,
   right_inv := pow_log_eq_self,
   map_mul' := λ _ _, by { simp only [pow, map_mul, of_add_add, to_add_mul] } }
 
+lemma log_mul [decidable_eq M] {n : M} (h : function.injective (λ m : ℕ, n ^ m))
+  (x y : powers (n : M)) : log (x * y) = log x + log y := (pow_log_equiv h).symm.map_mul x y
+
 theorem log_pow_int_eq_self {x : ℤ} (h : 1 < x.nat_abs) (m : ℕ) : log (pow x m) = m :=
 (pow_log_equiv (int.pow_right_injective h)).symm_apply_apply _
 

src/ring_theory/localization.lean

@@ -985,6 +985,9 @@ lemma mk_zero (b) : (mk 0 b : localization M) = 0 :=
 calc mk 0 b = mk 0 1 : mk_eq_mk_iff.mpr (r_of_eq (by simp))
 ... = 0 : by  unfold has_zero.zero localization.zero
 
+lemma lift_on_zero {p : Type*} (f : ∀ (a : R) (b : M), p) (H) : lift_on 0 f H = f 0 1 :=
+by rw [← mk_zero 1, lift_on_mk]
+
 private meta def tac := `[
 { intros,
   simp only [add_mk, localization.mk_mul, neg_mk, ← mk_zero 1],

src/set_theory/surreal/dyadic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Apurva Nakade
 -/
 import algebra.algebra.basic
-import group_theory.monoid_localization
+import ring_theory.localization
 import set_theory.surreal.basic
 
 /-!
@@ -178,33 +178,62 @@ begin
     linarith },
 end
 
-/-- The map `dyadic_map` sends ⟦⟨m, 2^n⟩⟧ to m • half ^ n. -/
-def dyadic_map (x : localization (submonoid.powers (2 : ℤ))) : surreal :=
-localization.lift_on x (λ x y, x • pow_half (submonoid.log y)) $
+/-- The additive monoid morphism `dyadic_map` sends ⟦⟨m, 2^n⟩⟧ to m • half ^ n. -/
+def dyadic_map : localization.away (2 : ℤ) →+ surreal :=
+{ to_fun :=
+  λ x, localization.lift_on x (λ x y, x • pow_half (submonoid.log y)) $
+  begin
+    intros m₁ m₂ n₁ 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 one_lt_two,
+      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,
+  map_zero' := localization.lift_on_zero _ _,
+  map_add' := λ x y, localization.induction_on₂ x y $
+  begin
+    rintro ⟨a, ⟨b, ⟨b', rfl⟩⟩⟩ ⟨c, ⟨d, ⟨d', rfl⟩⟩⟩,
+    have h₂ : 1 < (2 : ℤ).nat_abs, from one_lt_two,
+    have hpow₂ := submonoid.log_pow_int_eq_self h₂,
+    simp_rw submonoid.pow_apply at hpow₂,
+    simp_rw [localization.add_mk, localization.lift_on_mk, subtype.coe_mk,
+      submonoid.log_mul (int.pow_right_injective h₂), hpow₂],
+    calc (2 ^ b' * c + 2 ^ d' * a) • pow_half (b' + d')
+        = (c * 2 ^ b') • pow_half (b' + d') + (a * 2 ^ d') • pow_half (d' + b')
+        : by simp only [add_smul, mul_comm,add_comm]
+    ... = c • pow_half d' + a • pow_half b' : by simp only [zsmul_pow_two_pow_half]
+    ... = a • pow_half b' + c • pow_half d' : add_comm _ _,
+  end }
+
+@[simp] lemma dyadic_map_apply (m : ℤ) (p : submonoid.powers (2 : ℤ)) :
+  dyadic_map (is_localization.mk' (localization (submonoid.powers 2)) m p) =
+  m • pow_half (submonoid.log p) :=
 begin
-  intros m₁ m₂ n₁ 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 }
+  rw ← localization.mk_eq_mk',
+  refl,
 end
 
+@[simp] lemma dyadic_map_apply_pow (m : ℤ) (n : ℕ) :
+  dyadic_map (is_localization.mk' (localization (submonoid.powers 2)) m (submonoid.pow 2 n)) =
+  m • pow_half n :=
+by rw [dyadic_map_apply, @submonoid.log_pow_int_eq_self 2 one_lt_two]
+
 /-- 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 show that the map from dyadic rationals to surreals is injective
 
 -- TODO map the reals into the surreals, using dyadic Dedekind cuts
 -- TODO show this is a group homomorphism, and injective