MonoidHom from LE of Localization

Stream: Is there code for X?

[Yakov Pechersky]

Do we the map induced by a submonoid ordering?

import Mathlib

variable {R : Type*} [CommMonoid R] {S T : Submonoid R}

def foo (h : S ≤ T) : Localization S →* Localization T where
  toFun x := Localization.liftOn x (fun r s ↦ .mk r ⟨s, (h s.prop)⟩) <| by
    simp only [Localization.r_iff_exists, Subtype.exists, exists_prop, forall_exists_index, and_imp,
      Subtype.forall, Localization.mk_eq_mk_iff]
    intro a b c hc d hd s hs hs'
    exact ⟨s, h hs, hs'⟩
  map_one' := by
    have : (1 : Localization S) = .mk 1 1 := OreLocalization.one_def -- API lemma missing
    simp [this, Localization.liftOn_mk]
  map_mul' x y := by
    cases x; cases y
    simp [Localization.liftOn_mk, Localization.mk_mul]

[Aaron Liu]

I don't think it's in mathlib

[Eric Wieser]

I guess if we had a monoid version of docs#IsLocalization.lift then you could build it from that?

[Yakov Pechersky]

I am not sure how to use docs#IsLocalization.lift even if I had CommRings in hand and needed a RingHom.