localizations

Stream: maths

[Johan Commelin]

I'm confused by the recent refactor of localisations... everything is now about characteristic predicates, which is great. But we still need to know that localisations exist... did we accidentally throw away the construction?

[Johan Commelin]

Or am I just blind and bad at searching...

[Chris Hughes]

I had the same thought. @Amelia Livingston

[Alex J. Best]

Yeah we don't seem to have that, if anyone wants to play with one specific one though:

def int.cast_rat_raction_map : fraction_map ℤ ℚ :=
{
  map_units' := λ x, is_unit_iff_ne_zero.mpr (begin
    intro, cases x,
    rw [submonoid.mem_carrier, mem_non_zero_divisors_iff_ne_zero] at x_property,
    change (x_val : ℚ) = 0 at a,
    apply x_property,
    exact_mod_cast a,
  end),
  surj' := λ x, begin
    use (⟨x.num, ⟨(x.denom : ℤ), begin
        rw [submonoid.mem_carrier, mem_non_zero_divisors_iff_ne_zero],
        exact int.coe_nat_ne_zero_iff_pos.mpr x.pos,
      end⟩⟩ : ℤ × ↥(non_zero_divisors ℤ)),
      change x * (x.denom) = x.num,
      exact rat.mul_own_denom_eq_num, end,
  eq_iff_exists' := λ x y, begin
    split; intro,
    { use 1, simp only [mul_one, submonoid.coe_one] at *,
      change (x : ℚ) = y at a, exact_mod_cast a, },
    { cases a, change (x : ℚ) = y, norm_cast,
      have : (↑a_w : ℤ) ≠ 0 := by intro;
        exact zero_ne_one.symm (a_w.2 1
          (by rw (show (a_w.val : ℤ) = 0, from a); exact mul_zero 1)),
    exact (int.eq_of_mul_eq_mul_right this) a_h,}
   end,
   ..int.cast_ring_hom ℚ
  }

[Johan Commelin]

But the construction used to be there...
@Alex J. Best Thanks! PR!

[Alex J. Best]

Johan Commelin said:

But the construction used to be there...
Alex J. Best Thanks! PR!

#2921 naming/location comments welcome!

[Johan Commelin]

Thanks! I've left some comments

[Yury G. Kudryashov]

We have a construction in monoid_localization.

[Yury G. Kudryashov]

It's called submonoid.localization. It works for rings too, don't know whether we have a proof.

[Johan Commelin]

Aah, ok. And that can automagically be reused in, say fraction_map?

[Johan Commelin]

I know the underlying type works for rings...

[Johan Commelin]

But I guess there will be some proof obligations

[Amelia Livingston]

Sorry - it's coming back. I should have put it in the first PR; I had planned to open the second one quicker but things got in the way. I will open a little one with the old construction today.

[Johan Commelin]

Great, thanks!