extend a ring hom to the localisation

Stream: Is there code for X?

[Kevin Buzzard]

I'm assuming we have this somewhere but I can't find it:

import Mathlib.RingTheory.Localization.Basic

/- If φ : R → A is a ring hom and the image of S is contained in the units of A, then
φ extends to a map R[1/S] → A -/
def foo (R : Type) [CommRing R] (S : Submonoid R) (A : Type) [CommRing A]
    (φ : R →+* A) (hφ : ∀ s ∈ S, IsUnit (φ s)) : Localization S →+* A := sorry

[Adam Topaz]

IsLocalization.lift

[Adam Topaz]

Note that this works

import Mathlib

def foo (R : Type) [CommRing R] (S : Submonoid R) (A B : Type) [CommRing A] [CommRing B]
    [Algebra R B] [IsLocalization S B] (φ : R →+* A) (hφ : ∀ s : S, IsUnit (φ s)) :
    B →+* A := exact?%

but this fails:

import Mathlib

def foo (R : Type) [CommRing R] (S : Submonoid R) (A : Type) [CommRing A]
    (φ : R →+* A) (hφ : ∀ s : S, IsUnit (φ s)) : Localization S →+* A := exact?%

I guess this is an example of a weak point of exact?, namely that it can't guess instances like IsLocalization S (Localization S).

[Kevin Buzzard]

Right, I tried by exact? and this failed so I asked here :-) Thanks! I was looking in the wrong files for this.

[Adam Topaz]

(Note that I also changed the hypothesis h\phi slightly)

[Kevin Buzzard]

Yeah I was guessing how to say this, any way will do :-)