Zulip Chat Archive

Stream: maths

Topic: localizations


view this post on Zulip Johan Commelin (Jun 02 2020 at 09:02):

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?

view this post on Zulip Johan Commelin (Jun 02 2020 at 09:02):

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

view this post on Zulip Chris Hughes (Jun 02 2020 at 10:49):

I had the same thought. @Amelia Livingston

view this post on Zulip Alex J. Best (Jun 02 2020 at 15:50):

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 
  }

view this post on Zulip Johan Commelin (Jun 02 2020 at 16:40):

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

view this post on Zulip Alex J. Best (Jun 02 2020 at 18:07):

Johan Commelin said:

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

#2921 naming/location comments welcome!

view this post on Zulip Johan Commelin (Jun 02 2020 at 18:12):

Thanks! I've left some comments

view this post on Zulip Yury G. Kudryashov (Jun 02 2020 at 18:15):

We have a construction in monoid_localization.

view this post on Zulip Yury G. Kudryashov (Jun 02 2020 at 18:17):

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

view this post on Zulip Johan Commelin (Jun 02 2020 at 18:17):

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

view this post on Zulip Johan Commelin (Jun 02 2020 at 18:17):

I know the underlying type works for rings...

view this post on Zulip Johan Commelin (Jun 02 2020 at 18:17):

But I guess there will be some proof obligations

view this post on Zulip Amelia Livingston (Jun 02 2020 at 18:33):

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.

view this post on Zulip Johan Commelin (Jun 02 2020 at 18:39):

Great, thanks!


Last updated: May 11 2021 at 15:12 UTC