Kernel of localization map

Stream: Is there code for X?

[Christian Merten]

Do we have something like:

import Mathlib

variable {R S P : Type*} (Q : Type*) [CommSemiring R] [CommSemiring S] [CommSemiring P]
  [CommSemiring Q]
  {M : Submonoid R} {T : Submonoid P}
  [Algebra R S] [Algebra P Q] [IsLocalization M S] [IsLocalization T Q]
  (g : R →+* P) (hy : M ≤ Submonoid.comap g T)

variable (S) in
def kerMap : RingHom.ker g →ₗ[R] RingHom.ker (IsLocalization.map Q g hy : S →+* Q) where
  toFun x := ⟨algebraMap R S x, by simp [RingHom.mem_ker, (RingHom.mem_ker g).mp x.property]⟩
  map_add' x y := by
    simp only [AddSubmonoid.coe_add, Submodule.coe_toAddSubmonoid, map_add, AddSubmonoid.mk_add_mk]
  map_smul' a x := by
    simp only [SetLike.val_smul, smul_eq_mul, map_mul, RingHom.id_apply,
      SetLike.mk_smul_of_tower_mk, Algebra.smul_def]

instance : IsLocalizedModule M (kerMap S Q g hy) :=
  sorry

[Andrew Yang]

docs#Submodule.isLocalizedModule is close.

[Christian Merten]

Thanks for the pointer. I managed to show it directly, but I'll revisit this later when I am done proving my goal.