Concrete fraction ring of int

Stream: Is there code for X?

[Yakov Pechersky]

Do we have this?

import field_theory.ratfunc

example : ℚ ≃+* fraction_ring ℤ := sorry

I am building it up manually, juggling all sorts of gcd and dvd proofs. Perhaps we have this equivalence explicitly?

[Johan Commelin]

This should already be there, maybe the other way round. I'm quite sure.

[Johan Commelin]

grep gave me

src/ring_theory/localization.lean
1747:instance rat.is_fraction_ring : is_fraction_ring ℤ ℚ :=

[Yakov Pechersky]

Yes, but that is a Prop. But that does not give the "canonical" iso, right? Also, the API is a little missing here:

import field_theory.ratfunc

example : is_fraction_ring ℤ ℚ := rat.is_fraction_ring
example : is_fraction_ring ℤ (fraction_ring ℤ) := localization.is_localization -- library_search or suggest don't solve this

[Alex J. Best]

Maybe you can use https://leanprover-community.github.io/mathlib_docs/ring_theory/localization.html#is_localization.ring_equiv_of_ring_equiv to get the iso?

[Filippo A. E. Nuccio]

What do you call the "canonical" iso? When working on Dedekind domain, we somewhat convinced ourselves that having one proof of the iso was enough.

[Yakov Pechersky]

Here's what I have so far. It's a WIP, could be I stated something wrong:

import field_theory.ratfunc

lemma int.nat_abs_sign (z : ℤ) :
  z.sign.nat_abs = if z = 0 then 0 else 1 :=
by rcases z with (_ | _) | _; refl

lemma int.nat_abs_sign_of_nonzero {z : ℤ} (hz : z ≠ 0) :
  z.sign.nat_abs = 1 :=
by rw [int.nat_abs_sign, if_neg hz]

-- field of fractions ℚ
def fwd : ℚ → fraction_ring ℤ :=
λ q, localization.mk q.num
    ⟨q.denom, mem_non_zero_divisors_iff_ne_zero.mpr (by simpa using q.pos.ne')⟩

def rev : fraction_ring ℤ → ℚ :=
λ q, localization.rec (λ n d, ⟨int.sign d * n / n.gcd d,
  if n = 0 then 1 else int.nat_abs d / n.gcd d,
  begin
    split_ifs with hn hn,
    { exact zero_lt_one },
    cases d with d hd,
    rw [set_like.coe_mk],
    rw mem_non_zero_divisors_iff_ne_zero at hd,
    obtain ⟨_ | k, hk⟩ : n.gcd d ∣ d.nat_abs :=
      (int.nat_abs n).gcd_dvd_right (int.nat_abs d),
    { simpa [hd] using hk },
    replace hd : 0 < d.nat_abs,
    { contrapose! hd,
      simpa using hd },
    have hpos : 0 < n.gcd d := int.gcd_pos_of_non_zero_left d hn,
    simp [hk, mul_comm, nat.mul_div_assoc _ (dvd_refl _), hpos],
  end,
  begin
    split_ifs with hn hn,
    { simp },
    cases d with d hd,
    have hpos : 0 < n.gcd d := int.gcd_pos_of_non_zero_left d hn,
    rw mem_non_zero_divisors_iff_ne_zero at hd,
    rw [set_like.coe_mk, int.nat_abs_div _ _ ((n.gcd_dvd_left d).mul_left d.sign),
        int.nat_abs_mul, int.nat_abs_sign_of_nonzero hd, one_mul],
    exact nat.coprime_div_gcd_div_gcd hpos
  end⟩)
  begin
    rintro a c ⟨b, hb⟩ ⟨d, hd⟩ h,
    simp only [eq_rec_constant, set_like.coe_mk],
    rw localization.r_iff_exists at h,
    obtain ⟨⟨k, hk⟩, h⟩ := h,
    rw mem_non_zero_divisors_iff_ne_zero at hb hd hk,
    simp only [set_like.coe_mk, mul_eq_mul_right_iff, hk, or_false] at h,
    split_ifs with ha hc hc ha,
    { simp [ha, hc] },
    { simpa [ha, hc, hb] using h },
    { simpa [ha, hc, hd] using h },
    have hc' : c = a * d / b,
    { rw [h, int.mul_div_assoc _ (dvd_refl _), int.div_self hb, mul_one] },
    subst hc',
    split,
    { rw int.div_eq_div_of_mul_eq_mul,
      { exact (int.gcd_dvd_left _ _).mul_left _ },
      { simp [int.gcd_eq_zero_iff, ha] },
      { simp [int.gcd_eq_zero_iff, hc] },
      sorry },
    { sorry },
  end
  q

[Johan Commelin]

is_fraction_ring asserts that the algebra map ℤ → ℚ is an iso. I'm sure that there is something in mathlib that lets you turn this assertion + algebra_map ℤ ℚ into a ring_equiv.

[Alex J. Best]

Is this what you are looking for?

import field_theory.ratfunc

noncomputable
def iso : ℚ ≃+* fraction_ring ℤ :=
is_localization.ring_equiv_of_ring_equiv ℚ (fraction_ring ℤ) (ring_equiv.refl ℤ)
  (by simp : submonoid.map (ring_equiv.refl ℤ).to_monoid_hom (non_zero_divisors ℤ) = (non_zero_divisors ℤ))

#check iso

[Anne Baanen]

Isn't thereThere is also docs#is_localization.alg_equiv which doesn't need the _of_ring_equiv parameters

[Anne Baanen]

In particular its specialization docs#fraction_ring.alg_equiv:

import ring_theory.localization
#check (fraction_ring.alg_equiv ℤ ℚ).symm.to_ring_equiv

[Kevin Buzzard]

@Yakov Pechersky now ask him to do Dedekind reals = Cauchy reals = uniform completion reals = Eudoxus reals!

[Yakov Pechersky]

You joke, but I think that the fact that this statement isn't easily proven is helping me identify some API holes:

def fwd : ℚ → fraction_ring ℤ :=
λ q, localization.mk q.num
    ⟨q.denom, mem_non_zero_divisors_iff_ne_zero.mpr (by simpa using q.pos.ne')⟩

def rev : fraction_ring ℤ → ℚ :=
λ q, localization.lift_on q (λ n d, rat.mk n d)

def myiso : ℚ ≃ fraction_ring ℤ :=
{ to_fun := fwd,
  inv_fun := rev,
  left_inv := sorry,
  right_inv := sorry }

example : myiso.symm = (fraction_ring.alg_equiv ℤ ℚ).to_equiv :=

[Yakov Pechersky]

Specifically, API in dealing with int.sign, a missing rat.ext, and linking localization and is_localization.

[Reid Barton]

I think n / d is the API, not rat.mk

[Yakov Pechersky]

Right, but that requires me to actually juggle the gcd or lcm, no?

[Reid Barton]

Definitely something went wrong if you're talking about gcds

[Reid Barton]

It does seem annoying though, this is what I came up with:

import field_theory.ratfunc

def fwd : ℚ → fraction_ring ℤ :=
λ q, localization.mk q.num
     ⟨q.denom, mem_non_zero_divisors_iff_ne_zero.mpr (by simpa using q.pos.ne')⟩

def rev : fraction_ring ℤ → ℚ :=
λ q, localization.lift_on q (λ n d, (n : ℚ) / d) begin
  rintros a c b d,
  rw localization.r_iff_exists,
  rintro ⟨k, h⟩,
  dsimp at *,
  rw div_eq_div_iff,
  { exact_mod_cast int.eq_of_mul_eq_mul_right (non_zero_divisors.ne_zero k.2) h },
  { simpa using (non_zero_divisors.ne_zero b.2) },
  { simpa using (non_zero_divisors.ne_zero d.2) }
end


def myiso : ℚ ≃ fraction_ring ℤ :=
{ to_fun := fwd,
  inv_fun := rev,
  left_inv := rat.num_div_denom,
  right_inv := begin
    apply localization.ind,
    rintro ⟨a, b⟩,
    change fwd (a / b) = localization.mk a b,
    change localization.mk _ _ = _,
    set r := (a : ℚ) / b,
    rw localization.mk_eq_mk_iff,
    apply localization.r_of_eq,
    simp only [set_like.coe_mk, mul_one, submonoid.coe_one],
    suffices : (a : ℚ) * r.denom = r.num * b,
    { exact_mod_cast this },
    rw ← div_eq_div_iff,
    { symmetry, apply rat.num_div_denom },
    { simpa using (non_zero_divisors.ne_zero b.2) },
    { exact_mod_cast r.denom_ne_zero }
  end }

[Reid Barton]

I think you're really not supposed to use it this way, and it would be easier to prove that the iso from above equals these functions if you really want that

[Yakov Pechersky]

I tried to follow your suggestion, but I'm having trouble with one of the directions:

import field_theory.ratfunc

-- field of fractions ℚ
noncomputable example : ℚ ≃+* fraction_ring ℤ := (fraction_ring.alg_equiv ℤ ℚ).symm.to_ring_equiv

attribute [simps] fraction_ring.alg_equiv

example : (fraction_ring.alg_equiv ℤ ℚ : fraction_ring ℤ → ℚ) =
  λ q, localization.lift_on q (λ n d, (n / d : ℚ))
    begin
      rintro a c ⟨b, hb⟩ ⟨d, hd⟩,
      rw localization.r_iff_exists,
      rintro ⟨⟨k, hk⟩, h⟩,
      rw mem_non_zero_divisors_iff_ne_zero at hb hd hk,
      simp only [set_like.coe_mk, coe_coe],
      rw div_eq_div_iff,
      { simpa [←int.cast_mul, hk] using h },
      { simpa only [int.cast_eq_zero, ne.def, coe_coe] using hb },
      { simpa only [int.cast_eq_zero, ne.def, coe_coe] using hd },
    end :=
begin
  ext x,
  induction x with n d a b c d h,
  { rw [fraction_ring.alg_equiv_apply, localization.lift_on_mk, localization.mk_eq_mk',
      is_localization.map_mk'],
    simp },
  { simp }
end

-- the equivalence between the two fields is what we expect
example : ((fraction_ring.alg_equiv ℤ ℚ).symm : ℚ → fraction_ring ℤ) =
  λ q, localization.mk q.num
    ⟨q.denom, mem_non_zero_divisors_iff_ne_zero.mpr (by simpa using q.pos.ne')⟩ :=
begin
  ext x,
  simp only [int.cast_coe_nat, set_like.coe_mk, ring_hom.eq_int_cast,
             fraction_ring.alg_equiv_symm_apply, localization.mk_eq_mk'],
  sorry
end

[Yakov Pechersky]

Ehhh I guess I can just use the "forward" result and cheat :)

example : ((fraction_ring.alg_equiv ℤ ℚ).symm : ℚ → fraction_ring ℤ) =
  λ q, localization.mk q.num
    ⟨q.denom, mem_non_zero_divisors_iff_ne_zero.mpr (by simpa using q.pos.ne')⟩ :=
begin
  ext x,
  apply (fraction_ring.alg_equiv ℤ ℚ).injective,
  rw [alg_equiv.apply_symm_apply, fraction_ring.alg_equiv_apply, localization.mk_eq_mk',
      is_localization.map_mk'],
  simp
end

[Yakov Pechersky]

This proof is coming into use to verify that the localization action is c • ⟨a, b⟩ = ⟨c • a, b⟩:

example (z : ℤ) (q : ℚ) :
  localization.smul z ((fraction_ring.alg_equiv ℤ ℚ).symm q) = (fraction_ring.alg_equiv ℤ ℚ).symm (z • q) :=
begin
  have : (fraction_ring.alg_equiv ℤ ℚ).symm q =
    localization.mk q.num
    ⟨q.denom, mem_non_zero_divisors_iff_ne_zero.mpr (by simpa using q.pos.ne')⟩,
  { apply (fraction_ring.alg_equiv ℤ ℚ).injective,
    rw [alg_equiv.apply_symm_apply, fraction_ring.alg_equiv_apply, localization.mk_eq_mk',
        is_localization.map_mk'],
    simp },
  refine (fraction_ring.alg_equiv ℤ ℚ).injective _,
  rw [this, localization.smul_mk, alg_equiv.apply_symm_apply, fraction_ring.alg_equiv_apply,
      localization.mk_eq_mk', is_localization.map_mk'],
  simp [mul_div_assoc]
end

[Yakov Pechersky]

Am I misusing the API here? I feel like there are some simp lemmas that I have to avoid because otherwise I get into a difficult-to-wrangle goal.

[Yakov Pechersky]

The docstring for docs#localization.smul says

/-- Scalar multiplication in a ring localization is defined as `c • ⟨a, b⟩ = ⟨c • a, c • b⟩`. -/

but for "rat ~ fraction_ring int" it seems like it is the z • q.num / q.denom as I would expect. Am I misunderstanding the constructor syntax in the docstring, or something more broadly about how scalar actions on localizations work?

[Reid Barton]

I think the docstring is wrong, judging from the next lemma...

[Yakov Pechersky]

Right. I wanted to make sure that I understood the definition correctly and how localization.mk works by proving an example I thought would differentiate.

[Yakov Pechersky]

Is there a good textbook / outside-of-mathlib reference for the "canonical" choice? A cursory search only found https://math.stackexchange.com/q/2965345, which indicated to me that the choice might have been what the docstring wrote. That's why I was checking.

[Reid Barton]

Right, this is something that Eric and I keep talking about. There are two different situations. If a group (or monoid) acts on a ring, then that means g . (a * b) = (g . a) * (g . b). In that case, in the localization you should also have g . (a / b) = (g . a) / (g . b). The other situation is when considering a localization of an R-algebra. In that case you have r . (a * b) = (r . a) * b and so r . (a / b) = (r . a) / b.
In Lean we write both of these with • and call it mul_action but only the first one is "an action on a ring". (The second one is an action on the underlying set of a ring.)

[Eric Wieser]

@Reid Barton, I think part of the problem is that we don't really have many instances of the type of action you're referring to, according to docs#mul_distrib_mul_action; pretty much the only interesting actions in that list are docs#mul_aut.apply_mul_distrib_mul_action and docs#conj_act.mul_distrib_mul_action, all the rest are inherited actions.

[Kevin Buzzard]

Maybe we should just use new notation for (the rarer) one of these?

[Kevin Buzzard]

Mathematical notation is a bit of an art. We know a * (b + c) = a * b + a * c and choose notation wisely to make this sort of thing happen ("times distributes over plus" is indicated with notation and is probably the reason for BIDMAS/PEMDAS). We also know a * (b * c) = (a * b) * c ("times associates with times")-- Turns out that • definitely distributes over +, and definitely associates with itself, but it can't work out whether it distributes over or associates with *. So maybe it's two notations.