## Stream: maths

### Topic: localizations

#### 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?

#### Johan Commelin (Jun 02 2020 at 09:02):

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

#### Chris Hughes (Jun 02 2020 at 10:49):

I had the same thought. @Amelia Livingston

#### 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 ℚ
}


#### Johan Commelin (Jun 02 2020 at 16:40):

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

#### Alex J. Best (Jun 02 2020 at 18:07):

Johan Commelin said:

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

#### Yury G. Kudryashov (Jun 02 2020 at 18:15):

We have a construction in monoid_localization.

#### 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.

#### Johan Commelin (Jun 02 2020 at 18:17):

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

#### Johan Commelin (Jun 02 2020 at 18:17):

I know the underlying type works for rings...

#### Johan Commelin (Jun 02 2020 at 18:17):

But I guess there will be some proof obligations

#### 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.

#### Johan Commelin (Jun 02 2020 at 18:39):

Great, thanks!

Last updated: May 11 2021 at 15:12 UTC