canonical isomorphism between localizations

Stream: Is there code for X?

[Nikolas Kuhn]

What is the slickest way to give the canonical isomorphism between two localizations of a ring at the same sub-monoid? Concretely, I'd like to prove something along these lines

example (R S : Type) [comm_ring R] [comm_ring S] (a: R →+* S) (r : R)  :
  localization.away (a r) ≃+* localization (submonoid.map ⟨a.1, a.2, a.3⟩ (submonoid.powers r)) :=
sorry

(I believe that the isomorphism is in fact secretely an equality.)

Ultimately, I want to identify the two maps obtained from localizing R at r along this isomorphism, but it would be helpful to construct it first.

[Adam Topaz]

docs#is_localization.alg_equiv gives the isomorphism between two localizations at the same submonoid.

[Adam Topaz]

So if you prove that, say, the RHS has a is_localization instance of the right shape, that would give it to you.

[Adam Topaz]

This would give an isomorphism of algebras, which you can then covert to a ring isomorphism if absolutely necessary

[Adam Topaz]

If the two sides are really defeq, then you should be able to use docs#ring_equiv.refl

[Nikolas Kuhn]

Thanks! I could make something work:

import ring_theory.localization.basic

example (R S : Type) [comm_ring R] [comm_ring S] (a: R →+* S) (f: R) :
localization (submonoid.map ⟨a.1, a.2, a.3⟩ (submonoid.powers f)) ≃ₐ[S]  localization.away (a f):=
begin
  have h₁ : submonoid.map ↑a (submonoid.powers f) = submonoid.powers (a f) :=
    submonoid.map_powers _ _,
  have h₂: is_localization (submonoid.powers (a f)) (localization.away (a f)), by apply_instance,
  rw ← congr_arg is_localization h₁ at h₂,
  exact @localization.alg_equiv _ _
    (submonoid.map ↑a (submonoid.powers f)) (localization.away (a f)) _ _ h₂,
end

[Yakov Pechersky]

Your have h2 should be a haveI and that way you won't have to use the @ at the end

[Nikolas Kuhn]

Ah, great. I was wondering how to add instances.

[Nikolas Kuhn]

Although I seem to still have to introduce h_2 in order to rewrite it...

[Eric Wieser]

⟨a.1, a.2, a.3⟩ should be a.to_monoid_hom or maybe just a