English
There is a canonical additive monoid homomorphism from Localization Away from 2 to Surreal, sending the class of m/(p) to m · powHalf(log p) for p ∈ powers(2).
Русский
Существует каноническое отображение из локализации вдали от 2 в множество сюрреальных чисел, сохраняющее аддитивность и отправляющее класс m/(p) в m · powHalf(log p) при p ∈ powers(2).
LaTeX
$$$$ \mathrm{dyadicMap}\big(\mathrm{IsLocalization.mk}'(\mathrm{Localization}(\mathrm{Submonoid.powers}(2)))\ m\ p\big) = m \cdot powHalf(\log p). $$$$
Lean4
/-- The additive monoid morphism `dyadicMap` sends ⟦⟨m, 2^n⟩⟧ to m • half ^ n. -/
noncomputable def dyadicMap : Localization.Away (2 : ℤ) →+ Surreal
where
toFun
x :=
(Localization.liftOn x fun x y => x * powHalf (Submonoid.log y)) <|
by
intro m₁ m₂ n₁ n₂ h₁
obtain ⟨⟨n₃, y₃, hn₃⟩, h₂⟩ := Localization.r_iff_exists.mp h₁
simp only [mul_eq_mul_left_iff] at h₂
cases h₂
· obtain ⟨a₁, ha₁⟩ := n₁.prop
obtain ⟨a₂, ha₂⟩ := n₂.prop
simp only at ha₁ ha₂ ⊢
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 : ℤ).natAbs := 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₂, mul_comm, mul_comm m₂]
· have : (1 : ℤ) ≤ 2 ^ y₃ := mod_cast Nat.one_le_pow y₃ 2 Nat.succ_pos'
linarith
map_zero' := by simp_rw [Localization.liftOn_zero _ _, Int.cast_zero, zero_mul]
map_add' x
y :=
Localization.induction_on₂ x y <| by
rintro ⟨a, ⟨b, ⟨b', rfl⟩⟩⟩ ⟨c, ⟨d, ⟨d', rfl⟩⟩⟩
have h₂ : 1 < (2 : ℤ).natAbs := 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.liftOn_mk, Submonoid.log_mul (Int.pow_right_injective h₂), hpow₂]
simp only [Int.cast_add, Int.cast_mul, Int.cast_pow, Int.cast_ofNat]
calc
(2 ^ b' * c + 2 ^ d' * a) * powHalf (b' + d') =
(c * 2 ^ b') * powHalf (b' + d') + (a * 2 ^ d') * powHalf (d' + b') :=
by simp only [right_distrib, mul_comm, add_comm]
_ = c * powHalf d' + a * powHalf b' := by simp only [zsmul_pow_two_powHalf]
_ = a * powHalf b' + c * powHalf d' := add_comm _ _
