Localization functor

Stream: Is there code for X?

[Edison Xie]

Do we have this in mathlib? Is this just some other special case of the localization functor in catregory theory folder?

import Mathlib

open IsLocalizedModule in
noncomputable def LocalizationFunctor {R : Type*} [CommRing R] (S : Submonoid R):
    ModuleCat R ⥤ ModuleCat (Localization S) where
  obj M := ModuleCat.of _ <| LocalizedModule S M
  map {M N} f := ModuleCat.ofHom <| {
      __ := IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M)
        (LocalizedModule.mkLinearMap S N) f.hom
      map_smul' sr sm := by
        induction sm using LocalizedModule.induction_on with
        | h m s =>
        induction sr using Localization.induction_on with
        | H rs =>
        simp [LocalizedModule.mk_smul_mk, map_LocalizedModules]
      }
  map_id M := by ext; simp
  map_comp f g := by
    ext1
    simp only [ModuleCat.hom_ofHom, ModuleCat.hom_comp]
    ext x
    simp only [LinearMap.coe_mk, LinearMap.coe_toAddHom, LinearMap.coe_comp]
    rw [← LinearMap.coe_comp]
    erw [← IsLocalizedModule.map_comp']

[Joël Riou]

I do not think it is in mathlib. It should probably go in some new file in Algebra.Category.ModuleCat, and under some suitable assumptions on the universes, it should be compared to the tensor product functor.
That this is a localization functor (with a calculus of fractions) should follow from docs#CategoryTheory.Adjunction.isLocalization_leftAdjoint