Simplest form of a dyadic number

Stream: general

[Violeta Hernández]

Given x : Localization.Away (2 : ℤ), how can I recover the minimal m and n with x = m / 2^n?

[Aaron Liu]

I thought about using docs#Localization.awayLift, but it's noncomputable...

[Bhavik Mehta]

The module doc of that file suggests docs#exists_reduced_fraction' would be helpful

[Violeta Hernández]

It's a shame this operation isn't computable, but it's no deal breaker.

[Violeta Hernández]

(Speaking of, it'd be nice to have a DecidableEq insteance on this type too.)

[Aaron Liu]

This solves your problem

import Mathlib

def toRat {n : ℤ} [NeZero n] (f : Localization.Away n) : ℚ :=
  f.lift (fun p ↦ p.fst / p.snd) fun a b hab ↦ by
    obtain ⟨a₁, a₂, ha₂⟩ := a
    obtain ⟨b₁, b₂, hb₂⟩ := b
    obtain ⟨⟨u, hu⟩, v, hn, hd⟩ := hab
    dsimp at *
    have hs {s} (hs : s ∈ Submonoid.powers n) : s ≠ 0 := by
      rintro rfl
      apply powers_le_nonZeroDivisors_of_noZeroDivisors NeZero.out at hs
      exact zero_not_mem_nonZeroDivisors hs
    rw [div_eq_div_iff (Int.cast_ne_zero.mpr (hs ha₂)) (Int.cast_ne_zero.mpr (hs hb₂))]
    apply mul_right_injective₀ (Int.cast_ne_zero.mpr (hs hu))
    dsimp
    norm_cast
    rw [mul_left_comm, hd, mul_comm, ← mul_assoc, hn, mul_right_comm]

[Violeta Hernández]

Oh, clever! So I can pass to ℚ and then get the simplest form by using the existing API on rationals.

[Violeta Hernández]

It'd be nice to have this as well

theorem den_toRat_mem_powers {n : ℤ} (hn : 0 < n) (x : Localization.Away n) :
    ((@toRat n ⟨hn.ne'⟩ x).den : ℤ) ∈ Submonoid.powers n := sorry

This should follow from the fact that if m / n is a (not necessarily reduced) fraction where n is a power of k, then its (reduced) denominator is also a power of k. Do we have anything like this?

[Ruben Van de Velde]

Probably you want something like (a/b).den \dvd b

[Ruben Van de Velde]

There's docs#Rat.den_dvd

[Violeta Hernández]

Awesome!

[Violeta Hernández]

I'm thinking about how to PR this. Presumably we can do something slightly more general? Namely, we can show that any localization of ℤ induces a computable monomorphism into ℚ. And we can use this to build the corresponding DecidableEq instance.

[Ruben Van de Velde]

Violeta Hernández said:

the fact that if m / n is a (not necessarily reduced) fraction where n is a power of k, then its (reduced) denominator is also a power of k

(Presumably k is prime)

[Violeta Hernández]

Violeta Hernández said:

I'm thinking about how to PR this. Presumably we can do something slightly more general? Namely, we can show that any localization of ℤ induces a computable monomorphism into ℚ. And we can use this to build the corresponding DecidableEq instance.

Would this be desirable in Mathlib?

[Eric Wieser]

I assume the computability issue arises from IsLocalization not actually holding the data needed to do anything computably?

[Aaron Liu]

The issue is that IsUnit (f r) does not give the data necessary to construct the inverse.

[Eric Wieser]

Is that from docs#IsLocalHom ?

[Johan Commelin]

I think that dyadic numbers are a sufficiently special case that we might want to treat them separately from general localizations.

[Violeta Hernández]

Aaron Liu said:

The issue is that IsUnit (f r) does not give the data necessary to construct the inverse.

That seems like a simple fix, could we just make a version of this function where you give an inverse explicitly?

[Aaron Liu]

Violeta Hernández said:

Aaron Liu said:

The issue is that IsUnit (f r) does not give the data necessary to construct the inverse.

That seems like a simple fix, could we just make a version of this function where you give an inverse explicitly?

Is this ok?

import Mathlib

def Localization.Away.lift' {R P : Type*} [CommSemiring R] [CommSemiring P] (f : R →+* P)
    (r : R) (hinv : ∀ (u : Submonoid.powers r), Invertible (f u)) : Away r →+* P where
  toFun := OreLocalization.liftExpand (fun a b ↦ f a /ₚ unitOfInvertible (f b)) fun a b s ht ↦ by
    apply divp_eq_divp_iff.mpr
    simp_rw [val_unitOfInvertible, smul_eq_mul, map_mul]
    -- ac_rfl -- why does this fail?
    ring
  map_one' := by
    rw [OreLocalization.one_def, OreLocalization.liftExpand_of]
    apply divp_eq_iff_mul_eq.mpr
    simp
  map_mul' := by
    apply OreLocalization.ind
    intro a₁ a₂
    apply OreLocalization.ind
    intro b₁ b₂
    simp_rw [OreLocalization.oreDiv_mul_oreDiv, OreLocalization.liftExpand_of]
    field_simp
    rw [mul_comm (f a₁), mul_assoc (f b₁), ← mul_assoc (f a₁), ← map_mul f a₁]
    rw [mul_comm a₁, OreLocalization.ore_eq, map_mul]
    -- ac_rfl -- why does this fail?
    ring
  map_zero' := by
    simp_rw [OreLocalization.zero_def, OreLocalization.liftExpand_of]
    apply divp_eq_iff_mul_eq.mpr
    simp
  map_add' := by
    apply OreLocalization.ind
    intro a₁ a₂
    apply OreLocalization.ind
    intro b₁ b₂
    simp_rw [OreLocalization.oreDiv_add_oreDiv, OreLocalization.liftExpand_of]
    simp_rw [Submonoid.smul_def, smul_eq_mul]
    -- why does this require `CommRing` when `CommSemiring` should do just fine
    -- rw [Units.divp_add_divp]
    apply (@mul_right_inj_of_invertible _ _ _ _ _ ((hinv a₂).mul (hinv b₂))).mp
    field_simp
    simp_rw [divp, val_inv_unitOfInvertible, mul_add, add_mul, ← mul_assoc]
    simp_rw [mul_right_comm _ _ ⅟_]
    rw [invOf_mul_cancel_right, mul_invOf_self, one_mul]
    simp_rw [← map_mul, ← map_add]
    rw [mul_assoc (a₂ * b₁), mul_mul_mul_comm, mul_comm (a₂ : R), OreLocalization.ore_eq]
    apply congrArg f
    ring

def Localization.Away.lift {R P : Type*} [CommSemiring R] [DecidableEq R] [CommSemiring P] (f : R →+* P)
    (r : R) (hinv : Invertible (f r)) : Away r →+* P :=
  Localization.Away.lift' f r
    fun u ↦ (invertiblePow (f r) (Submonoid.log u)).copy _ <| by
      rw [← map_pow, ← Submonoid.pow_coe, Submonoid.pow_log_eq_self]

[Violeta Hernández]

Nice!

[Violeta Hernández]

(deleted)

[Violeta Hernández]

@Aaron Liu Do you think you could PR this? It'd be really helpful.

[Aaron Liu]

#22662